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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
