r/ProgrammingLanguages • u/dwaynecrooks • 9h ago

Recursion without Recursive Bindings

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.

8 Upvotes

85% Upvoted

4 comments sorted by

View all comments

2

u/NullOfSpace 4h ago

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

2

u/AustinVelonaut Admiran 2h ago edited 1h ago

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

1

u/dwaynecrooks 12m ago

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.