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