# 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 (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 `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.

## References

1. Conor McBride - First-order Unification by Structural Induction