# Simple Inductive Types

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

## Table of contents

- Example datatypes
- General form
- Formation and introduction rules
- Definition by pattern matching
- Elimination and equality rules
- Large elimination
- Beyond elimination rules
- Large inductive types

## 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 c_{1}: A_{1}... c_{n}: A_{n}

The name D of the data type and the names c_{1}, ..., c_{n} of the constructors must be new wrt the current signature and context.

Agda checks that A_{1}, ..., A_{n} : Set wrt the current signature and context. Moreover, each A_{i} has the form

(y_{1}: B_{1}) -> ... -> (y_{m}: B_{m}) -> D

where an argument types B_{i} of the constructors is either

*non-inductive*(a*side condition*) and does not mention D at all,- or
*inductive*and has the form

(z_{1}: C_{1}) -> ... -> (z_{k}: C_{k}) -> D

where D must not occur in any C_{j}.

### Strict positivity

The condition that D must not occur in any C_{j} can be also phrased as D must only occur *strictly positively* in B_{i}.

Agda can check this positivity condition.

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

c_{1}: A_{1}... c_{n}: A_{n}

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.