Total functional programming

Total functional programming (also known as strong functional programming [This term is due to: Citation|last1=Turner|first1=D.A.|author-link=David Turner (computer scientist)|contribution=Elementary Strong Functional Programming|title=First International Symposium on Functional Programming Languages in Education|date=December 1995|journal=Springer LNCS|volume=1022|page=1–13.] , to be contrasted with ordinary, or "weak" functional programming) is a programming paradigm which restricts the range of programs to those which are provably terminating.

Termination is guaranteed through a restricted form of recursion, which operates only upon ‘reduced’ forms of its arguments. One such form is Walther recursion. In addition, every function must be a total (as opposed to partial) function. That is, it must have a definition for everything inside its domain. This may lead to unexpected or arbitrary definitions such as $forall\; x\; subset\; mathbb\{N\}.\; x\; div\; 0\; =\; 0$

These restrictions mean that total functional programming is not Turing-complete. However, the set of algorithms which can be used is still huge. For example, any algorithm which has had an asymptotic upper bound calculated for it can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument which is decremented upon each iteration or recursion.

Another outcome of total functional programming is that there is no longer a separation between strict evaluation and lazy evaluation.

Total functional programming must necessarily also make a distinction between data and codata—the former is finitary, which the latter is potentially infinite. Such potentially infinite data structures are needed for applications such as I/O. Using codata entails the usage of such operations as corecursion.

Both Epigram and Charity could be considered total functional programming languages, even though they don't work in the way Turner specifies in his paper. So could programming directly in plain System F, in Martin-Löf type theory or the Calculus of Constructions.

Footnotes

References

*