News for hackers. Stuff that matters.
Re:What is “Open Recursion”? by comex on Tuesday July 18, 2017 @08:25PM (#14801189)
Yeah, the post is a bit misleading. "Open recursion" is the OOP-like feature itself, not (as the post says) the extension you need to implement it.

What you need is the ability to implement recursive functions. That's not 'built in' to the lambda calculus, because there's no real concept of variable bindings, just functions that take arguments. In other words, you can't say "function x() { x(); }". In the untyped lambda calculus, that's no problem, because you can simulate it, e.g. by saying

    let x = (_x) => _x(_x);
    x(x);
Your implementation of open recursion uses a similar construct in 'mutualRecursion', as well as in the implementation of 'inc' (which calls 'set' passing 'set' itself as an argument).

But in the simply typed lambda calculus, that doesn't work, because 'x' would have an infinite type. For example, how would you write the type of x in TypeScript? Something like this:

    let x: (???) => whatever = (_x) => _x(_x);
where '???' is the type of x itself, so...

    let x: ((???) => whatever) => whatever = (_x) => _x(_x);

    let x: (((???) => whatever) => whatever) => whatever = (_x) => _x(_x);
...that doesn't work.

You could use a record/class type:

    class X {
        f: (X) => whatever;
        constructor(x) { this.x = x; }
    }
    let x = new X((_x) => _x.f(_x));
    x.f(x);
...but the desugaring of records into lambda calculus doesn't allow for that. (The use of X within its own type definition is recursive.)

You could use a generic function type:

    let x: <T>(arg: (T) => T) => whatever = (_x) => _x(_x);
but the simply typed lambda calculus has no generics.

But there's a more modest extension that can enable recursion, which is taking a fixed-point combinator (which in the untyped lambda calculus is just a function you can implement, e.g. as the Y combinator), and baking it into the typed lambda calculus as a primitive. Which is one of the things Pierce talks about in the book.

There are no comments on this comment yet.