Re:The Why of Y (2001) [pdf]
by snrji on Sunday December 09, 2018 @07:19AM
(#18640529)
I'm not proficient in Haskell, but how would the compiler be able to statically type that expression?
[ Parent
| on HN ]
Prelude> y f = f (y f)
Prelude> :type y
y :: (t -> t) -> t
Because f is applied to an argument, it must be a function of generic type t -> u. Because y is applied to f, it must be a function of type (t -> u) -> v. Then the type of y f is v. Because f is applied to y f, t = v. Then the type of f (y f) is u. Because y f is defined as f (y f), the two expressions need to have the same type, t = u. Therefore f is of type t -> t and y is of type (t -> t) -> t.
Re:The Why of Y (2001) [pdf]
by user2994cb on Sunday December 09, 2018 @09:30AM
(#18640990)
It's true that the original non-recursive definition of Y doesn't typecheck in Haskell:
Prelude> \f->(\x->f(x x))(\x->f(x x))
<interactive>:5:14:
Occurs check: cannot construct the infinite type: r0 ~ r0 -> t
...