←back to thread

Baking the Y Combinator from Scratch

(the-nerve-blog.ghost.io)
123 points mprast | 2 comments | | HN request time: 0.018s | source
Show context
mkagenius ◴[] No.43637919[source]
Is there a technique to remember this? I will understand it today and forget after a few weeks.
replies(4): >>43638317 #>>43638319 #>>43639364 #>>43639727 #
crdrost ◴[] No.43639727[source]
Yes.

Lambda calculus is about template substitution. It is the abstract mathematics of substituting templates into other templates. Alonzo Church got interested in this when he realized that it had numbers,

    type NumF = <X>(f: (x: X) => X) => (x: X) => X
    const zero: NumF = f => x => x
    const one: NumF = f => x => f(x)
    const two: NumF = f => x => f(f(x))
Addition is not too hard to define, multiplication is actually just function composition, and decrement is an unexpected motherf$@&er. To understand this last point, it may help to understand that this encoding of numbers is basically zero as [], one as [null], two as [null, null], etc and you are trying to use Array.prototype.reduce to compute the array with one fewer element. So you can do it with a (last, curr) pair or a null initial value, you have to know what those look like in the lambda calculus to translate,

    // predecessor and successor
    const succ = n => f => x => n(f(x))
    // Maybe fns: in λ-calc you'd uncurry
    type MaybeF<x> = <z>(ifNil: z, ifJust: (x: x) => z) => z
    const nil: MaybeF<any> = (ifNil, _ifJust) => ifNil
    function just<x>(x: x): MaybeF<x> {
      return (_ifNil, ifJust) => ifJust(x);
    }

    const pred = n =>
        n(maybe_n => maybe_n(just(zero), k => just(succ(k))))(nil)
      
Now you asked for a technique to remember the Y combinator. The basic thing to remember is the infinite template substitution discovered by Haskell Curry,

    (f => f(f))(f => f(f))
Forgetting everything you know about programming languages, and just thinking about template substitution, this is a template on the left, being substituted with a value on the right, and the reason it's an infinite loop is that after the substitution you get the exact same expression that you had before the substitution. [On the right we could have also written g => g(g) if that helps, the two variables are defined in separate scopes and only happen to have the same name f to make it clearer that this will loop infinitely if you try to eagerly evaluate it.]

Terms like this, were why Curry wanted a type theory. He immediately understood that this was kind of a weird expression because if you tried to express the idea of f(f) it was secretly holding on to a sort of paradox of self-reference or an infinity or whatever you want to call it. It is a function type which takes only the same function type as an argument, and returns God-knows-what. If you just forbid self-reference in the typing judgments, you don't get this sort of weird f(f) pathology.

So if you are remembering f(f) being somehow the key to the Y combinator, then you immediately see that you can kind of step it by not immediately evaluating it,

    const Q = (f => () => f(f))(f => () => f(f))
so as a matter of algebra Q() = Q although a programming language struggles to prove equality between functions so as a matter of programming that might not be equal. So this is a function you can call Q()()()() and it's just infinitely callable without producing any other values.

But why () =>, why not x => ? Well, you can introduce that but Q will just ignore it, it doesn't know what to do with that. So you need to write f(f)(x) to plumb it through to do something.

Note briefly that there IS a difference between f(f) and x => f(f)(x). The latter delays execution of f(f) until needed and so is still stepped, the former is an infinite loop.

And the last thing is that you need to hand this internal function to someone else, some decider, to decide when to call the recursion. This leads to the full form,

    const Y = decider => (f => decider(x => f(f)(x))(f => decider(x => f(f)(x)))
Usage with an example decider:

    const factorial = Y(recurse => n => n <= 1 ? 1 : n * recurse(n - 1));
replies(2): >>43642470 #>>43642707 #
1. Akronymus ◴[] No.43642470[source]
> To understand this last point, it may help to understand that this encoding of numbers is basically zero as [], one as [null], two as [null, null], etc

Isnt it rather nil, [nil], [[nil]] and [[[nil]]] and so on?

replies(1): >>43655084 #
2. crdrost ◴[] No.43655084[source]
No, although you do see that in set theory, but this is a specific idea about the type signatures and encodings.

List type:

    type Stack<x> = null | {first: x, rest: Stack<x>}
The church encoding of a data structure, is to go through all of these cases separated by |, and define a handler for each one, and then define a function which accepts all those handlers and calls the appropriate one for its case:

    type StackF<x> = <z>(
        ifNull: (n: null) => z,
        ifItem: (first: x, rest: z) => z
      ) => z;
The Scott encoding is actually a little more practical, and has `rest: StackF<x>` in that second handler, but that's not what we have here.

Now the point is that a unit type like `null` that only has one possible value, that first handler can actually be simplified to just `ifNull: z`. Similarly if we consider a list of nulls, we would get

    type NullStackF = <z>(
        ifEnd: z,
        ifItem: (rest: z) => z
      ) => z;
And after swapping the arguments and currying, you get precisely the type of the Church numerals.

The Church encoding of a list is effectively replacing that list with its reduce function, so that's why I am saying that it's basically Array prototype.reduce on an Array<null> type. (I actually think it's reduceRight but this type is symmetric under .reverse() so who gives a darn). So it's

    const zero_ = f => [].reduce(f)
    const one_ = f => [null].reduce(f)
    const two_ = f => [null, null].reduce(f)
in JS. But if you had just Scott-encoded the numbers instead, you would have had no problems with pred() but you need the Y combinator to actually use the numerals for something interesting:

    type ScottNum = <z>(next: (rest: ScottNum) => z) => (z: z) => z;

    const zero: ScottNum = _f => x => x
    const one: ScottNum = f => _x => f(zero)
    const two: ScottNum = f => _x => f(one)
    function succ(n: ScottNum): ScottNum {
      return f => _x => f(n)
    }
    function pred(n: ScottNum): ScottNum {
      return n((x: ScottNum) => x)(zero)
    }
    function church<z>(n: ScottNum, f: (z: z) => z): (z: z) => z {
      return z => n(m => f(church(m, f)(z)))(z)
    }