I believe that GHC's overlapping instance extensions effectively uses inequalities. Why do you think that 'inequalities' model 'best-fit'? instance C Int -- (1) instance C a -- (2) under a 'best-fit' instance reduction strategy we would resolve C a by using (2). 'best-fit' should be very easy to implement. Simply order instances (resulting CHRs) in an appropriate 'best-fit' order. In case of instance C Int instance a =!=Int | C a (2') we can't reduce C a (because we can't satisfy a=!=Int) Notice that (2') translates to rule C a | a =!=Int <==> True I think it's better to write a =!=Int not as part of the instance context but write it as a guard constraint. I don't think there's any issue for an implementation (either using 'best-fit' or explicit inequalities). The hard part is to establish inference properties such as completeness etc. Martin Tom Schrijvers writes:
On Thu, 13 Apr 2006, Martin Sulzmann wrote:
Coherence (roughly) means that the program's semantics is independent of the program's typing.
In case of your example below, I could type the program either use the first or the second instance (assuming g has type Int->Int). That's clearly bound.
Guard constraints enforce that instances are non-overlapping.
instance C Int instance C a | a =!= Int
The second instance can only fire if a is different from Int.
Non-overlapping instances are necessary but not sufficient to obtain coherence. We also need that types/programs are unambiguous.
Claus Reinke was discussing this with me some time ago. He called it the best fit principle, which would in a way, as you illustrate above, allow inequality constraints to the instance head. You could even write it like:
instance (a /= Int) => C a
as you would do with the superclass constraints... I wonder whether explicit inequality constraints would be useful on their own in all the places where type class and equality constraints are used (class and instance declarations, GADTs, ...). Or maybe it opens a whole new can of worms :)
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be