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

[Scott Turner]

On 2007 May 13 Sunday 14:52, Benja Fallenstein wrote:
> 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. 

I've had some fun with it, but need to be led by the nose to know what to 
avoid. Which line or lines of the below Haskell code go beyond what can be 
done in a language with just data? And which line or lines violate what can 
be done with codata?

> 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