# 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ₗ) → Set ℓ 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 : Set 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 ⊥ : Set where
data Bad : Set 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.