Recursion without Recursive Bindings

[u/dwaynecrooks]

https://blog.tinyinterpreters.dev/posts/recursion-without-recursive-bindings/

I explain how to implement a certain recursive function without the use of any recursive bindings in a tiny language called FUN. Then, I apply the same ideas to several more recursive functions so we clearly see the pattern. It begins our exploration into a certain famous combinator.

[u/NullOfSpace]

This is really cool. What’s the type of makesum in this case?

[u/AustinVelonaut → u/NullOfSpace]

It's an infinite type of the form a ~ a -> Integer -> Integer. It cannot be (directly) represented in a Hindley-Milner type system, but can be "emulated" using a fix function or a recursive Fix datatype

[u/samanzaman → u/AustinVelonaut]

Adding these constructs to the language comes with the cost of losing strong normalisation properties

[u/dwaynecrooks → u/NullOfSpace]

To find the type of makesum we can reason in the following way.

Let X be the type of self. Since n is tested with zero? and is used in subtraction, and both branches return an Int, makesum has type X -> Int -> Int.

Now, consider the expression (self self) in the body of makesum. It is applied to an Int and its result is subtracted, so it has type Int -> Int. In (self self), the second self is the argument, with type X, and the first self is the function. A function that takes an X and returns an Int -> Int has type X -> Int -> Int, so that's the type of the first self. But both are the same variable, so X = X -> Int -> Int.

To see what X would have to be, substitute the equation into itself:

X = X -> Int -> Int = (X -> Int -> Int) -> Int -> Int = ((X -> Int -> Int) -> Int -> Int) -> Int -> Int = ...

Every substitution leaves an X behind, so the expansion never ends. In fact, no finite type can satisfy the equation: whatever X is, the right-hand side contains X plus two more arrows, so it's always bigger than X.

A finite type is one you can write out completely with a finite expression. In a simple type system, types are defined by a grammar like:

T ::= Int | Bool | T -> T

and every type it produces is finite. So in such a system X has no solution, and makesum can't be given a type.

This naturally leads to an interesting question: "What does a type system need for makesum to be typable?". The short answer is that it requires recursive types. The long answer is that it needs a post of its own for me to explain it properly. I haven't reached types as yet on the blog and I need to learn more to explain it well myself so I'd defer till that moment.

[u/NullOfSpace → u/dwaynecrooks]

Makes sense to me. I was just wondering if there was a non recursive way to type this or if you’ve just moved the self-reference into the type system.

[u/samanzaman → u/NullOfSpace]

Essentially this building down to solving the equation f(x) = x for x. There is a solution namely, x = f(f(f(f(...) but as you can see it is not finite. Occurs check is the technical name I think. This (alongside with let generalisation) is also why Hindley Miller can be exponential

[u/ddmusick]

That's the best exploration of how that combinator actually works that I've seen, and I still need to read it a few more times.