The information on this page is likely to be out of date. See the official user manual for information on the latest version of Agda.
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
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)
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.