# Simple Inductive Types

This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0

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

Then the unit set:

```  data True : Set where
tt : True
```

The True set represents the trivially true proposition.

```  data False : Set where
```

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

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 data type D is the following

``` data D : Set where
c1 : A1
...
cn : An
```

The name D of the data type and the names c1, ..., cn of the constructors must be new wrt the current signature and context.

Agda checks that A1, ..., An : Set wrt the current signature and context. Moreover, each Ai has the form

``` (y1 : B1) -> ... -> (ym : Bm) -> D
```

where an argument types Bi of the constructors is either

• non-inductive (a side condition) and does not mention D at all,
• or inductive and has the form
``` (z1 : C1) -> ... -> (zk : Ck) -> D
```

where D must not occur in any Cj.

### Strict positivity

The condition that D must not occur in any Cj can be also phrased as D must only occur strictly positively in Bi.

Agda can check this positivity condition.

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 one can write a non-terminating function using them.

To see how one can write a looping definition using the Bad datatype from above, see BadInHaskell. For more general information on termination see Totality.

## Formation and introduction rules

The declaration above of the data type I generates a typing

```  D : Set
```

which is called the formation rule of D in Martin-Löf type theory. Similarly the typings of the constructors

```  c1 : A1
...
cn : An
```

are called the introduction rules of I in Martin-Löf type theory.

## Definition by pattern matching

When a data type has been declared functions can be defined by pattern matching on its elements. Here are some examples.

```  _+_ : Nat -> Nat -> Nat
m + zero = m
m + suc n = suc (m + n)

not : Bool -> Bool
not true  = false
not false = true

_+'_ : Ord -> Ord -> Ord
m +' zeroOrd  = m
m +' sucOrd n = sucOrd (m +' n)
m +' limOrd f = limOrd (\n -> m +' f n)
```

Agda has a special facility for pattern matching over an empty type. For example, we can define a function from the empty set to an arbitrary other set:

```  emptyfunction : (C : Set) -> False -> C
emptyfunction C ()
```

This is definition by pattern matching on the elements of False. Since this type has no elements, there are no cases. Agda indicates this by the second line, which tells the system that this is definition by no cases on the second argument.

## Elimination and equality rules

All these cases are examples of ''structural recursion" (in one argument) on the way an element of a given data type is defined. To each correct data type declaration we can associate a constant (the recursor or elimination constant) which expresses the general principle of structural recursion for the data type. Each such constant is defined by pattern matching:

```  natrec : (C : Nat -> Set) -> C zero -> ((x : Nat) -> C x -> C (suc x)) -> (z : Nat) -> C z
natrec C d e zero    = d
natrec C d e (suc n) = e n (natrec C d e n)

if : (C : Bool -> Set) -> C true -> C false -> (z : Bool) -> C z
if C d e true  = d
if C d e false = e

onecase : (C : True -> Set) -> C tt -> (z : True) -> C z
onecase C d tt = d

nocase : (C : False -> Set) -> (z : False) -> C z
nocase C ()

ordrec : (C : Ord -> Set) -> C zeroOrd -> ((x : Ord) -> C x -> C (sucOrd x)) -> ((f : Nat -> Ord) -> ((x : Nat) -> C (f x)) -> C (limOrd f)) -> (z : Ord) -> C z
ordrec C d e g zeroOrd    = d
ordrec C d e g (sucOrd a) = e a (ordrec C d e g a)
ordrec C d e g (limOrd f) = g f (\x -> ordrec C d e g (f x))
```

The typings of these constants are called elimination rules in Martin-Löf type theory and the defining equations are called equality rules.

## Large elimination

We can also define sets by structural recursion. Here is a definition of the function which translates an element in Bool to the corresponding Set:

```  isTrue : Bool -> Set
isTrue true  = True
isTrue false = False
```

We can even define large versions of the elimination constants above. For example,

```  if1 : (C : Bool -> Set1) -> C true -> C false -> (z : Bool) -> C z
if1 C d e true  = d
if1 C d e false = e
```

## Beyond elimination rules

Agda's pattern matching goes beyond the usual notion of structural recursion in one argument.

``` We can for example define a function by pattern matching on two arguments

_==_ : Nat -> Nat -> Bool
zero  == zero  = true
zero  == suc n = false
suc m == zero  = false
suc m == suc n = m == n
```

Recursive calls can more generally be on structurally smaller arguments:

```  half : Nat -> Nat
half zero          = zero
half (suc zero)    = zero
half (suc (suc n)) = suc (half n)
```

Agda allows quite a general class of definition of recursive functions by pattern matching. Both a termination checker (which checks size-change termination in the sense Jones et al) and a coverage checker are provided, but we postpone the description of these until later - see Totality.

## Large inductive types

Agda also allows the definition of large inductive types, such as

```  data Large : Set1 where
El    : Set -> Large
Arrow : Large -> Large -> Large
```

Since one of the constructors of Large ranges over the type Set, Large cannot be a member of Set but has to belong to the next universe Set1.

In general, to define a data type in Set(i+1) all constructor types must be in Seti.