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

Scott Turner haskell at pkturner.org
Tue May 15 22:28:08 EDT 2007


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


More information about the Haskell-Cafe mailing list