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

[Stefan O'Rear]

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

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