Skip to content

Juvix Blog

Hola and welcome to the Juvix blog!

Welcome to our cosy corner, where we dive into the world of functional programming and next-generation distributed apps! We'll be exploring Juvix and beyond, discussing fascinating aspects and applications. So come on in, and let's embark on this exciting journey together!

What can you expect?

Throughout our articles, you'll discover functional programming (FP), and potentially, implementation notes pertinent to the ongoing development cycles of Juvix. Our primary objective is to share our insights about Juvix while encouraging discussions centred on functional programming concepts and methodologies.

Stay Positive with Your Data Types

In this blog post, we will investigate the notion of strictly positive inductive data types, which is a condition that Juvix mandates for a data type to be considered 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.


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

  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;