[Haskell-cafe] Re: coherence when overlapping?
sulzmann at comp.nus.edu.sg
Thu Apr 13 04:40:25 EDT 2006
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
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.
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 Schrijvers
> Department of Computer Science
> K.U. Leuven
> Celestijnenlaan 200A
> B-3001 Heverlee
> tel: +32 16 327544
> e-mail: tom.schrijvers at cs.kuleuven.be
More information about the Haskell-Cafe