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