Overview of the language

What follows is a very brief introduction to the main features of the Agda language. Do not expect to understand everything if you've never used a similar language before. It should nevertheless give you a feeling of the language...

What follows is taken directly from the old documentation... Some work might be needed

Functions

Function types are written `(x : A) -> B` or `A -> B` for non-dependent functions. Function types can range over arbitrary telescopes, for instance, the type of the substitutivity law for a polymorphic equality

``` Eq : (A : Set) -> A -> A -> Set
```

can be stated as

``` (A : Set)(C : A -> Set)(x y : A) -> Eq A x y -> C x -> C y
```

Functions are constructed by lambda abstractions, which can be either typed or untyped. For instance, both expressions below have type `(A : Set) -> A -> A` (the second expression checks against other types as well):

``` \ (A : Set)(x : A) -> x
\ A x -> x
```

Implicit arguments

It is possible to omit terms that the type checker can figure out for itself, replacing them by `_`. If the type checker cannot infer the value of an `_` it will report an error. For instance, for the polymorphic identity function

``` `id : (A : Set) -> A -> A`
```

the first argument can be inferred from the type of the second argument, so we might write `id _ zero` for the application of the identity function to `zero`.

Implicit function spaces are written with curly braces instead of parenthesis. For instance,

``` _==_  : {A : Set} -> A -> A -> Set
subst : {A : Set}(C : A -> Set){x y : A} -> x == y -> C x -> C y
```

Note how the first argument to `_==_` is left implicit. Similarly we may leave out the implicit arguments `A`, `x`, and `y` in an application of `subst`. To give an implicit argument explicitly, enclose in curly braces. The following two expressions are equivalent:

``` subst C eq cx
subst {_} C {_} {_} eq cx
```

Worth noting is that implicit arguments will be inserted also at the end of an application, so the following is equivalent:

``` subst C
subst C {_} {_}
```

To get the function of type `{x y : A} -> x == y -> C x -> C y` we have to explicitly abstract over `x` and `y`:

``` \{x}{y} -> subst C
```

Implicit arguments can also be referred to by name, so if we want to give the expression `e` explicitly for `y` without giving a value for `x` we can write

```  subst C {y = e} eq cx
```

When constructing implicit function spaces the implicit argument can be omitted, so both expressions below are valid expressions of type `{A : Set} -> A -> A`:

```  \ {A} x -> x
\ x -> x
```

There are no restrictions on when a function space can be implicit. Internally, explicit and implicit function spaces are treated in the same way. This means that there are no guarantees that implicit arguments will be solved. When there are unsolved implicit arguments the type checker will give an error message indicating which application contains the unsolved arguments. The reason for this liberal approach to implicit arguments is that limiting the use of implicit argument to the cases where we guarantee that they are solved rules out many useful cases in practice.

Inductive data types and functions definitions

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

Pattern matching

Introduction

This page explains the reduction behaviour of functions defined by pattern matching. Consider the following two implementations of the less than function on natural numbers.

```  data Bool : Set where
true  : Bool
false : Bool

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

-- First implementation
_<1_ : Nat -> Nat -> Bool
zero  <1 suc m = true
suc n <1 suc m = n <1 m
_     <1 zero  = false

-- Second implementation
_<2_ : Nat -> Nat -> Bool
_     <2 zero  = false
zero  <2 suc m = true
suc n <2 suc m = n <2 m
```

Perhaps surprisingly (since the two implementations have the same non-overlapping clauses), _<1_ and _<2_ does not have the same reduction behaviour. For neutral `n` we have that `n <1 zero` does not reduce, whereas `n <2 zero` reduces to `false`. The reason for this is explained below.

Case tree equivalence

The set of defining equations for a functions are equivalent to a case tree, and the order of the equations determines which one. For `_<1_` the equivalent case tree is

```n <1 m = case n of
zero  -> case m of
suc m -> true
zero  -> false
suc n -> case m of
suc m -> n < m
zero  -> false
```

whereas for _<2_ it's

```n <2 m = case m of
zero  -> false
suc m -> case n of
zero  -> true
suc n -> n <2 m
```

Looking at the case tree it's clear that in the first case `n < zero` will not reduce to `false` for neutral `n`, but in the second case it will. Pattern matching always starts with the left-most constructor pattern in the first clause. For `_<1_` this is the first argument, whereas for `_<2_` it's the second argument.

Operational view

An alternative more operational way of looking at what's going on is the following. When reducing an application of a function by pattern matching the clauses will be tried one at a time, from top to bottom. For each clause the arguments will be matched against the corresponding patterns from left to right. If there is a mismatch the next clause is tried. If there is an inconclusive match (e.g. matching a neutral term against a constructor pattern) the application won't reduce. For `_<1_` we can't see whether `n` matches `zero` or not, so the reduction is suspended.

Berry's majority function

The reason for suspending reduction at the first sign of inconclusive matching is to keep the correspondence to a case tree. Consider Berry's majority function:

```data Bool : Set where
tt : Bool
ff : Bool

maj tt tt tt = tt
maj tt ff x  = x
maj ff x  tt = x
maj x  tt ff = x
maj ff ff ff = F
```

Here, all clauses are disjoint, but there is no case tree which delivers all equations as definitional equalities. Following the rules for pattern matching given above you'll discover that with this definition you get all but `maj x tt ff = x`.