Skip to content

Stay Positive

Let us explore the concept of strictly positive inductive data types, a critical requirement within the Juvix framework for classifying a data type as well-typed.

An inductive type is considered strictly positive if it either:

  1. Does not appear within the argument types of its constructors, or
  2. Appears strictly positively within the argument types of its constructors.

A name is considered strictly positive for an inductive type if it never appears in a negative position within the argument types of its constructors. The term negative position denotes instances located to the left of an arrow in a type constructor argument.

Example

Consider the following data type X where A and B are types in scope:

  type X :=
    | c0 : (B -> X) -> X
    | c1 : (X -> A) -> X;

In this example, the type X occurs strictly positively in the constructor c0, but negatively in the constructor c1 in the type argument X -> A. Therefore, X is not strictly positive.

Positive parameters can also be described as those that do not occur in negative positions. For instance, the type B in the c0 constructor above appears to the left of the arrow B->X, placing B in a negative position. It is essential to consider negative parameters when verifying strictly positive data types, as they might enable the definition of non-strictly positive data types.

Let us consider another example:

  type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;

  type T1 := c1 : T0 T1 -> T1;

In this example, the type T0 is strictly positive, while the type T1 is not. It is only after unfolding the type application T0 T1 in the data constructor c1 that we can determine T1 occurs in a negative position due to T0. More specifically, the type parameter A of T0 is negative.

Bypassing the Strict Positivity Condition

To bypass the positivity check in a data type declaration, you can annotate it with the positive keyword. Alternatively, you can use the CLI global flag --no-positivity when type checking a Juvix file.

  positive
  type T0 (A : Type) := c0 : (T0 A -> A) -> T0 A;

Examples of Non-Strictly Positive Data Types

  • The Bad data type is not strictly positive due to the negative parameter A of Tree.
  type Tree (A : Type) :=
    | leaf : Tree A
    | node : (A -> Tree A) -> Tree A;

  type Bad := bad : Tree Bad -> Bad;
  • A is a negative parameter.
  type B (A : Type) := b : (A -> B (B A -> A)) -> B A;