Total functional programming

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. 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 complexity O(n2)). A quicksort implementation on lists (which would be rejected by a substructural recursive checker) is, using Haskell: import Data.List (partition) qsort [] = [] qsort [a] = [a] qsort (a:as) = let (lesser, greater) = partition (