Levent, 

thanks for your explanation. I liked it. 

There are a few things I would like to comment.

1) My previous message was mistaken. Sorry. Forget it. I will try
again.

So suppose again the simpler map:: (a -> b) -> [a] -> [b]. 

Then (in fact) system CT infers that the only possible definition of
union that can be used in "union . map fst" is the first one: that
with type [a]->[a]->[a].

The second one, with type (a->a->Bool)->[a]->[a]->[a], cannot, since,
in system CT, [b] and (a->a->Bool) do not match (unification fails). 

So, the type of "union . map fst" is simply [(a, b)] -> [a] -> [a].

(Again, sorry for my mistake in the previous message.)

2) So now let us consider the more general map, that is overloaded for
lists and functions. In System CT, this would be done by giving
definitions (instances, no class declaration required) of map,
including:

     map:: (a->b) -> [a] -> [b]        and
     map:: (a->b) -> (c->a) -> (c->b)

and "union . map fst" could be used with each of these. 

If it is applied to a list of pairs, the first map will be used
(together with union::[a]->[a]->[a]).

If it is applied to a function, of type a -> (a->Bool, b), the second
map will be used (together with union::(a->a->Bool)->[a]->[a]->[a]). 

3) I think that if the type system allows unifications like, say, 

        c b  with a->a->Bool

things get (unnecessarily) more complicated. 
    
Yours,

Carlos







Reply via email to