Total Functional Programming

TotalFunctionalProgramming is FunctionalProgramming but only using 'total' functions.

The difference between a 'total' function and a 'partial' function is that, in its domain, a total function will never diverge. Or, put another way, it will always terminate. Obviously TotalFunctionalProgramming is not TuringComplete... at least not all by itself. If used in a GeneralPurposeProgrammingLanguage, one would usually use another layer (perhaps a procedural layer, or in a ProcessModel layer) to achieve TuringComplete operation.

Examples are CharityLanguage and Epigram language.

TotalFunctionalProgramming greatly simplifies type analysis of the language and many other properties (e.g. equality between codata types), and allows a great many optimizations. With divergence out of the picture, one can guarantee that lazy, strict, lenient (parallel), partial, and other evalution strategies will always reach the same result. Thus, the decision becomes strictly one of optimization. Given that analysis is easier, optimizers are also much easier to verify automatically (e.g. using Coq).

Any terminating function can be written in TotalFunctionalProgramming. If you can bound the number of steps, you could always set an integer to that bound and count down on that integer to prove termination... brute force, kludgy, but it works. The thing is that not every algorithm can be written conveniently or 'elegantly', especially given restrictions common to the design (such as using primitive recursion rather than allowing Coq-powered theorem proofs of termination).

Fortunately, ~75% of everything we ever write in FunctionalProgramming is PrimitiveRecursive in first or second order, and much of the rest can readily be adapted. Primitive support for transforming Natural numbers from the 's(s(s(s(s(0)))))' PeanoArithmetic representation into the 'cons(1 cons(0 cons(1 nil)))' binary representation does help quite a bit in optimizing various mathematics algorithms.

TotalFunctionalProgramming does not preclude CollectionOrientedVerbs or support for 'sets' as a primitive type, so long as those operations are guaranteed to terminate (usually they are, since sets are finite). TotalFunctionalProgramming does support 'infinite' codata, but not the ability to filter it (unless you can somehow prove that there are a finite number of steps between each positive match).

Writing something like Ackermann's function does become a bit of a challenge. However, while the former is an exercise worth pursuing, the latter is a pretty complex and difficult to prove correct in a normal FunctionalProgramming language. It is for tasks like writing up parsers that it becomes easy to appreciate knowing the function will terminate.

The term "total functional programming" was coined by DavidTurner in his 2004 paper "Total Functional Programming". The paper is available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.5271.

An earlier (1995) version of the same paper used the term ElementaryStrongFunctionalProgramming, also known simply as StrongFunctionalProgramming. The earlier paper is available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.8766.

As already mentioned there are some efficient algorithms that are not easily expressed with total functions or in a functional style at all. For an example see SameFringeProblem.

How do you justify that example? The HaskellLanguage answer to SameFringeProblem is the cleanest, most easily expressed implementation of all. TotalFunctionalProgramming allows lazy, lenient, strict, etc. evaluation - all lead to the same answer, so more options are available. More generally, I agree with your statement... there are many efficient algorithms not expressed efficiently with FunctionalProgramming in general (including TFP), especially those that involve manipulating state and pointers. However, the particular example you provided is not a clear indicator of this at all.

If you're stuck with strict evaluation, then I suppose you'd have difficulty efficiently implementing the SameFringeProblem in TFP and functional. TotalFunctionalProgramming typically allows definition of codata, but TFP implemented by enforcing functions be PrimitiveRecursive cannot recurse over the resulting codata, and so you must keep one tree in its normal representation and fold over it monadically.

 define Tree    = fun: A => type T of tree(T T)|leaf(A)        ;; structural type def. for tree
 define FStream = fun: A => type S of ~(type yield(A S)|done)  ;; structural type def, potentially terminating stream 

 ;; tree iterator is simple 'iter(a:A b:TREES)', with 'b' being 'stack' of trees. Generalizes as a depth-first search.
 define MakeTI = fun F: leaf(A)   => {fun: TREES => iter(A TREES)}
                      | tree(L R) => {fun: TREES => {F L cons(R TREES)}}
 ;; convert a tree iterator to a finite stream, ~(unfold). Could be generalized into a HOF for many types.
 define TItoFS = fun U: iter(A nil)       => ~(yield(A ~(done)))
                      | iter(A cons(L R)) => ~(yield(A {U {MakeTI L R}}))

 ;; chaining the codata as a 'world' state. Generalizes into a monad.
 define CBase = fun C: leaf(A) =>  fun: ~(yield(B S)) => ({equal A B} S)
                                      |  _            => (false ~(done))   
                     | tree(L R) => fun: S =>
                         let (V1 S1) = {C L S} 
                         in  case V1 of false => (false ~(done))
                                      | true  => {C R S1} 

 ;; efficient, strict-evaluation answer to SameFringeProblem, in TotalFunctionalProgramming
 define SameFringe = fun: T1 => fun: T2 =>
   let  (Rf Sf) = {CBase T1 {T1toFS {MakeTI T2 nil}}} 
   in {and Rf {equal ~(done) Sf}}   ;; equal if CBase returns true and there isn't any leftover element in Sf

Difficult to express? Yes, but generalizing monads would help a lot. So would some syntactic sugar. And, of course, one could simply favor the lazy implementation.

CategoryFunctionalProgramming