On 10/23/07, Jules Bean
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