# [Haskell-cafe] Re: Existential types (Was: Type vs TypeClass duality)

apfelmus apfelmus at quantentunnel.de
Thu Oct 25 05:57:39 EDT 2007

```Alfonso Acosta wrote:
> This bit was specially helpful:
>
> "So, how to compute a value  b  from an existential type ∃a.(a -> a)? ..."
>
> Could you give a specific example of computing existential types?

Well, the word "compute" was probably not a good choice, I meant the
following question: "given a type  ∃a.(a, a -> String) , how can I
pattern match on it? And how to construct values of that type?" (Note
the different example, since  ∃a.(a -> a)  pretty much behaves like the
singleton type  () ).

That's probably best detailed with a comparison to the "finite" sum type
Either A B . (∃ is like an "infinite" sum.) (I'll abbreviate concrete
types like  Int  with  A,B,...  since that's less to write.) For
constructing a value of type  Either A B , we have two functions

Left  :: A -> Either A B
Right :: B -> Either A B

Likewise for ∃, we have functions

fromA :: (A, A -> String) -> ∃a.(a, a -> String)
fromB :: (B, ... etc.
...

but this time for all types  A,B,... . We don't need infinitely many
such functions, one polymorphic functions will do

from  :: ∀b. (b, b -> String) -> ∃a.(a, a -> String)

In fact, that's exactly what the constructor of

data Showable = forall b. Showable (b, b -> String)

does:

Showable :: ∀b. (b, b -> String) -> Showable

That's all there is to it. (To connect to TJ's original post, he
basically wants a language where you don't have to write down this
function  from  or  Showable  anymore, the compiler should infer it for
you.)

Pattern matching is similar. For  Either A B , we have case expressions

foobar :: Either A B -> C
foobar e = case e of
Left  a -> foo a
Right b -> bar b

You probably also know the Prelude function

either :: ∀c. (A -> c) -> (B -> c) -> Either A B -> c

In fact, the case expression can be seen as a syntactic convenience for
the  either  function, any such pattern match with branches  foo  and
bar  can be rewritten as

foobar e = either foo bar e

(Exercise: Convince yourself that it's the same for the function  maybe
. Exercise: Same for  foldr  (ok, ok, the situation is a bit different
there).)

Now, ∃ also has a "pattern match" function. Naively, we would have to
supply an infinite amount of branches

match :: ∀c.
((A, A -> String) -> c)
-> ((B, B -> String) -> c)
-> ...
-> ∃a.(a, a -> String) -> c

but again, this is just one polymorphic branch

match :: ∀c. (∀a. (a,a -> String) -> c) -> ∃a.(a, a -> String) -> c

Again, this is what happens when using a case expression for

data Showable = forall b. Showable (b, b -> String)

foobar :: Showable -> C
foobar s = case s of
Showable fx -> foo fx

The branch  foo  must have a polymorphic type ∀a. (a,a -> String) ->
C. That's all there is to understand pattern matching.

Of course, all this doesn't explain where existential types are useful.
(TJ's post is one example but that's one of their least useful uses.)
Actually, they show up rather seldom.

Peter Hercek wrote:
>> More generally, we have
>>
>>   ∃a.(f a)    = ∀b. (∀a.(f a) -> b) -> b
>>
> Is that by definition? Any pointers to an explanation why
> they are valid?

The right hand side is exactly the type of the  match   function
(without the last function argument). The idea is that this type can in
fact be used as an implementation for ∃ , just like

∀c. (A -> c) -> (B -> c) -> c

can be used as an implementation for  Either A B .

Alfonso Acosta wrote:
> The Haskell Wikibook is usually be helpful but unfortunately it wasn't
> that clear in the case of existentials (for me at least). I think the
> existentials article misses the clarity shown by aplemus' explanation
> and furthermore does not cover the "computing a value from an
> existantial type" directly. Maybe it would be a good idea to extend
> it.

Yes please! At the moment, I don't have the time to polish the article
or my e-mails myself. In any case, I hereby license my explanations
about existentials under the terms noted on
http://en.wikibooks.org/wiki/User:Apfelmus. (This also means that I
don't allow to put them on the haskellwiki which has a more liberal

> Thanks for posting this, I finally understand existentials!

λ(^_^)λ

Regards,
apfelmus

```