# 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.