Total functional programming (also known asstrong functional programming,^[1] to be contrasted with ordinary, orweakfunctional programming) is aprogramming paradigm that restricts the range of programs to those that areprovably terminating.^[2]

Termination is guaranteed by the following restrictions:

1. A restricted form ofrecursion, which operates only upon 'reduced' forms of its arguments, such asWalther recursion,substructural recursion, or "strongly normalizing" as proven byabstract interpretation of code.^[3]
2. Every function must be a total (as opposed topartial) 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${\displaystyle \mathrm{\forall }x\in \mathbb{N}.x÷0=0}$ for division); adding another argument to specify the result for those inputs; or excluding them by use of type system features such asrefinement types.^[2]

These restrictions mean that total functional programming is notTuring-complete. However, the set of algorithms that can be used is still huge. For example, any algorithm for which anasymptotic 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.

For example,quicksort is not trivially shown to be substructural recursive, but it only recurs to a maximum depth of the length of the vector (worst-case time complexityO(n²)). A quicksort implementation on lists (which would be rejected by a substructural recursive checker) is, using Haskell:

importData.List(partition)qsort[]=[]qsort[a]=[a]qsort(a:as)=let(lesser,greater)=partition(<a)asinqsortlesser++[a]++qsortgreater

To make it substructural recursive using the length of the vector as a limit, we could do:

importData.List(partition)qsortx=qsortSubxx-- minimum caseqsortSub[]as=as-- shows termination-- standard qsort casesqsortSub(l:ls)[]=[]-- nonrecursive, so acceptedqsortSub(l:ls)[a]=[a]-- nonrecursive, so acceptedqsortSub(l:ls)(a:as)=let(lesser,greater)=partition(<a)as-- recursive, but recurs on ls, which is a substructure of-- its first input.inqsortSublslesser++[a]++qsortSublsgreater

Some classes of algorithms have no theoretical upper bound but do 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 bothstrict evaluation andlazy evaluation result in the same behaviour, in principle; however, one or the other may still be preferable (or even required) for performance reasons.^[4]

In total functional programming, a distinction is made betweendata andcodata—the former isfinitary, while the latter is potentially infinite. Such potentially infinite data structures are used for applications such asI/O. Using codata entails the usage of such operations ascorecursion. However, it is possible to doI/O in a total functional programming language (withdependent types) also without codata.^[5]

BothEpigram andCharity could be considered total functional programming languages, even though they do not work in the wayTurner specifies in his paper. So could programming directly in plainSystem F, inMartin-Löf type theory or theCalculus of Constructions.

• Termination analysis

• Programming paradigms
• Functional programming
• Proof assistants

• Articles with short description
• Short description is different from Wikidata