Strictly positive data types
We follow a syntactic description of strictly positive inductive data types.
An inductive type is said to be strictly positive if it does not occur or occurs strictly positively in the types of the arguments of its constructors. A name qualified as strictly positive for an inductive type if it never occurs at a negative position in the types of the arguments of its constructors. We refer to a negative position as those occurrences on the left of an arrow in a type constructor argument.
In the example below, the type X
occurs strictly positive in c0
and
negatively at the constructor c1
. Therefore, X
is not strictly
positive.
axiom B : Type;
inductive X {
c0 : (B > X) > X;
c1 : (X > X) > X;
};
We could also refer to positive parameters as such parameters occurring
in no negative positions. For example, the type B
in the c0
constructor above is on the left of the arrow B>X
. Then, B
is at a
negative position. Negative parameters need to be considered when
checking strictly positive data types as they may allow to define
nonstrictly positive data types.
In the example below, the type T0
is strictly positive. However, the
type T1
is not. Only after unfolding the type application T0 (T1 A)
in the data constructor c1
, we can find out that T1
occurs at a
negative position because of T0
. More precisely, the type parameter
A
of T0
is negative.
inductive T0 (A : Type) {
c0 : (A > T0 A) > T0 A;
};
inductive T1 {
c1 : T0 T1 > T1;
};
Bypass the strict positivity condition
To bypass the positivity check, a data type declaration can be annotated
with the keyword positive
. Another way is to use the CLI global flag
nopositivity
when typechecking a Juvix
File.
$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
module E5;
positive
inductive T0 (A : Type){
c0 : (T0 A > A) > T0 A;
};
end;
Examples of nonstrictly data types

NSPos
is at a negative position inc
.inductive Empty {}; inductive NSPos { c : ((NSPos > Empty) > NSPos) > NSPos; };

Bad
is not strictly positive beceause of the negative parameterA
ofTree
.inductive Tree (A : Type) { leaf : Tree A; node : (A > Tree A) > Tree A; }; inductive Bad { bad : Tree Bad > Bad; };

A
is a negative parameter.inductive B (A : Type) { b : (A > B (B A > A)) > B A; };