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. 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