Thanks for the concise explanation. I do have one minor question though.
> -+- 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.
Don't you mean *epimorphic* instead of isomorphic (not that it matters)?
For any existential type a of cardinality less than that of String, it
is isomorphic, but if a = String, then by Cantor's theorem String ->
String has a cardinality greater than String and cannot be isomorphic to it.
> ∃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].
True. This loses no observable information because (given the
existential) even if there may be no unique function for a given String,
there would be no way to tell any two such apart anyway, as the only
thing you can do with them is to apply the functions of Show, and they
all return the same String.
apfelmus 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
