What is "Total Functional Programming"?

Question

Wikipedia has this to say:

Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm which restricts the range of programs to those which are provably terminating.

and

These restrictions mean that total functional programming is not Turing-complete. However, the set of algorithms which can be used is still huge. For example, any algorithm which has had an asymptotic upper bound calculated for it can be trivially transformed into a provably-terminating function by using the upper bound as an extra argument which is decremented upon each iteration or recursion.

There is also a Lambda The Ultimate Post about a paper on Total Functional Programming.

I hadn't come across that until last week on a mailing list.

Are there any more resources, references or any example implementations that you know of?

Answer 1

If I understood that correctly, Total Functional Programming means just that: Programming with Total Functions. If I remember my math courses correctly, a Total Function is a function which is defined over its entire domain, a Partial Function is one which has "holes" in its definition.

Now, if you have a function which for some input value v goes into an infinite recursion or an infinite loop or in general doesn't terminate in some other fashion, then your function isn't defined for v, and thus partial, i.e. not total.

Total Functional Programming doesn't allow you to write such a function. All functions always return a result for all possible inputs; and the type checker ensures that this is the case.

My guess is that this vastly simplifies error handling: there aren't any.

The downside is already mentioned in your quote: it's not Turing-complete. E.g. an Operating System is essentially a giant infinite loop. Indeed, we do not want an Operating System to terminate, we call this behaviour a "crash" and yell at our computers about it!

Answer 2

Charity is another language that guarantees termination:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Hume is a language with 4 levels. The outer level is Turing complete and the innermost layer guarantees termination:
http://www-fp.cs.st-andrews.ac.uk/hume/report/