Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm that restricts the range of programs to those that are provably terminating.
Termination is guaranteed by the following restrictions:
- A restricted form of recursion, which operates only upon ‘reduced’ forms of its arguments, such as Walther recursion, substructural recursion, or "strongly normalizing" as proven by abstract interpretation of code.
- Every function must be a total (as opposed to partial) function. That is, it must have a definition for everything inside its domain.
- There are several possible ways to extend commonly used partial functions such as division to be total: choosing an arbitrary result for inputs on which the function is normally undefined (such as for division); adding another argument to specify the result for those inputs; or excluding them by use of type system features such as refinement types.
These restrictions mean that total functional programming is not Turing-complete. However, the set of algorithms that can be used is still huge. For example, any algorithm for which an asymptotic upper bound can be calculated (by a program that itself only uses Walther recursion) can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument decremented on each iteration or recursion.
Some classes of algorithms without a theoretical upper bound, but which have a practical upper bound (for example, some heuristic-based algorithms) can be programmed to "give up" after so many recursions, also ensuring termination.
Another outcome of total functional programming is that both strict evaluation and lazy evaluation result in the same behaviour, in principle; however, one or the other may still be preferable (or even required) for performance reasons.
In total functional programming, a distinction is made between data and codata—the former is finitary, while the latter is potentially infinite. Such potentially infinite data structures are used for applications such as I/O. Using codata entails the usage of such operations as corecursion. However, it is possible to do I/O in a total functional programming language (with dependent types) also without codata.
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.
Famous quotes containing the words total, functional and/or programming:
“Unlike Descartes, we own and use our beliefs of the moment, even in the midst of philosophizing, until by what is vaguely called scientific method we change them here and there for the better. Within our own total evolving doctrine, we can judge truth as earnestly and absolutely as can be, subject to correction, but that goes without saying.”
—Willard Van Orman Quine (b. 1908)
“Indigenous to Minnesota, and almost completely ignored by its people, are the stark, unornamented, functional clusters of concrete—Minnesota’s grain elevators. These may be said to express unconsciously all the principles of modernism, being built for use only, with little regard for the tenets of esthetic design.”
—Federal Writers’ Project Of The Wor, U.S. public relief program (1935-1943)
“If there is a price to pay for the privilege of spending the early years of child rearing in the driver’s seat, it is our reluctance, our inability, to tolerate being demoted to the backseat. Spurred by our success in programming our children during the preschool years, we may find it difficult to forgo in later states the level of control that once afforded us so much satisfaction.”
—Melinda M. Marshall (20th century)