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...
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
