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.