The Approved Proposal

Okay, so I got the proposal approved a few weeks ago, but I have been too busy doing productive work to write about it here. I'll summarize the proposal in this post. To write a program exclusively with total functions, some restriction on recursion must be enforced. In my system, this restriction can be summarized as that recursion must be syntactically structural. This means that the argument of a recursive call must have been bound by a pattern-matching deconstruction of the actual parameter. My proposal is to implement this rule, along with a few other necessary details, as a GHC language extension, to provide a total standard library, and to write certain example programs in the total discipline. I will then attempt to draw conclusions about what further work is necessary to make total functional programming practical. Of course, there are many details that I've left out here. It's especially interesting to see how the concept of syntactic structural recursion must be expanded to deal with functions of higher arity, higher-order functions, and mutual recursion.