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

On Tue, May 15, 2007 at 10:28:08PM -0400, Scott Turner wrote:

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?

There is nothing wrong with having both codata and data in a consistent language. For instance, in System Fω, you can have both []: λ(el : *). ∀(res : *). (el → res → res) → res → res and co-[]: λ(el : *). ∀(res : *). (∀(seed : *). seed → (seed → el) → (seed → seed) → res) � The trouble comes when they can be freely mixed. Stefan