The Potential of Total Functional Programming

A total functional programming language is a language where programs are guaranteed to terminate in a finite amount of time; that is, they will neither crash, nor run into infinite loops.

To make a total functional programming language is actually not that complex—the key to totality is what to omit rather than what to include.

• You start by defining a typed language, where all functions are total, ie they are defined for all inputs. A common example of a non-total function is division, because division is undefined when the denominator is zero.
• You omit I/O (as the outside world is finicky and non-deterministic), or make I/O happen “outside”¹ the program as in Haskell.
• Crucially, you omit support for recursive definitions in the type system.²

The last point might sound like heresy—isn’t recursion foundational to functional programming? While it’s possible to allow limited forms of recursion, with general recursion it’s trivial to write non-terminating programs (just write a function that calls itself), so it ruins our termination guarantee. While this might sound awfully limiting , remember that we can still have foundational functions like reduce in our language—we just can’t define them inside the program itself.

What’s the point?

We have a programming language that, if it type checks, is guaranteed to terminate. Of course, there’s also the added bonus of knowing that your programs will never crash, but this is just the beginning:

• The termination guarantee opens up new use cases for functional programming; for example, instead of clients and server communicating via a REST API, the client could send a complete program to be executed on the server. Since the program will always halt and has limited access to the system you don’t have to worry about a program using up all your CPU or deleting your hard drive.³ Imagine never having to write an internal CRUD service ever again!
• Totality also means that we can evaluate parts of our program at compile time—this enables us to use more advanced type systems, like dependent types
• Just as totality enables more advanced type systems, it also allows us to perform more aggressive optimizations; essentially, we can inline the entire program. Coupled with rewrite rules, this could allow us to eg write a functional query language with a query planner

Further reading

• Dhall is a total functional programming language designed for configuration management. The fact that it’s total means it’s safe to run on a server without having to worry about an infinite loop bringing the system down.
• Morte: an intermediate language for super-optimizing functional programs introduces Morte, an experimental intermediate language that uses total functional programming to rewrite programs into optimal forms.
• If you’re curious about dependent types, check out Idris and Lean!