Total functional programming

Total functional programming (also known as strong functional programming,

1. A restricted form of
   substructural recursion, or "strongly normalizing" as proven by abstract interpretation of code.^[3]
2. 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 ${\displaystyle \forall x\in \mathbb {N} .x\div 0=0}$ 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.^[2]

These restrictions mean that total functional programming is not

For example,

import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater

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

import Data.List (partition)

qsort x = qsortSub x x
-- minimum case
qsortSub []     as     = as -- shows termination
-- standard qsort cases
qsortSub (l:ls) []     = [] -- nonrecursive, so accepted
qsortSub (l:ls) [a]    = [a] -- nonrecursive, so accepted
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
                            -- recursive, but recurs on ls, which is a substructure of
                            -- its first input.
                         in qsortSub ls lesser ++ [a] ++ qsortSub ls greater

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 both

• Termination analysis

References