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

[Benja Fallenstein]

2007/5/12, Derek Elkins <derek.a.elkins at gmail.com>:
> In Haskell codata and data coincide, but if you want consistency, that cannot be
> the case.

For fun and to see what you have to avoid, here's the proof of Curry's
paradox, using weird infinite data types. We'll construct an
expression that inhabits any type a. (Of course, you could just write
(let x=x in x). If you want consistency, you have to outlaw that one,
too. :-))

I'll follow the proof on Wikipedia: http://en.wikipedia.org/wiki/Curry's_paradox

data Curry a = Curry { unCurry :: Curry a -> a }

id :: Curry a -> Curry a

f :: Curry a -> (Curry a -> a)
f = unCurry . id

g :: Curry a -> a
g x = f x x

c :: Curry a
c = Curry g

paradox :: a
paradox = g c

Modulo the constructor and destructor invocation, this is just the
familiar non-terminating ((\x -> x x) (\x -> x x)), of course.

- Benja