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:

  • 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:

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

Polymorphic data type

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.

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

  import Stdlib.Data.Bool open 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.

Comments