Strictly Positive Type

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):

$$\begin{gathered} \text{data }T:\text{Set where} \\ c:(T\to \perp )\to T \end{gathered}$$

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).

Relation to Functors

In category theory, strictly positive types correspond to initial algebras for 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
• abbott2004-containers