
On Tue, 2007-10-23 at 17:40 +0800, TJ wrote:
On 10/23/07, Jules Bean
wrote: 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.
I think your idea is good, but I also think it's much harder to specify and implement than you seem to imply. Here's an example of one difficult point (the first one I thought of); I'm sure there are many more. Consider the function: show_list x = map show x Can you use show_list on your list? If so: what type does show_list have? How is it implemented? (Consider that in a typical Haskell implementation, show_list would take a hidden dictionary parameter and a normal list parameter. But on your list, show_list takes a list where each element contains a hidden dictionary.) Carl Witty