# 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 : Set where
zero : Nat
suc  : Nat  Nat

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

data Bool : Set where
true  : Bool
false : Bool

The True set represents the trivially true proposition:

data True : Set where
tt : True

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

data False : Set where

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

data BinTree : Set where
leaf   : Nat  BinTree
branch : BinTree  BinTree  BinTree

Finally, the data type of Brouwer ordinals:

data Ord : Set 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 : Setᵢ 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 : Set) : Set 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 Set. For example, fixed-length vectors can be defined by indexing them over their length of type Nat:

data Vector (A : Set) : Nat  Set 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 Set can be defined as follows:

data Even : Nat  Set 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ₗ)  Setwhere
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

--     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: Set where