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

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

On 10/24/07, Peter Hercek wrote:

I do not see why forall can be lifted to the top of function arrows. I probably do not understand the notation at all. They all seem to be different to me.

Consider this simple function: \b x y -> if b then x else y Let's say we wanted to translate that into a language like System F, where every lambda has to have a type. We could write something like: \(b::Bool) (x::?) (y::?) -> if b then x else y but we need something to put in those question marks. We solve this by taking the type of x and y as an additional parameter: \(a::*) (b::Bool) (x::a) (y::a) -> if b then x else y This would have the type "forall a. Bool -> a -> a -> a". In a dependently typed system, we might write that type as "(a::*) -> (b::Bool) -> (x::a) -> (y::a) -> a". Since b doesn't depend on a, we can switch their order in the argument list, \(b::Bool) (a::*) (x::a) (y::a) -> if b then x else y This has type "Bool -> forall a. a -> a -> a" or "(b::Bool) -> (a::*) -> (x::a) -> (y::a) -> a". Haskell arranges things so that the implicit type arguments always appear first in the argument list. I find it helps to think of forall a. as being like a function, and exists a. as being like a pair. -- Dave Menendez http://www.eyrie.org/~zednenem/

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

Hello Luke, Tuesday, October 23, 2007, 12:42:19 PM, you wrote:

of me whining about Haskell's "lack" of OO features. How are you supposed to design your programs modularly if you can't have a type-agnostic list?

But it doesn't bug me anymore. I can't really say why.

i tink because it's very easy to pass any required function together with the data. OOP classes is just fixed way to do this while FP is lower-level, more flexible tool. look at http://haskell.org/haskellwiki/OOP_vs_type_classes -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

On 10/23/07, Jules Bean wrote:

Short answer: You are worrying about syntax. The things you want are possible.

TJ wrote:

...

Following up on my previous thread, I have figured out why it bothered me that we cannot have a list such as the following: ["abc", 123, (1, 2)] :: Show a => [a]

That type doesn't mean what you want it to mean. That means :

A list of objects of some fixed type 'a', such that a is a member of the typeclass 'Show'. In fact, "worse" than that, it's a polymorphic list, which means the *caller* should be able to choose the type 'a'.

What you want to mean is 'A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show.

Yes, of course. But given that what I want isn't directly expressible in Haskell, without creating an existential type, I would not have been able to give a valid Haskell type signature anyway ;-)

Incidentally there is no restriction that all the elements in a list have to be an ADT. They can be functions, or tuples of functions, or higher order functions, or lists of tuples of higher order polymorphic functions operating on lists of functions on tuples of.....

Yes. My mistake.

...

Suppose that I have a list of type Show a => [a], I imagine that it would not be particularly difficult to have GHC insert a hidden item along with each value I cons onto the list, in effect making the concrete type of the list [(Dictionary Show, a)].

Right. That's almost exactly what the Showable existential does.

...

I'm assuming that it will not be particularly difficult because GHC will know the types of the values I cons onto it, so it will most definitely be able to find the Show dictionary implemented by that type, or report a type mismatch error. No dynamic type information is necessary.

Now it sounds like your only complaint is that : has the wrong type?

No. I am saying that Haskell's type system forces me to write boilerplate.

That is, the type inference algorithm which GHC uses, which is not the only one you can imagine, but for a variety of reasons is considered to be one of the best choices, cannot 'automatically' construct existentials, and requires some kinds of explicit annotations to 'delimit' the existential.

Why can't it automatically construct them then? Assuming we do have a syntax for "A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show", as the following: ls :: [a where Show a] Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. Which is exactly the same as for a list intList of type [Int], where a) everything you cons onto it is of type Int b) where you extract items from intList, you use them only as it is valid to use an Int (+,-,*,/,etc) Now assuming the existential type data E = forall a. Show a => E a EList :: [E] What I have done is to wrap up the idea that E contains any instance of Show, and that EList contains any E. Which is a roundabout way of saying what I wanted to say: ls contains any instance of Show. It seems Haskell's type inference has not kept up with advancements in existential types.

I will also repeat the non-justified assertion that others have made, and that I've made myself in the other thread, that you don't need existentials as often in haskell as you do in OO languages, and they certainly don't always need to be type-class quantified ones.

And I would like to say that whether or not I need it is not the issue, as I currently do not in fact need it. This is a study of the Haskell language not my possible practical applications of it. TJ

On 10/23/07, Jules Bean wrote:

I believe it is to do with the requirement that expressions have a unique principle type. Certainly in principle the algorithm you outline is possible, but I don't know what else you would lose.

I'm not familiar with the term "principal type". I shall have to study it.

...

And I would like to say that whether or not I need it is not the issue, as I currently do not in fact need it. This is a study of the Haskell language not my possible practical applications of it.

Whether one needs it, or does not need it, is indeed an issue: any change to the type inference algorithm has a cost. That cost has to be judged against the value of it. If an extension is seldom needed, then its value is low, so the cost is unlikely to be considered worth it. If an extension is frequently need and the cost is low, then that argues for it..

Ah... harsh realities of engineering. Well I hope this is judged to be important enough to be included in a future revision of Haskell. Thanks, TJ

...

Why can't it automatically construct them then? Assuming we do have a syntax for "A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show", as the following:

ls :: [a where Show a]

Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. Not sure if anyone has mentioned something similar, and it's not quite what people have been suggesting - but with minimal boilerplate (that I'm sure a TH hacker could derive for you) you can get close to typeclass parameterised lists using GADTs (& ghc 6.8 snapshots ;)) at

the moment. Regards, Tris {-# LANGUAGE EmptyDataDecls, ScopedTypeVariables, PatternSignatures, GADTs, RankNTypes, KindSignatures, TypeOperators #-} {- A list where all elements are in class Show -} testList :: SingleList ShowConstraint testList = () # (LT,EQ,GT) # False # 'a' # (3.0 :: Double) # "hello" # nil {- My user functions over that list -} test = map' (\ShowC -> show) testList test2 = foldr' (\ShowC -> (+) . length . show) 0 testList {- A tiny bit of boilerplate for Show, later rinse repeat for other typeclasses -} data ShowConstraint a where ShowC :: (Show a) => ShowConstraint a instance Show a => Reify (ShowConstraint a) where reify = ShowC {- *Main> test ["()","(LT,EQ,GT)","False","'a'","3.0","\"hello\""] *Main> test2 30 -} {- The bit that is a library -} {- A generic list definition, - (a b) is the witness of the type class for this type, - b is the actual value we put in the list -} data SingleList (a :: * -> *) where Cons :: (a b) -> b -> SingleList a -> SingleList a Nil :: SingleList a {- helper functions to avoid having to pass in the witness explicitly -} nil :: SingleList a nil = Nil infixr 5 # (#) :: (Reify (a b)) => b -> SingleList a -> SingleList a val # rest = Cons reify val rest {- A way to get the type class constraint witness automagically -} class Reify a where reify :: a {- traditional(ish) map, note the function is passed the witness so it can use that - to get the typeclass constraint back into scope by pattern matching on it -} map' :: forall a c . ((forall b . a b -> b -> c) -> SingleList a -> [c]) map' _ Nil = [] map' f (Cons r v rest) = f r v : map' f rest {- and foldr -} foldr' :: forall a c . (forall b . a b -> b -> c -> c) -> c -> SingleList a -> c foldr' f d = go where go Nil = d go (Cons r v rest) = (f r v) (go rest)

On Wed, Oct 24, 2007 at 11:00:14AM +0800, TJ wrote:

Tristan Allwood:

Very cool. I don't understand some (a lot of) parts though:

...

instance Show a => Reify (ShowConstraint a) where reify = ShowC

ShowC has type "(Show a) => ShowConstraint a", whereas reify is supposed to have type "ShowConstraint a". Yes. ShowC is a constant that wraps up the knowledge of (Show a =>) for ShowConstraint. So (in this case)

reify :: ShowConstraint a reify = ShowC (since ShowC is the only non-bottom value ShowConstraint can take) But in order to return ShowC, we must know that a 'is in' Show, which is why the instance declaration requires that at the point you use reify you can demonstrate that a is in Show: instance Show a => Reify (ShowConstraint a) where ^^^^^^^^^ If the Show a => bit is removed, then the type checker rightly complains, because the ShowC doesn't have a Show a context that it needs. So the trick is that in the cons (#) function which uses reify, you need to prove 'Reify (a b)', and it just so happens that by the instance declaration above, wherever you have 'Show a' then you have 'Reify (ShowConstraint a)' which is why testList needs nothing more than the values to put into it like a normal list.

...

data SingleList (a :: * -> *) where Cons :: (a b) -> b -> SingleList a -> SingleList a Nil :: SingleList a

Cons has a type variable "b" in its signature, but no forall. I suppose it comes from the * -> * in SingleList's type?

Nope. The (a :: * -> *) is a kind annotation and means that the a is a type that is parameterised by a type (e.g. Maybe :: * -> *, whereas Maybe Int :: *), which is why you can write (a b). I think technically it's a redundant annotation here as it can be inferred from the (a b) useage. The b is 'just' a normal, exisistentially quantified variable - GADTs don't require you to write forall in their declarations - see the very last sentence on http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html

That's all I can come up with for now. A great deal of high level coding flying around above my head now.

Hope that helps some, Regards, Tris