Inductive data types

The inductive keyword is reserved for declaring inductive data types. An inductive type declaration requires a unique name for its type and its constructors, functions for building its terms. Constructors can be used as normal identifiers and also in patterns. As shown later, one can also provide type parameters to widen the family of inductive types one can define in Juvix.

The simplest inductive type is the Empty type with no constructors.

inductive Empty {};

In the following example, we declare the inductive type Nat, the unary representation of natural numbers. This type comes with two data constructors, namely zero and suc. A term of the type Nat is the number one, represented by suc zero or the number two represented by suc (suc zero), etc.

inductive Nat {
    zero : Nat;
    suc : Nat → Nat;
};

The way to use inductive types is by declaring functions by pattern matching. Let us define, for example, the function for adding two natural numbers.

inifl 6 +;
+ : Nat → Nat → Nat;
+ zero b ≔ b;
+ (suc a) b ≔ suc (a + b);

As mentioned earlier, an inductive type may have type parameters. The canonical example is the polymorphic type List. The type List is the inductive type that considers the type of the elements in the list as a parameter. A constructor to build the empty list, that is the base case, and another constructor to enlarge the list, we usually called it cons. One possible definition for this type is the following type taken from the Juvix standard library:

infixr 5 ∷;
inductive List (A : Type) {
  nil : List A;
  ∷ : A → List A → List A;
};

elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
elem _ _ nil ≔ false;
elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;

To see more examples of inductive types and how to use them, please check out the Juvix standard library