[Haskell-cafe] type questions again....

[Luke Palmer]

2008/1/11 Nicholls, Mark <Nicholls.Mark at mtvne.com>:
> Can someone explain (in simple terms) what is meant by existential and
> universal types.
>
> Preferably illustrating it in terms of logic rather than lambda calculus.

Well, I don't know about logic.  While they are certainly related to
existential and universal types in logic, I don't really see a way to
explain them in terms of that.

Universal types are easy, you use them every day in Haskell.  Take for
example id:

> id :: a -> a

Or better illustrated (using ghc extension):

> id :: forall a. a -> a

That means that for any type a I pick, I can get a value of type a ->
a from id.  If you wrap an existential type up in a constructor, not
much changes:

> newtype ID = ID (forall a. a -> a)

ID can hold any value of type forall a. a -> a; i.e. it can hold any
value which exhibits the property that it can give me a value of type
a -> a for any type a I choose.  In this case the only things ID can
hold are id and _|_, because id is the only function that has that
type.   Here's how I might use it:

> applyID :: ID -> (Int,String) -> (Int,String)
> applyID (ID f) (i,s) = (f i, f s)

Note how I can use f, which is a universal type, on both an Int and a
String in the same place.

You can also put typeclass constraints on universals.  Take the
universal type forall a. Num a => a -> a.  Among functions that have
this type are:

> add1 :: forall a. Num a => a -> a
> add1 x = x + 1

> id' :: forall a. Num a => a -> a
> id' = id  -- it doesn't have to use the constraint if it doesn't want to

Wrapping this up in a constructor:

> newtype NUM = NUM (forall a. Num a => a -> a)

We can create values:

> NUM add1 :: NUM
> NUM id   :: NUM

And use them:

> applyNUM :: NUM -> (Int, Double) -> (Int, Double)
> applyNUM (NUM f) (i,d) = (f i, f d)



Existential types are dual, but you need to use constructors to use
them.  I'll write them using GADTs, because I think they're a lot
clearer that way:

data NUM' where
    NUM' :: Num a => a -> NUM'

Look at the type of the constructor NUM'.  It has a universal type,
meaning whatever type a you pick (as long as it is a Num), you can
create a NUM' value with it.  So the type contained inside the NUM'
constructor is called existential (note that NUM' itself is just a
regular ADT; NUM' is not existential).

So when you have:

> negNUM' :: NUM' -> NUM'
> negNUM' (NUM' n) = NUM' (negate n)

Here the argument could have been constructed using any numeric type
n, so we know very little about it.  The only thing we know is that it
is of some type a, and that type has a Num instance.  So we can
perform operations to it which work for any Num type, such as negate,
but not things that only work for particular Num types, such as div.

> doubleNUM' :: NUM' -> NUM'
> doubleNUM' (NUM' n) = NUleM' (n + n)

We can add it to itself, but note:

> addNUM' :: NUM' -> NUM' -> NUM'
> addNUM' (NUM' a) (NUM' b) = NUM (a + b)  -- Illegal!

We can't add them to each other, because the first argument could have
been constructed with, say, a Double and the other with a Rational.

But do you see why we're allowed to add it to itself?

How about this:

> data Variant where
>    Variant :: a -> Variant

This is a type that can be constructed with any value whatsoever.
Looks pretty powerful... but it isn't.  Why not?

Luke