See the official user manual for the most up-to-date version of the information on this page.
This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0
Table of contents
- Importance of totality
- Ensuring totality
- Detailed information
Agda is a total language, so all computations must terminate and return a value without any run-time errors. This means that effectively not all programs that can be defined in (for instance) Haskell or ML can defined in Agda. We also say that in a total language all computations are strongly-normalizing.
Knowing that your programs will always evaluate successfully is a nice thing to have by itself, but there is a deeper reason.
In a dependently typed language, computations may be required not only at run-time, but also during type checking. If arbitrary (i.e. non-terminating) computations were allowed, then the typechecking would become undecidable - the type checker would loop from time to time.
Examples. Suppose that
foo : Bool and evaluation of
foo never ends.
This program would loop the type checker (
_==_ is the usual propositional equality):
fooIsTrue : foo == true fooIsTrue = refl
getType : Bool -> Set getType true = Nat getType false = Bool nat? : getType foo nat? = 5
We need to check if
getType foo == Nat, but to do that we need to fully evaluate
foo - but we assumed that this would never end.
To make sure that all computations are total, a few checks are performed in Agda:
- Type checking
- Coverage checking
- Termination checking
- Strict positivity of constructors checking
- Guardedness checking in coinductive programs
The first 3 positions are the most essential ones, the rest can be skipped on first reading.
Type checking rules out run-time errors like applying a function that expects a
Nat to a
Coverage checking rules out partial functions - i.e. functions defined by pattern matching with some cases omitted.
For example, if this was allowed
data Color : Set where Red Green Blue : Color flipColor : Color -> Color flipColor Red = Green flipColor Green = Red -- no pattern for Blue
flipColor Blue would result in a run-time error.
(Agda rejects this definition with "Incomplete pattern matching for flipColor".)
Therefore, when defining a function by pattern matching in Agda one must cover all cases (more precisely, all cases that are correct with respect to types).
Not all recursive functions are permitted - Agda accepts only these recursive schemas that it can mechanically prove terminating.
In the simplest case, a given argument must be exactly one constructor smaller in each recursive call. We call this scheme primitive recursion. A few correct examples:
data Nat : Set where zero : Nat suc : Nat -> Nat plus : Nat -> Nat -> Nat plus zero m = m plus (suc n) m = suc (plus n m) natEq : Nat -> Nat -> Bool natEq zero zero = true natEq zero (suc m) = false natEq (suc n) zero = false natEq (suc n) (suc m) = natEq n m
natEq are defined by primitive recursion.
The rec. call in
plus is OK because
n is a subexpression of
suc n (so
n is structurally smaller than
So every time plus is recursively called the first argument is getting smaller and smaller.
Since a natural number can only have a finite number of suc constructors we know that plus will always terminate.
natEq terminates for the same reason, but in this case we can say that both the first and second arguments of natEq are decreasing.
In some systems (i.e. Coq) primitive recursion is the only allowed scheme. Agda's termination checker is less restrictive - it allows structural recursion.
This means that we require recursive calls to be on a (strict) subexpression of the argument (see
fib below) -
this is more general that just taking away one constructor at a time.
It also means that arguments may decrease in an lexicographic order - this can be
thought of as nested primitive recursion (see
Example (Fibonacci's numbers):
fib : Nat -> Nat fib zero = zero fib (suc zero) = suc zero fib (suc (suc n)) = plus (fib n) (fib (suc n))
Example (Ackermann's function)
ack : Nat -> Nat -> Nat ack zero m = suc m ack (suc n) zero = ack n (suc zero) ack (suc n) (suc m) = ack n (ack (suc n) m)
ack either the first argument decreases or it stays the same and the second one decreases.
This is the same as a lexicographic ordering.
- Conor McBride - First-order Unification by Structural Induction