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

On 2007 May 13 Sunday 14:52, Benja Fallenstein wrote:

2007/5/12, Derek Elkins :

...

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