overlapping instances and constraints
sulzmann at comp.nus.edu.sg
Tue Feb 28 01:07:25 EST 2006
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
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.
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;-).
> 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
More information about the Haskell-prime