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
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