Strong functional programming was proposed by David Turner, a founding father of modern functional programming (FP), as a better version of the functional programming paradigm realized today in Haskell. Where Haskell insists on purity, strong FP further insists that all functions terminate on all inputs. So strong FP goes beyond pure FP, to guarantee an even stronger property than purity, namely termination. In this post I will suggest a practical approach to Turner’s vision, based on monads.
Purity for a programming language means that there are no implicit side effects: whenever a function is called with the same arguments, it must return the same result. By an amazingly clever trick, we can represent impure functions like getTimeOfDay() — this function is so impure that it is a bug if it ever behaves purely — in the pure language Haskell. We view such functions as implicitly taking an extra input representing the entire state of the computer, and implicitly producing an updated version of that state as an extra output. And then we hide this fiction by using a monad, called IO in Haskell, so you never actually have access to the state. You just have various primitives like getChar :: IO Char. This is a character, but accessing it requires you to enter the IO monad, from which there is no way to escape. So in practice, Haskell programs have an impure layer within the IO monad, and then invoke various pure functions that are not in the IO monad. This is because pure code can be injected into the IO monad using the return function of the monad (which does exactly that: bring pure things into IO).
Now, in Turner’s lovely paper linked above, which I quite recommend, there are arguments for the value of strong FP. But Turner does not explain how to make this practical, and maybe is not even thinking about that, since he worries rather a bit about the fact that the restriction to terminating programs only means that a strong FP language will not be Turing complete. But I would like to point out that for practicality, we need to take the same path that Haskell took for purity. Haskell is pure, but uses monads to allow impure computations. What we need for a practical strong FP language is a language that is pure and enforces termination, but can also accommodate — and here I definitely propose monads as the way to go — impure and possibly non-terminating computation.
So I imagine a world where there is a monad, maybe called GenRec, for possibly nonterminating computation, and code from the terminating part of the language can be injected into that monad using its return function. And GenRec computations could be lifted into IO, too. So we can play the same game that Haskell does, but with two special monads (IO and GenRec) instead of one (just IO).
And while we are thinking this way, about teasing apart the structure of the language using monads, I also am wondering about a monad for possibly type-unsound computation. In OCaml, for example, there is this somewhat infamous Obj.magic which lets you change the type of an expression to anything you want. This could lead to segmentation faults and other disasters. But yet it is there, and apparently is useful in some cases, for example when compiling languages like Coq, with a more powerful type system, to tell OCaml’s compiler to just trust us that something is ok.
So what about an ultimate monad called something like Unrestricted (name too long, ok), that allows unsound casts, general recursion, and IO.
Now your language is accommodating all kinds of programs, and providing a range of guarantees. This is just taking the core awesome idea of Haskell, and expanding it both towards more safe (i.e., the terminating part of the language) and also less (i.e., unsound casts).
A final parting shot on this: with layers of monads, one thinks immediately of monad transformers, and then maybe thinks the idea will be too complicated. But I am exploring currently a language design, which I am intending to head in the direction I have just outlined, where we use subtyping to keep some coercions implicit. This could mean that the super-annoying liftings that are needed with monad transformers could be elided completely using subtyping. My language design is already committed to subtyping for one its central features (a type-based form of terminating recursion), and so investigating subtyping as a way to make programming with layers of monads more workable seems very natural.
Thanks for reading!
QA9 