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