overlapping instances and constraints

[Martin Sulzmann]

Check out Section 8.1. in

P. J. Stuckey and M. Sulzmann. A theory of overloading. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(6):1-54, 2005.

for how to use disequality constraints to "resolve" overlapping
instances.

BTW, the translation scheme in the above paper employs a run-time
dictionary passing scheme (similar to Thatte's 94 paper 'Semantics of
type classes revisited' which I didn't know at the time of writing).
Though, it's not hard to imagine how to extract proofs out of CHR
programs to support a compile-time dictionary passing scheme.
For example, see 
[February 2006] Recursive Dictionaries and Type Improvement in
Type Class Proofs on my web site.

Martin




Claus Reinke writes:
 > 
 > [
 >  I'll only address some of your issues in this message, as they fall nicely
 >  under the use of a feature I'd like to see anyway: 
 >      type disequality constraints
 > ]
 > 
 > >- A program that type checks can have its meaning changed by adding an
 > >instance declaration
 > >- Similarly adding "import M()" can change the meaning of a program (by
 > >changing which instances are visible
 > 
 > yes, these are consequences of the "start with overlapping declarations, 
 > then avoid overlapping instances by selecting the most specific declaration".
 > 
 > we could avoid that, by using disequality constraints, as some other 
 > constraint logic systems have done. that way, for many examples, there 
 > wouldn't be any overlapping instances in the first place:
 > 
 >     class C a where c :: a -> String
 >     instance C [a]     | a/=Char where c as  = .. -- dealing with most lists
 >     instance C String                where c s = ..   -- special case for strings
 > 
 > [note that the special syntax for disequality constraints (borrowing from 
 >  FDs) here is only needed as long as instance contexts are ignored;
 >  otherwise, type disequality would just be a built-in binary type class,
 >  and the instance would look like this:
 >      instance (a/=Char) => C [a] where c as = ..
 > ]
 > 
 > we could now rule out any overlapping instance declarations, while
 > still permitting instance declarations covering the gaps left by the
 > disequality constraints.
 > 
 > this should work well for uses of overlapping instances as local conditionals,
 > but it would rule out the popular pattern of extensible type case with default
 > rule. the latter explicitly depends on specifying a default instance that may
 > be replaced by more specific instances in future modules.
 > 
 > so we can avoid these issues for some use cases, and that may be worth
 > trying out as a first step, but if we want all use cases, it seems we will have
 > to live with those consequences.
 > 
 > >- When exactly is overlap permitted?  Is this ok?
 > >instance C a Int
 > >instance C Bool b
 > >Previously GHC rejected this, on the grounds that it could be ambiguous
 > >when you came across (C Bool Int).  But not GHC accepts it, on the
 > >grounds that (C Bool Char) is quite unambiguous.  
 > 
 > again, a consequence of the best-match rule. but note that in examples
 > like this, there are two "levels" of overlap: the first level is resolved by
 > the best-match rule, the second _remains_ overlapping. so GHC is faced
 > with the choice of rejecting the declarations outright because they _might_
 > run into this overlap, or to wait and see whether they _will_ run into it.
 > 
 > this could actually be cured by using disequality constraints:
 > 
 >     instance C a Int | a/=Bool
 >     instance C Bool b | b/=Int
 > --    instance C Bool Int         -- we can declare this if we want it
 > 
 > even without ruling out overlapping instance declarations, this excludes
 > the problematic case while permitting the unproblematic ones.
 > 
 > just as unification allows us to prefer specific type instances, disequality
 > allows us to avoid specific type instances, so we would be able to state
 > _only_ the first, resolvable, level of overlap in this example, without
 > having to deal with the by-product of the second, unresolvable, and
 > therefore possibly erroneous level of overlap.
 > 
 > the other issues you raise are just as important, but won't be addressed
 > as easily, so I leave them for later (and possibly for others;-).
 > 
 > cheers,
 > claus
 > 
 > ps I don't know whether additional references are helpful or needed,
 >     but google for "disequality constraints" or for "disunification" (see
 >     also "constructive negation").
 > 
 > _______________________________________________
 > Haskell-prime mailing list
 > Haskell-prime at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime