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