[Haskell-cafe] Type system madness

[Andrew Coppin]

Stefan O'Rear wrote:
> All users should worry about is Quantifiers.
>
> A quantifier is an operator on types which defines a variable in some
> way.
>   

OK...

> id has type :: ∀α. α → α
>
> toUpper (can) have type :: ∃α. α → α
>   

So... you're saying that id:: x -> x works for *every* possible choice 
of x, but toUpper :: x -> x works for *one* possible choice of x?

(BTW... How in the hell do you get symbols like that in plain ASCII??)

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

I have wide interests in diverse areas of science, mathematics and 
computing, covering everything from cryptology to group theory to data 
compression - but formal logic is something I've never been able to bend 
my mind around. :-(

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

I stand in awe of people who actually understand what "universal" and 
"existential" actually mean... To me, these are just very big words that 
sound impressive.

So, are you saying that if x is existential, it must work for any 
possible x, but if x is universal, I can choose what x is?

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

Erm...