4 ms·

I'm a little confused by the summary. To me it looks like he's showed that you can simulate open recursion with only structures and functions. If it's because

I'm a little confused by the summary. To me it looks like he's showed that you can simulate open recursion with only structures and functions. If it's because doing so requires forward-declarations/hoisting/reassignment, here[1] is an implementation in JavaScript that has only a single `let` statement, for the counter itself. [1] https://jsfiddle.net/n2c3s7r5/ https://jsfiddle.net/n2c3s7r5/

munificent 9y ago
I could be wrong, but I think your mutualRecursion() function is a multi-parameter version of the Y combinator, which is the classic way of introducing recursion to a language that doesn't natively support it. If so then, yes, that works.
- clusmore 9y ago
  > but I think your mutualRecursion() function is a multi-parameter version of the Y combinator Yes, exactly. I've created a fork [1] where I replace the multiple-parameter Y combinator with a single-parameter kind that operates on what is effectively a vtable. [1] https://jsfiddle.net/9ump7bt5/1/ https://jsfiddle.net/9ump7bt5/1/
wickawic 9y ago
Agreed, but I think the distinction is that the original book was talking about language design. Since languages are Turing complete we can always implement the features of one in another, but it stands that open recursion is not a feature of his Dart subset. It would certainly be a stretch to call a language OO just because you can replicate OO features from first principles!
comex 9y ago
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.

munificent 9y ago

I could be wrong, but I think your mutualRecursion() function is a multi-parameter version of the Y combinator, which is the classic way of introducing recursion to a language that doesn't natively support it. If so then, yes, that works.

clusmore 9y ago
> but I think your mutualRecursion() function is a multi-parameter version of the Y combinator Yes, exactly. I've created a fork [1] where I replace the multiple-parameter Y combinator with a single-parameter kind that operates on what is effectively a vtable. [1] https://jsfiddle.net/9ump7bt5/1/ https://jsfiddle.net/9ump7bt5/1/

wickawic 9y ago

Agreed, but I think the distinction is that the original book was talking about language design. Since languages are Turing complete we can always implement the features of one in another, but it stands that open recursion is not a feature of his Dart subset. It would certainly be a stretch to call a language OO just because you can replicate OO features from first principles!

comex 9y ago

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.