Nicholls, Mark Nicholls.Mark at mtvne.com
Fri Jan 11 12:47:20 EST 2008

```
> -----Original Message-----
> From: Luke Palmer [mailto:lrpalmer at gmail.com]
> Sent: 11 January 2008 17:11
> To: Nicholls, Mark
> Subject: Re: [Haskell-cafe] type questions again....
>
> 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.

Yep....it's universal because forall types a.

> If you wrap an existential type up in a constructor, not
> much changes:

If you wrap a what?....should this read existential or universal?

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

It's the only function you've defined the type of....

Id2 :: forall a. a -> a

Now it can hold id2?

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

Yep.

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

"it doesn't have to use the constraint if it doesn't want to" ?

If id was of type..

Id::forall a. Ord a => a -> a

Then I assume it would complain?

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

Yep.

>
>
> Existential types are dual,

Dual? (like a dual basis rather than double?)

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

yes

and then it goes wrong...

> So the type contained inside the NUM'
> constructor

?

> is called existential (note that NUM' itself is just a
> regular ADT; NUM' is not existential).
>

Why existential....see below...I have a guess

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

I think one of the harrowing things about Haskell is the practice of
out of me....

OK so this declaration says that forall x constructed using "NUM'
n"...there *exists* a type T s.t. T is a member of type class NUM"...
which in term implies that that there exists the function negate...

yes?

It's existential...because the word "exists" occurred in the above
translation.

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

Because the existence of the value implies the existence of a type in
the typeclass?

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

We can add it to itself because "+" is of type "a->a->a"...

I think....

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

Eeek.....

Because a could be of any type whatsover?...so how I actually do
anything with it?

Don't know complete guess really.

> Luke
```