Data Types

Simple datatypes

Example datatypes

In the introduction we already showed the definition of the data type of natural numbers (in unary notation):

data Nat : Type where
    zero : Nat
    suc  : Nat → Nat

We give a few more examples. First the data type of truth values:

data Bool : Type where
  true  : Bool
  false : Bool

The True set represents the trivially true proposition:

data True : Type where
    tt : True

The False set has no constructor and hence no elements. It represents the trivially false proposition:

data False : Type where

Another example is the data type of non-empty binary trees with natural numbers in the leaves:

data BinTree : Type where
  leaf   : Nat → BinTree
  branch : BinTree → BinTree → BinTree

Finally, the data type of Brouwer ordinals:

data Ord : Type where
  zeroOrd : Ord
  sucOrd  : Ord → Ord
  limOrd  : (Nat → Ord) → Ord

General form

The general form of the definition of a simple datatype D is the following

data D : Typeᵢ where
  c₁ : A₁
  ...
  cₙ : Aₙ

The name D of the data type and the names c₁, …, cₙ of the constructors must be new w.r.t. the current signature and context, and the types A₁, …, Aₙ must be function types ending in D, i.e. they must be of the form

(y₁ : B₁) → ... → (yₘ : Bₘ) → D

Parametrized datatypes

Datatypes can have parameters. They are declared after the name of the datatype but before the colon, for example:

data List (A : Type) : Type where
  []  : List A
  _∷_ : A → List A → List A

Indexed datatypes

In addition to parameters, datatypes can also have indices. In contrast to parameters which are required to be the same for all constructors, indices can vary from constructor to constructor. They are declared after the colon as function arguments to Type. For example, fixed-length vectors can be defined by indexing them over their length of type Nat:

data Vector (A : Type) : Nat → Type where
  []  : Vector A zero
  _∷_ : {n : Nat} → A → Vector A n → Vector A (suc n)

Notice that the parameter A is bound once for all constructors, while the index {n : Nat} must be bound locally in the constructor _∷_.

Indexed datatypes can also be used to describe predicates, for example the predicate Even : Nat → Type can be defined as follows:

data Even : Nat → Type where
  even-zero  : Even zero
  even-plus2 : {n : Nat} → Even n → Even (suc (suc n))

General form

The general form of the definition of a (parametrized, indexed) datatype D is the following

data D (x₁ : P₁) ... (xₖ : Pₖ) : (y₁ : Q₁) → ... → (yₗ : Qₗ) → Type ℓ where
  c₁ : A₁
  ...
  cₙ : Aₙ

where the types A₁, …, Aₙ are function types of the form

(z₁ : B₁) → ... → (zₘ : Bₘ) → D x₁ ... xₖ t₁ ... tₗ

Strict positivity

When defining a datatype D, Agda poses an additional requirement on the types of the constructors of D, namely that D may only occur strictly positively in the types of their arguments.

Concretely, for a datatype with constructors c₁ : A₁, …, cₙ : Aₙ, Agda checks that each Aᵢ has the form

(y₁ : B₁) → ... → (yₘ : Bₘ) → D

where an argument types Bᵢ of the constructors is either

non-inductive (a side condition) and does not mention D at all,
or inductive and has the form
```
(z₁ : C₁) → ... → (zₖ : Cₖ) → D
```
where D must not occur in any Cⱼ.

The strict positivity condition rules out declarations such as

data Bad : Type where
    bad : (Bad → Bad) → Bad
    --     A     B      C
    -- A is in a negative position, B and C are OK

since there is a negative occurrence of Bad in the type of the argument of the constructor. (Note that the corresponding data type declaration of Bad is allowed in standard functional languages such as Haskell and ML.).

Non strictly-positive declarations are rejected because they admit non-terminating functions.

If the positivity check is disabled, so that a similar declaration of Bad is allowed, it is possible to construct a term of the empty type, even without recursion.

{-# OPTIONS --no-positivity-check #-}

data ⊥ : Type where

data Bad : Type where
  bad : (Bad → ⊥) → Bad

self-app : Bad → ⊥
self-app (bad f) = f (bad f)

absurd : ⊥
absurd = self-app (bad self-app)

For more general information on termination see Termination Checking.