Skip to content

2022

Stay Positive with Your Data Types

In this discussion, we will 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.