[Haskell-cafe] Higher order types via the Curry-Howard correspondence

[Benja Fallenstein]

2007/5/13, Benja Fallenstein <benja.fallenstein at gmail.com>:
> Modulo the constructor and destructor invocation, this is just the
> familiar non-terminating ((\x -> x x) (\x -> x x)), of course.

The same technique also gives us

data Y a = Y (Y a -> a)

y :: (a -> a) -> a
y f = (\(Y x) -> f $ x $ Y x) $ Y $ (\(Y x) -> f $ x $ Y x)

or

y :: (a -> a) -> a
y f = g (Y g) where
    g (Y x) = f $ x $ Y x

as well as these formulations, which make GHC loop forever on my system:

y :: (a -> a) -> a
y f = (\(Y x) -> f (x (Y x))) (Y (\(Y x) -> f (x (Y x))))

y :: (a -> a) -> a
y f = g (Y g) where
    g (Y x) = f (x (Y x))

(Aaah, the power of the almighty dollar. Even type inference isn't
safe from it.)

- Benja