The Y Combinator in Go with generics

Much of the point of the Y combinator is the construction of a fixed point operator without appealing to self-definition. Using fix in its own definition violates that, one could say that the recursion arises due to Haskell's recursive bindings.

The standard definition in untyped lambda calculus is

    \f -> (\x -> f (x x)) (\x -> f (x x))

but if we try to give a type to x, let's call it X, we'll see something funny

    X = i -> o               -- we know it's a function type because it's applied
    X = X -> o               -- it's self-applied, so the input must be X
    X = (X -> o) -> o        -- expanding the inner reference
    X = ((X -> o) -> o) -> o -- oh no

Unfortunately, this won't type in Haskell because `type X = (X -> o) -> o` is invalid and would loop the type checker. We must introduce an explicit indirection. This explicitness forces us to control if and when this type expands and prevents the checker from looping.

    newtype Loop a = Loop (Loop a -> a)

    defer :: (Loop a -> a) -> Loop a
    defer f = Loop f

    apply :: Loop a -> (Loop a -> a)
    apply (Loop f) = f

This type is exactly a solution to `X = (X -> o) -> o` but with the recursion explicitly tagged, as

    x               :: Loop o
    apply x         :: Loop o -> o
    apply x . defer :: (Loop o -> o) -> o

So now we can type the type Y combinator without utilizing Haskell's self-referential bindings.

    y f :: (a -> a) -> a
    y f = apply half half
      where 
        half :: Loop a                  -- the type of X
        half x = defer (f (apply x x))  -- i.e. \x -> f (x x)

Still pretty concise compared to Go!

(Probably saw this first at https://r6.ca/blog/20060919T084800Z.html)

That's a fixed point combinator, not the Y Combinator.

https://stackoverflow.com/questions/4273413/y-combinator-in-...

pretty sure the point of the Y combinator is to server as a definition for recursion in languages that do not support it natively (ie, lambda calc)

if you're making a recursive function call then you're just making something that kinda looks like Y but isn't.

FWIW i don't think you can write Y in haskell, it would not make much sense.

according to this thread you can't, because it doesn't type check.

https://stackoverflow.com/questions/4273413/y-combinator-in-...

The first example will lead to infinite recursion. There is no base case.

why isn't it "auto this"? That that would make it <type> <name> like everything else in the language

The problem is marrying two ideas: lambda calculus (where all computation is done implicitly via anonymous functions), and recursion (where some set of functions call each other by name in a cycle).

This is a bit more interesting than it looks because ostensibly you're using the name of a function in its definition before that name ever has a meaning -- you're not really saying that you should literally call that symbol, but that the compiler should produce a function according to some set of rules that fills in the self references.

That doesn't work in lambda calculus though, where definitions are concrete and you don't have compiler magic to resolve the undefined symbol in your definition. A solution is to pass some function to itself as an argument, and you have a code pattern that goes along with it (the Y combinator).

This retains some "usefulness" in the sense that lambda calculus is still being explored for various purposes as a foundation for other things, and also in that languages based on that line of thought might benefit from using that structure explicitly. If you have some sort of syntactic sugar for recursion in your language of choice though and don't care about foundations then it's probably not very applicable.

The thing is that you don't want to use directly the Y-combinator, ever.

It is a tool to show that untyped lambda calculus with just anonymous functions and applications is already Turing-complete, because you can write the `Y-combinator`, thus you can define recursive functions, and thus you can write `while` loops.

In a way, the Y-combinator is one of the possible ways to reach Turing-completeness by accident. It is an important example to keep in mind if you want to design a type system for a programming language that is not Turing-complete.

But as soon as you want Turing-completeness, the Y-combinator is not a nice primitive for most users. In this case, either your language is flexible enough to write a good library for recursive definitions based on the Y-combinator. Otherwise, it often works better to introduce recursive definitions as a primitive, even if theoretically this primitive is not absolutely needed.

You're right, these posts assume one knows what the Y combinator is for. Wikipedia has a decent explanation: https://en.wikipedia.org/wiki/Fixed-point_combinator

Key point:

    the Y combinator implements simple recursion. In the lambda calculus it is not possible to refer to the definition of a function in a function body. Recursion may only be achieved by passing in a function as a parameter. The Y combinator demonstrates this style of programming. 

You don't really need it in modern programming languages that natively support named functions and recursion, but it's an interesting part of the underlying theory of lambda calculus.

The Y combinator lets you implement recursion without using recursion. For example, a Javascript closure can't refer to itself. But if we define the (strict) Y combinator using JS closures:

    let Y = f => (x => x(x))(x => f(z => x(x)(z)))

then we can call it, again only using closures, and define a function that sums the numbers from 1 to N by "calling itself":

    let sumToN = Y(sumToN => n => n == 0 ? 0 : n + sumToN(n-1))

    sumToN(4)
    // -> 10

In practice, no one actually implements recursion this way because it would be slow. So instead it's more of a statement about the expressiveness of languages, and how "we have recursion!" doesn't actually give you any power you didn't have before, if you had functions.

It's a plaything, it's not meant to be applied in the real world. It's like asking for a "motivating practical example" for a quine.

Knowledge of the Y-combinator helps avoid making your language divergent (sometimes desirable), disallowing explicit recursion is not enough! The typed lambda calculus uses static types to prevent the Y-combinator and give a sound logic for proofs.

The same question could be posed for many other mathematical and theoretical computer science constructs. It's a mathematical building block, a node in the graph that is the world of mathematics, and it's possible it plays a part in some advance if you were working in that field.

Look at eg the Curry's Paradox part on the WP page for a taste.