strictly positive

Definition

In type theory, strict positivity is a syntactic restriction on inductive type definitions requiring that the type being defined, $T$, occurs only to the right of function arrows in the types of its constructor arguments. This constraint ensures the defined type represents a well-founded least fixed point and guarantees the termination of recursive functions and logical consistency.

Formally, we say $T$ occurs strictly positively in a type expression $E$ if any of the following holds:

1. $E$ does not contain $T$.
2. $E$ is $T$.
3. $E$ is $\Pi (x:A).B$ (or $A\to B$) where $T$ does not occur in $A$, and $T$ occurs strictly positively in $B$.
4. $E$ is an application of a previously defined strictly positive type constructor (e.g., $ListT$), where $T$ occurs strictly positively in the parameters.

Non-strictly Positive Example

We reject definitions where $T$ occurs in a negative position (to the left of an arrow):

&\text{data } T : \text{Set where} \\ &\quad c : (T \to \bot) \to T \end{aligned} $$ Here $T$ occurs negatively in the domain of the argument to $c$. This violation allows the encoding of paradoxical combinators, leading to non-termination and inconsistency ([[Girard's Paradox]]). If we suppose that we do have an initial algebra then this would mean that there is some type $⟦\ T\ ⟧ : \mathrm{Set}_1$ such that there is an isomorphism between the forming functor,

\begin{aligned} F:\mathrm{Set}\to \mathrm{Set}\ F X = X\to \bot\ (⟦\ T\ ⟧\to \bot) \cong ⟦\ T\ ⟧ \end{aligned}

In particular there is some $f : (⟦\ T\ ⟧ \to \bot)\to ⟦\ T\ ⟧$ and some $g : ⟦\ T\ ⟧\to (⟦\ T\ ⟧ \to \bot)$. Which lets us construct a term of $\bot$ ([[Empty Type|a very bad thing]]),

\begin{aligned} y:=f (\lambda x.g\ x\ x): ⟦\ T\ ⟧\ z:=g\ y\ y :\bot \end{aligned}

## Relation to Functors In [[category theory]], strictly positive types correspond to [[Algebra on an Endofunctor|initial algebras]] for [[Strictly Positive Functor|strictly positive functors]]. A functor $F$ is strictly positive if it can be built from constant functors, the identity functor, products, and coproducts (and fixed points thereof). ## References - [[coquand1988-inductive-types|coquand1988]] - [[abbott2004-containers]]