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

[apfelmus]

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


> Thanks for posting this, I finally understand existentials!

λ(^_^)λ


Regards,
apfelmus