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@haskell.org > http://haskell.org/mailman/listinfo/haskell-prime _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
