type class

[Zhanyong Wan]

Hi Mark,

Thanks for the references you provided!

Mark P Jones wrote:

> My instinct (which perhaps somebody will prove incorrect) is that this will
> not help.  Suppose, for example, that you needed to unify ([a],[b]) with f c
> as part of the type inference process.  How would you solve this problem?
> Alas, there are several different, and incompatible ways:
> 
>    ([a], [b]) =  (/\a. ([a],[b])) a
>               =  (/\b. ([a],[b])) b
>               =  (/\c. (c, [b])) [a]
>               =  (/\d. ([a], d)) [b]
>               =  (/\e. e) ([a], [b])
> 
> Note that the /\-terms in each of these examples satisfies your restriction.
> So I don't think you'll be able to obtain most general unifiers or principal
> types with this restriction.

Let's put your example into the context of type classes:

	class T f c where
	  method :: f c

Now when we want to use method as a ([a],[b]), ambiguity arises, as you
suggested.

However, I think this just means we should allow *at most one* of the
following instances to be declared:

	instance T (/\a. ([a],[b])) a
        instance T (/\b. ([a],[b])) b
        instance T (/\c. (c, [b])) [a]
        instance T (/\d. ([a], d)) [b]
        instance T (/\e. e) ([a], [b])

In other words, the above instances are considered overlapping.
____________________________________________________
|  As long as we only have one of these instances  |
|  in the program, there is no ambiguity.          |
----------------------------------------------------

I'm sure there must be other ramifications (e.g. maybe now whether two
instances are overlapping becomes undecidable -- I haven't thought over
it yet), but it seems worth further investigation.

-- Zhanyong