[Haskell-cafe] Type system madness
andrewcoppin at btinternet.com
Mon Jul 9 16:57:14 EDT 2007
Stefan O'Rear wrote:
> All users should worry about is Quantifiers.
> A quantifier is an operator on types which defines a variable in some
> 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
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.
More information about the Haskell-Cafe