One side of total functions is getting rid of functions that never return. Normally in strict languages we don't worry about this very much because when you find one you just fix it. So what's the big deal?
Well, one of the benefits of total functional programming is that expressions can be evaluated in any order, or even in parallel, as long the data dependencies between them are respected.
Consider:
f(x) = let y = f(x-1) in (if x = 0 then 0 else y*y)
In this case if the compiler decides to calculate y
first, as an eager language typically would, the function will loop forever. In a lazy language you would typically be okay - calculation of y
is deferred until it is needed, which it is not when x = 0
.
In a total functional programming system, this kind of recursion is not allowed because it is impossible to prove for any recursive function that it will never run forever.