Re: [Haskell-cafe] Re: coherence when overlapping?
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
| I believe that GHC's overlapping instance extensions | effectively uses inequalities. I tried to write down GHC's rules in the manual: http://haskell.org/ghc/dist/current/docs/users_guide/type-extensions.htm l#instance-decls The short summary is: - find candidate instances that match - if there is exactly one, choose it - if the is more than one, choose the best fit UNLESS that choice would be changed if a type variable was instantiated Simon
On Thu, 13 Apr 2006, Martin Sulzmann wrote:
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).
Claus used the term best-fit, and what was meant is exactly the same as what you mean, i.e. a delayed until sufficiently instantiated best-fit rather than an immediate best fit. -- 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
On 2006-04-13, 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.
This best-fit is essentially what people doing multi-method dispatch want. It turns out to not be as trivial as one would hope. -- Aaron Denney -><-
participants (4)
-
Aaron Denney -
Martin Sulzmann -
Simon Peyton-Jones -
Tom Schrijvers