Recursion Schemes

Motivation

Ensuring that the computations which occur in types actually terminate is among the most central design problems in dependently typed languages. If a type-valued computation can be ⊥ (that is, bottom, the value of non-terminating computations), then that will render the language unsound as a logic, meaning we can't really trust any of the proofs the language gives us, which is after all the entire point of such an expressive type system. In languages such as Haskell, bottom inhabits every type. What this means in practice is that Haskell's type system is not expressive enough to distinguish between partial and total functions. But, because we want the types in our language to have a real semantics, it is desirable if at least type-valued computations operate withing the regime of total functional programming.

We have a few options in how we want to address this problem. The first is to simply decide you don't care about logical soundness at all. This is a valid approach and is the one Cayenne and (I believe) Dependent Haskell take. If we do want to ensure terms which appear in type-level computations always terminate, there is a very blunt approach we can take which is barely more complex than doing nothing at all: for any type-valued computation, attach an implicit timer that stops execution of the computation after some n {seconds, minutes, CPU cycles, levels of recursion, &c.} and throws an error if that limit is exceeded.

However, most designers of dependently typed languages do care about their proofs meaning something and so employ a totality checker. This is true of Coq, Agda, Idris, Epigram, F*, and others. For obvious reasons, soundness is especially important for proof assistants. Abel's foetus totality checker is the ur-example, but its descendants all work on similar principles. Of course, by necessity any termination checker must be conservative since we can't solve the halting problem (simpliciter) but that doesn't mean we can't decidably detect useful subsets of the set of terminating programs. In essence, the general method is to determine whether for each recursive call that the "accumulator" argument(s) gets "smaller" (for some definition thereof). This is called structural recursion, and is relatively straightforward to check for, though somewhat restrictive. There are useful generalizations of structural recursion like Walther Recursion which relax these constraints a bit.

In Idris, totality is not a part of a functions type; notionally, totality stands apart. In my opinion, this complicates the ontology of the language.

In general, I am suspicious of "best effort" algorithms being embedded into the semantics of a language. This is a big reason why I am suspicious of type inference, because unless it is complete and every type can be assigned a principle type (I would note this is not the case even in SML, because of records), then whether a given program will compile will depend on the state of various imprecise heuristics. Barring breaking changes in the language specification itself, a given program which obeys the semantics of the language should always compile on any conforming compiler. In this scenario, we can either give up on enumerating any precise set of programs that are accepted by conforming compiler, or reify a particular set of heuristics as being a part of the language specification itself. Neither option is desirable.

Recursion Schemes

With all that motivation out of the way, what exactly are recursion schemes? In essence, recursion schemes allow a programmer to separate out the mechanism of recursion from (as the authors of the Yaya library put it) the "business logic". One helpful way to think of them, is as a way of transforming open-form expressions into closed-formed ones. For example, the fold function, familiar to all functional programmers, though conceptually recursive, contains no explicit recursion from the programmer's perspective.

To understand how this works in practice, let's consider two different SML examples. (Don't worry if you don't know SML, the way these functions work should be obvious)

fun fib n =
    if n <= 1 then 1 else fib(n - 1) + fib(n - 2)

fun fact n =
    if n <= 1 then 1 else n * fact(n - 1)

We can see that the form of these two functions, which calculate the nth item in the fibonacci sequence and n factorial respectively, have a lot of similarity. In fact, both functions are identical save for the else leg. In fact, we can factor out the recursion altogether:

fun scheme f n =
    if n <= 1 then 1 else f (scheme f, n) (* "scheme f" is a curried or partially applied here *)

val fib_s = scheme (fn (g, n) => g(n - 1) + g(n -2))
val fact_s = scheme (fn (g, n) => n * g(n -1))

The function scheme is an example of a recursion scheme(though a bit of a contrived one). Neither is it a particularly useful one, because nothing about scheme ensures termination occurs. Nevertheless, the example should be instructive. For a more in depth treatment of recursion schemes, Manfred von Thun's language Joy makes prodigious use of them.

We can improve our recursion scheme by further restricting its form and ensuring that the accumulator decreases in value:

fun test n = if n < 0 then n else raise Fail "not negative";

fun term f n =
    if n <= 1 then 1 else f ((fn d => term f (n + (test d))), n)

val fib_t = term (fn (self, _) => self(~1) + self(~2))
val fact_t = term (fn (self, n) =>  n * self(~1))

Instead of unrestricted control over what value is passed to the next layer of recursion, the term scheme restricts this to the accumulator n plus some value. Moreover, we call the test function to ensure that this value is actually negative so that the accumulator actually decreases in size.

Effects

In the context of a dependently typed language, effects are a very natural way to isolate non-terminating computations from places where we don't want them to appear (e.g. types). In general, the effect of a computation is the union of the effects of all of the computations it encloses (effect polymorphism complicates this a bit, but we can ignore that for the sake of this discussion). However, if we want to treat non-termination (usually termed divergence in this context, or given the effect name div) as an effect, as we should, and use a totality checker to determine where divergence occurs, this means that we have to reckon divergence, qua effect, differently from all other effects.

Now, one might say that this is in fact not a problem, and that it's to be expected that primitive effects receive different treatment from user-defined effects. I think this is a perfectly credible decision, but I, personally, nearly always prefer to flatten the ontology of my languages as much as possible. In many ways, Anselm's

To be sure, that the div effect is conferred on a function as a consequence of binding (more precisely a function thunk, we are working with call-by-push-value after all) with rec instead of def (what other languages call let) does mean that div receives syntactic special treatment. But this, I think, is less "ontologically" pernicious than other forms of special casing because it really is just syntax sugar: at the Gaunilo level, Anselm's rec elaborates into the application of a general fixed point combinator. In languages where fixed point combinators cannot be typed (such as a/the simply-typed lambda calculus), we can choose to augment that language "by fiat" with such a combinator and win back Turing completeness in the process. Indeed, fix is primitive in Gaunilo and comes with the div effect.

Performance

Built-in recursion schemes have another benefit. Recursion is to functional programming what iteration is to imperative programming. Whatever elegance recursion as a means of expressing iteration may have, that does not necessarily translate into equivalent performance. Indeed, many functional languages such as Scheme mandate proper tail-call elimination.

Since Anselm's basic recursion schemes are built into the language as primitives, it is more straightforward for the language specification to mandate particular implementation strategies. In the case of Scheme, requiring tail call elimination is (in my opinion) semantically suspect because it entails the particulars of implementation leaking through the abstraction of the language itself.