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