[Haskell-cafe] Existential types (Was: Type vs TypeClass duality)
apfelmus
apfelmus at quantentunnel.de
Wed Oct 24 05:03:10 EDT 2007
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
More information about the Haskell-Cafe
mailing list