[Haskell-cafe] Type system madness

[Stefan O'Rear]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070709/796d6dc3/attachment.bin