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:
- Does not appear within the argument types of its constructors, or
- 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.