Skip to content

Data types

A data type declaration consists of:

  • The type keyword,
  • a unique name for the type,
  • the := symbol, and
  • a non-empty list of constructor declarations (functions for building the elements of the data type).

The simplest data type is the Unit type with one constructor called unit.

type Unit := unit : Unit;

In the following example, we declare the type Nat – the unary representation of natural numbers. This type comes with two constructors: zero and suc. Example elements of type Nat are the number one represented by suc zero, the number two represented by suc (suc zero), etc.

type Nat :=
  | zero : Nat
  | suc : Nat -> Nat;

Constructors can be used like normal functions or in patterns when defining functions by pattern matching. For example, here is a function adding two natural numbers:

infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);

A data type can possess type parameters. When a data type has a type parameter A, it is referred to as polymorphic in A. A classic example of this concept is the List type, which is polymorphic in the type of its list elements.

  infixr 5 ::;
  type List (A : Type) :=
    | nil : List A
    | :: : A -> List A -> List A;

The following function determines whether an element is in a list or not.

  open import Stdlib.Data.Bool using {Bool;false;||};

  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;

For more examples of inductive types and how to use them, see the Juvix standard library.