[Haskell-cafe] Type system madness

Jonathan Cast jcast at ou.edu
Mon Jul 9 17:02:05 EDT 2007


On Monday 09 July 2007, Andrew Coppin wrote:
> 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?

Remember the quantifiers!  id :: forall x. x -> x works for every choice of x, 
but toUpper :: exists x. x -> x works for only one 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?

As the consumer of the value.  For the producer, it works the other way 
around.

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

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs


More information about the Haskell-Cafe mailing list