DatatypeAndFunctionDefinitions

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
   bad : (Bad -> Bad) -> Bad

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)