On Mon, Jul 09, 2007 at 09:05:55PM +0100, Andrew Coppin wrote:
OK, can somebody explain to me *really slowly* exactly what the difference between an existential type and a rank-N type is?
(I couldn't find much of use on the wiki. I have now in fact written some stuff there myself, but since I don't understand it in the first place, I'm having difficulty trying to explain it to anybody else...)
There isn't really such a thing as existential types. Rank-N types exist, but they are more of an implementation detail. All users should worry about is Quantifiers. A quantifier is an operator on types which defines a variable in some way. id has type :: ∀α. α → α This means that id has type Int → Int, Bool → Bool, [Char] → [Char], etc etc etc. FOR ALL toUpper (can) have type :: ∃α. α → α toUpper has ONE of Int → Int, Char → Char, etc etc etc. a type α EXISTS such that toUpper has type α → α. Yes, I know toUpper has a more specific type - bare with me, it was the best example I could think of. If you're at all familiar with mathematics logic, don't hesistate to apply your intuitions about forall and exists - type systems and logics really are the same things. If you have a value of existential type, you can only do things with it that you can do with any type, because you don't know the actual type. Existential types hide information from the users. If you have a value of universal type, you can do things with it as if it had any matching type of your choice, because it doesn't know and can't care about the actual use type. Universal types hide information from the implementors. In Haskell 98, existential quantification is not supported at all, and universal quantification is not first class - values can have universal types if and only if they are bound by let. You cannot pass universally typed values to functions. Stefan