Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further insight]

2008-05-28 Thread Andrew Coppin
Luke Palmer wrote: When you're reasoning about this, I think it would help you greatly to explicitly put in *all* the foralls. In haskell, when you write, say: map :: (a - b) - [a] - [b] All the free variables are *implicitly* quantified at the top level. That is, when you write the above,

Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further insight]

2008-05-28 Thread Lennart Augustsson
These things become easier if you are explicit about type applications (which Haskell isn't). Phillippa mentioned it in an earlier post, but here it is again. First the old stuff, if you have a term of type (S-T) then the (normal form of) term must be (\ x - e), where x has type S and e has type

Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further insight]

2008-05-28 Thread Ryan Ingram
On 5/28/08, Isaac Dupree [EMAIL PROTECTED] wrote: Andrew Coppin wrote: Finally, that seems to make actual sense. I have one final question though: forall x, y. x - y - Z forall x. x - (forall y. y - Z) Are these two types the same or different? [Ignoring for a moment the obvious