2008
(Non-)Total Functional Programming
I’ve been getting back into language design again. (I haven’t written anything about it since August!)
Not too long ago I was introduced to Total Functional Programming. The paper is very interesting, and at first, the concept sounds great. Increase the ease of proofs of properties of your code at the expense of Turing-completeness. Who needs Turing-completeness anyway.
But after reading some comments on Lambda the Ultimate, something occurred to me. Maybe removing infinite looping, in an attempt to remove a certain kind of partial function — those that never return — is acceptable. But removing partial functions completely is not acceptable (to me).
To implement division, for example, you’d have to modify the definition of it, or change the type to make it impossible to type-check with a zero divisor. But in general, the compiler can’t prove that a runtime value is non-zero, so this forces the programmer to explicitly handle the case all the time. Maybe that’s desirable in some places, but is it always? I’m not sure.
What I take away from this is that, (1) partial functions won’t go away completely and (2) we have to accept some kind of undefined exceptional value.
Both could be eliminated by making your types über-complicated. But I think that’s the wrong way to go. An intuitive type for division is int -> int -> int or perhaps Num n => n -> n -> n. But not something artificial just to make the function total like Num n, NonZero nz => n -> nz -> n.
