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

[Alfonso Acosta]

Thanks for posting this, I finally understand existentials!

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?

I think this shows why digested tutorials, as opposed to research
papers (which tend require a strong background), are needed in the
Haskell community to make life easier for the newcomer.

Things as existentials (which are not part of the standard yet but
used frequently in real world applications)  should be documented in a
friendly way.

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.

Thanks apfelmus!

PS: Can't wait for the Real World Haskell Book to be released.


On 10/24/07, apfelmus <apfelmus at quantentunnel.de> wrote:
> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>