Totality

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

Introduction

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.

Importance of totality

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

Another example:

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.

Ensuring totality

To make sure that all computations are total, a few checks are performed in Agda:

1. Type checking
2. Coverage checking
3. Termination checking
4. Strict positivity of constructors checking
5. Guardedness checking in coinductive programs

The first 3 positions are the most essential ones, the rest can be skipped on first reading.

Type checking

Type checking rules out run-time errors like applying a function that expects a Nat to a Bool.

Coverage checking

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

then evaluating 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).

Termination checking

Not all recursive functions are permitted - Agda accepts only these recursive schemas that it can mechanically prove terminating.

Primitive recursion

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

Both plus and 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 suc n). 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.

Structural recursion

In some systems 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 ack below).

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)

In ack either the first argument decreases or it stays the same and the second one decreases. This is the same as a lexicographic ordering.