# Inductive Data Types And Pattern Matching

We will begin with a very simple notion, and will then gradually introduce more and more complex classes of data types: parameterized data types, indexed families of data types ("inductive families), and inductive-recursive data types.

Functions can be introduced by giving a type and a definition. For instance, the polymorphic identity function can be defined by

``` id : {A : Set} -> A -> A
id x = x
```

Note that the implicit argument is left out in the left hand side. As in a lambda abstraction it can be given explicitly by enclosing it in curly braces:

``` id : {A : Set} -> A -> A
id {A} x = x
```

Datatypes are introduced by `data` declarations. For instance, the natural numbers can be defined by

``` data Nat : Set where
zero : Nat
suc  : Nat -> Nat
```

To ensure normalisation, inductive occurrences must appear in strictly positive positions. For instance, the following datatype is not allowed:

``` data Bad : Set where
```

since there is a negative occurrence of `Bad` in the argument to the constructor.

Functions over elements of a datatype can be defined using pattern matching and structural recursion. The addition function on natural numbers is defined by

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

The operator form can be used both in left hand sides and right hand sides as seen here.

Datatypes can be parametrised over a telescope of parameters. These are written after the name of the datatype and scope over the constructors.

``` data List (A : Set) : Set where
[]   : List A
_::_ : A -> List A -> List A
```

This will introduce the constructors

``` []   : {A : Set} -> List A
_::_ : {A : Set} -> A -> List A -> List A
```

We can also define families of datatypes. For instance, the family over natural numbers `n` of proofs that `n` is even.

``` data IsEven : Nat -> Set where
evenZ  : IsEven zero
evenSS : (n : Nat) -> IsEven n -> IsEven (suc (suc n))
```

Note the difference between the left and the right side of the first `:`. Types appearing on the left are parameters and scope over the constructors. These have to be unchanged in the return types of the constructors. Types appearing on the right are indices which are not in scope in the constructors, and which take on arbitrary values in the constructor return types.

When pattern matching on an element of an inductive family we get information about the index. To distinguish parts of a pattern which are determined by pattern matching (the inaccessible patterns) and the parts which constitutes the actual pattern matching, the inaccessible patterns are prefixed with a dot. In For instance, we can prove that the sum of two even numbers is also even.

``` even+ : (n m : Nat) -> IsEven n -> IsEven m -> IsEven (n + m)
even+ .zero          m  evenZ        em = em
even+ .(suc (suc n)) m (evenSS n en) em =
evenSS (n + m) (even+ n m en em)
```

The proof is by recursion on the proof that `n` is even. Pattern matching on this proof will force the value of `n` and hence the patterns for `n` are prefixed with a dot to indicate that they are not part of the pattern matching. In this case we can make `n` and `m` implicit and write the proof as

``` even+ : {n m : Nat} -> IsEven n -> IsEven m -> IsEven (n + m)
even+  evenZ        em = em
even+ (evenSS n en) em = evenSS _ (even+ en em)
```