Total Functions
Functions are total if, for all inputs, they terminate with a well-typed result.
Idris cannot automatically determine if this is true for the general case (No program can due to the halting problem) However, in many cases Idris can determine a function is total by using heuristics like the following:
- All calls are themselves to total functions.
- If there is a recursive call then there must be a decreasing argument that converges toward a base case.
If we require a function to be total but Idris cannot automatically determine that, we may have to provide a proof.
Alternatively there is a notion of total for the dual of this for infinite data types, see below.
| For example, Idris knows that this is total because the RHS always involve smaller numbers. Idris code here | ||| Recursive definition of Fibonacci. fibRec : Nat -> Nat fibRec Z = Z fibRec (S Z) = S Z fibRec (S (S k)) = fibRec (S k) + fibRec k |
x
||| Accumulator for fibItr. Parameters: ||| * nth Fibonacci number ||| * Fibonacci number before last ||| * last Fibonacci number fibAcc : Nat -> Nat -> Nat -> Nat fibAcc Z a _ = a fibAcc (S k) a b = fibAcc k b (a + b) ||| Iterative definition of Fibonacci. fibItr : Nat -> Nat fibItr n = fibAcc n 0 1 |
Co Patterns
To be total it must produce a non-empty finite prefix of a well-typed infinite result in finite time.
discussion on forum here
fib : Stream Int
fib = fib' 1 2
where
fib' : Int -> Int -> Stream Int
fib' p1 p2 = p1 :: fib' p2 (p1 + p2) |
| Made up Agda-like syntax: |
record Stream a where
head : Stream a -> a
tail : Stream a -> Stream a |
