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

[apfelmus]

TJ wrote:
>>
>>     data Showable = forall a. Show a => Showable a
>>     stuff = [Showable 42, Showable "hello", Showable 'w']
> 
> Which is exactly the kind of 2nd-rate treatment I dislike.
> 
> I am saying that Haskell's type system forces me to write boilerplate.

Nice :) I mean, the already powerful Hindley-Milner type system is free 
of type annotations (= boilerplate). It's existential types and other 
higher-rank types that require annotations because type inference in 
full System F (the basis of Haskell's type system so to speak) is not 
decidable. In other words, there is simply no way to have System F 
without boilerplate.

That being said, there is still the quest for a minimal amount of 
boilerplate and in the right place. That's quite a hard problem, but 
people are working on that, see for instance

http://research.microsoft.com/~simonpj/papers/gadt/index.htm
http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm
http://research.microsoft.com/users/daan/download/papers/mlftof.pdf
http://research.microsoft.com/users/daan/download/papers/existentials.pdf

>>
>>      [exists a. Show a => a]
> 
> I actually don't understand that line. Substituting forall for exists,
> someone in my previous thread said that it means every element in the
> list is polymorphic, which I don't understand at all, since trying to
> cons anything onto the list in GHCi results in type errors.

Let's clear the eerie fog surrounding universal quantification in this 
thread.

-+- The mathematical symbol for  forall  is  ∀  (Unicode)
                                  exists  is  ∃

-+- ∀a.(a -> a) means:
     you give me a function (a -> a) that I can apply
     to _all_ argument types  a  I want.

   ∃a.(a -> a) means:
     you give me a function (a -> a) and tell me that
     _there is_ a type  a  that I can apply this function to.
     But you don't tell me the type  a  itself. So, this particular
     example ∃a.(a -> a) is quite useless and can be replaced with ().

-+- A more useful example is

     ∃a. Show a => a   i.e.  ∃a.(a -> String, a)

So, given a value (f,x) :: ∃a.(a -> String, a), we can do

     f x :: String

but that's pretty much all we can do. The type is isomorphic to a simple 
String.

     ∃a.(a -> String, a)  ~  String

So, instead of storing a list [∃a. Show a => a], you may as well store a 
list of strings [String].

-+- Since ∀ and ∃ are clearly different, why does Haskell have only one 
of them and even uses ∀ to declare existential types? The answer is the 
following relation:

   ∃a.(a -> a) = ∀b. (∀a.(a -> a) -> b) -> b

So, how to compute a value  b  from an existential type ∃a.(a -> a)? 
Well, we have to use a function  ∀a.(a -> a) -> b  that works for any 
input type (a -> a) since we don't know which one it will be.

More generally, we have

   ∃a.(f a)    = ∀b. (∀a.(f a) -> b) -> b

for any type  f a  that involves a, like

   f a = Show a => a
   f a = a -> a
   f a = (a -> String, a)

and so on.

Now, the declaration

   data Showable = forall a. Show a => Showable a

means that the constructor Showable gets the type

   Showable :: ∀a. Show a => a -> Showable

and the deconstructor is

   caseS :: Showable -> ∀b. (∀a.(Show a => a) -> b) -> b
   caseS sx f = case sx of { Showable x -> f x }

which is the same as

   caseS :: Showable -> ∃a. Show a => a

. GADT-notation clearly shows the ∀

   data Showable where
     Showable :: ∀a -> Showable


-+- The position of the quantifier matters.
- Exercise 1: Explain why

   [∀a.a]  ∀a.[a]  [∃a.a]  and  ∃a.[a]

are all different.
- Exercise 2: ∀ can be lifted along function arrows, whereas ∃ can't. 
Explain why

   String -> ∀a.a   =   ∀a.String -> a
   String -> ∃a.a  =/=  ∃a.String -> a

Since ∀ can always be lifted to the top, we usually don't write it 
explicitly in Haskell.

-+- Existential types are rather limited when used for OO-like stuff but 
are interesting for ensuring invariants via the type system or when 
implementing algebraic data types. Here the "mother of all monads" in 
GADT-notation

   data FreeMonad a where
     return :: a -> FreeMonad a
     (>>=)  :: ∀b. FreeMonad b -> (b -> FreeMonad a) -> FreeMonad a

Note the existential quantification of  b . (The ∀b can be dropped, like 
the ∀a has been.)


Regards,
apfelmus