[Haskell-cafe] Type vs TypeClass duality

[TJ]

On 10/23/07, Jules Bean <jules at jellybean.co.uk> 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