3 ms·
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 violat
by tel 4y ago
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 https://r6.ca/blog/20060919T084800Z.html)