Wed, 11 Oct 2000 09:53:52 -0400
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
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.