[Haskell-cafe] Re: coherence when overlapping?

[Martin Sulzmann]

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 at cs.kuleuven.be