Overlapping instances are undoubtedly useful, but they raise lots of interesting questions. Such as - 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 - Haskell would need to be a lot more specific about exactly where context reduction takes place. Consider f xs x = xs == [x] Do we infer the type (Eq a) => [a] -> a -> Bool? Thereby committing to a particular choice of instance? Or do we (as GHC does) infer the type (Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type Char, then an instance Eq [Char] instance would apply. GHC is careful to do the latter. - 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. [Actually this last point is relevant for MPTCs even if overlap isn't allowed.] Concerning using the instance context, yes, it's attractive, but it involves *search* which the current mechanism does not. Presumably you have in mind that the type system should "commit" only when there is only one remaining instance declaration that can fit. You need to be very careful not to prune off search branches prematurely, because in a traditional HM type checker you don't know what all the type are completely. And you need to take functional dependencies into account during the search (but not irrevocably). I have not implemented this in GHC. I don't know anyone who has. I don't even know anyone who has specified it. All good stuff to debate. I'd be happy to see the traffic on MPTCs reach half the level that syntax debates do! In general, I think that type-system proposals are much easier to evaluate when accompanied with formal type rules. It's not just a macho thing -- it really helps in debugging the dark corners. Simon | -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of | Claus Reinke | Sent: 26 February 2006 16:28 | To: haskell-prime@haskell.org | Subject: overlapping instances and constraints | | | the point about overlapping instances is that they shouldn't, | so we are looking for ways to resolve what looks like overlaps | unambiguously, so that there are no overlapping instances left. | | we don't want overlapping instances in the language definition, | but we do want more expressive means of defining non- | overlapping instances. | | 1. resolving overlaps in favour of the most specific declaration | does so, so why is that approach slated as "adopt: probably no"? | | http://hackage.haskell.org/trac/haskell-prime/ticket/54 | | 2. FDs can help to make types in instance declarations more | specific, thus avoiding some overlaps or at least helping the | "best-match" to resolve overlaps. defaults resolve some of | the simplest overlaps (which instance of Num did you mean?), | but not others, because their overloading is not expressed in | terms of classes (which empty list did you mean?). | | 3. in this context, could someone please remind me what exactly | is the reason that class constraints in instance declarations are | ignored when deciding whether two instances overlap? | | we have two worlds to consider, the unconstrained world of | semi-decidable type class programming, and the restricted | world which guarantees termination of type class inference. | | in the first world, it seems there is no reason not to look at | the constraints, because there are no termination guarantees | anyway. and in the second world, it seems there is no reason | not to look at the constraints, because we know that doing | so will terminate nicely, thank you. | | so why are some instance declarations still rejected as | overlapping even if their constraints clearly say they don't? | | cheers, | claus | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://haskell.org/mailman/listinfo/haskell-prime
[ 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").
Hello Claus, Monday, February 27, 2006, 4:10:00 PM, you wrote: CR> class C a where c :: a -> String CR> instance C [a] | a/=Char where c as = .. -- dealing with most lists CR> instance C String where c s = .. -- special case for strings i had plans to propose the same and even more: instance C2 a b | a/=b -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Mon, Feb 27, 2006 at 05:09:30PM +0300, Bulat Ziganshin wrote:
i had plans to propose the same and even more:
instance C2 a b | a/=b
I was thinking it would be all kinds of useful if we had two predefined classes class Eq a b class NEq a b where Eq has instances exactly when its two types are equal and NEq has instances exactly when its two types are not equal. Eq should be straightforward to implement, declaring any type automatically creates its instances. (sort of an auto-deriving). NEq might be more problematic as that would involve a quadratic number of instances so its implementation might need to be more special. but perhaps we can do with just 'Eq'. John -- John Meacham - ⑆repetae.net⑆john⑈
Hello John, Tuesday, February 28, 2006, 4:23:24 AM, you wrote:
i had plans to propose the same and even more:
instance C2 a b | a/=b
JM> I was thinking it would be all kinds of useful if we had two predefined JM> classes JM> class Eq a b JM> class NEq a b JM> where Eq has instances exactly when its two types are equal and NEq has JM> instances exactly when its two types are not equal. JM> Eq should be straightforward to implement, declaring any type JM> automatically creates its instances. (sort of an auto-deriving). NEq JM> might be more problematic as that would involve a quadratic number of JM> instances so its implementation might need to be more special. but JM> perhaps we can do with just 'Eq'. with 'Eq' class we can't do anything that is impossible without it :))) the whole devil is to make general instance NON-OVERLAPPING with specific one by EXPLICITLY specifying EXCLUSIONS with these "/=" rules: class Convert a b where cvt :: a->b instance Convert a a where -- are we need Eq here? :) cvt = id instance (NEq a b) => Convert a b where cvt = read.show ... yes, i recalled! my proposal was to allow "!" in instance headers: instance C Int where ... instance (!Int a, Integral a) => C a where ... instance (!Integral a, Enum a) => C a where ... adding your Eq class, it will be all we can do on this way interesting, that the language theoretics can say about decidability, soundness, and so on of this trick? :) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
instance C2 a b | a/=b
I was thinking it would be all kinds of useful if we had two predefined classes
class Eq a b class NEq a b
where Eq has instances exactly when its two types are equal and NEq has instances exactly when its two types are not equal.
class Eq a b instance Eq a a class NEq a b instance Fail a => NEq a a instance NEq a b class Fail all -- no instances I think I first saw that class Fail trick in an HList talk. but having those instances doesn't help if they are not used (eg, by following instance constraints, to aid in overlap resolution, or to confirm FDs; or simply because the system doesn't use the fact that Fail never has instances). Even just extending Eq/NEq to type-level predicates (with a 3rd, functionally dependent parameter) runs into trouble. I'd prefer to extend the language so that those uses become expressible, but for the short term, it'd be nice if the predicates _and_ their uses were built-in. hence the special syntax to indicate that this predicate is actually looked at when checking the instance. cheers, claus
Eq should be straightforward to implement, declaring any type automatically creates its instances. (sort of an auto-deriving). NEq might be more problematic as that would involve a quadratic number of instances so its implementation might need to be more special. but perhaps we can do with just 'Eq'.
John
-- John Meacham - ⑆repetae.net⑆john⑈ _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Hello Claus, Tuesday, February 28, 2006, 1:54:25 PM, you wrote: CR> class NEq a b CR> instance Fail a => NEq a a CR> instance NEq a b i think that this definition just use ad-hoc overlapping instances resolution mechanism that we want to avoid :))) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On 2/28/06, Bulat Ziganshin
Tuesday, February 28, 2006, 1:54:25 PM, you wrote: CR> class NEq a b CR> instance Fail a => NEq a a CR> instance NEq a b
i think that this definition just use ad-hoc overlapping instances resolution mechanism that we want to avoid :)))
Actually, it illustrates beautifully why ad-hoc overlapping doesn't
work. There are two interpretations, the desired one, and one that
just ignores the the first and uses the second for everything.
--
Taral
Tuesday, February 28, 2006, 1:54:25 PM, you wrote: CR> class NEq a b CR> instance Fail a => NEq a a CR> instance NEq a b
i think that this definition just use ad-hoc overlapping instances resolution mechanism that we want to avoid :)))
I don't want to avoid it completely, I want to give it more specifics to work with. but yes, type inequality would avoid many overlaps. the example was just meant to demonstrate the programmers could already specify their intention in current Haskell, by using Eq/NEq (in instance constraints), but it wouldn't be much use as long as current Haskell implementations ignore those intentions.
Actually, it illustrates beautifully why ad-hoc overlapping doesn't work. There are two interpretations, the desired one, and one that just ignores the the first and uses the second for everything.
I'm not sure what you're talking about? both hugs and ghc clearly specify that the more specific instance declaration is chosen when overlapping instance declarations are permitted. the repeated a makes the first declaration more specific, so both hugs and ghc accept the attached code, and deliver the same result, as specified. [if only that could be said for all programs, Haskell' could be built on much safer grounds, and everybody happier:-] overlapping resolution by choosing the most specific instance is no more black art than pattern-matching resolution by choosing the first match - some would say, less so. cheers, claus
On 2/28/06, Claus Reinke
I'm not sure what you're talking about? both hugs and ghc clearly specify that the more specific instance declaration is chosen when overlapping instance declarations are permitted.
I have trouble with this "more specific" term. It's not well-defined,
i.e. not a total order on possible instance declarations.
The point I was trying to make was that in the case where a
precondition (in this case, Fail a) does not apply, what stops the
resolution algorithm falling back on the other instance declaration?
--
Taral
both hugs and ghc clearly specify that the more specific instance declaration is chosen when overlapping instance declarations are permitted.
I have trouble with this "more specific" term. It's not well-defined, i.e. not a total order on possible instance declarations.
The point I was trying to make was that in the case where a precondition (in this case, Fail a) does not apply, what stops the resolution algorithm falling back on the other instance declaration?
preconditions (instance constraints) are not taken into account in best-fit overlap resolution. the ordering is plain substitution: instance A is more specific than instance B if there is a (non-empty) substitution that can be applied to make B's head identical to A's. where that is not possible, the overlapping declarations are not accepted. see, eg.: http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions.htm... in that sense, the flag name -fallow-overlapping-instances is slightly misleading, because it really only permits a subset of overlaps - ones that can be resolved unambiguously, using a substitution ordering of the instance heads. it is always clear which instance to choose - no search, no backtracking. cheers, claus ps people, including me, have argued the instance context ought to be taken into account. but again, that doesn't need to lead to much search - most of us would be happy if instance contexts would be required to uniquely determine the instance to be chosen, a rather conservative extension of current practice. that is because we often use a pair of instance declarations where the context for one includes the negation of some of the context in the other - they are mutually exclusive, so everything is happily deterministic, but the implementation does not notice..
Claus Reinke wrote:
most of us would be happy if instance contexts would be required to uniquely determine the instance to be chosen, a rather conservative extension of current practice.
How would that work? There's no way to prove that instance (Num a) => Foo a where ... instance Foo Char where ... don't overlap, because there's no way to know what instances of Num might be declared in other modules. If you reason based on what's in scope, you end up with the same problems that Simon detailed for overlapping instances. I can't think of any situation where the context could safely be used to resolve overlap except for a class private to the current module whose instances are locally constrained, but that doesn't seem like it would be very useful. -- Ben
Claus Reinke wrote:
most of us would be happy if instance contexts would be required to uniquely determine the instance to be chosen, a rather conservative extension of current practice.
I'm not so sure about the "most of us", as you note yourself the defaulting pattern is quite popular (and useful). I certainly couldn't live without it. And even that aside, I'd much rather have the type system infer a "most particular" instance than to have to specify that myself. Also IMHO, adding a new construct (type (in)equality) to the language is a lot more obtrusive than to do something meaningful of the constructs that the language already provides. So I'd have issues with "conservative" as well... Of course, this is all from the perspective of a user, not a type inference engine implementor... ;-) /Niklas
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
Simon Peyton-Jones wrote:
- 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
- Haskell would need to be a lot more specific about exactly where context reduction takes place.
I think all of these problems would go away if overlap was permitted within a module but forbidden across modules. Are there uses of overlapping instances for which this isn't flexible enough? -- Ben
On 2/28/06, Ben Rudiak-Gould
Simon Peyton-Jones wrote:
- 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
- Haskell would need to be a lot more specific about exactly where context reduction takes place.
I think all of these problems would go away if overlap was permitted within a module but forbidden across modules. Are there uses of overlapping instances for which this isn't flexible enough?
Certainly! In HSP [1] there is a class (simplified here) class IsXML xml where toXML :: xml -> XML data XML = Element .... | CDATA String that deals with how things should be represented as XML. There are a number of basic instances for this, such as instance IsXML String where toXML = CDATA instance (Show a) => IsXML a where toXML = toXML . show The intention of the latter is to be a default instance unless another instance is specified. These instances can be found in the base HSP module, but the idea is that HSP users should be able to work with their own datatypes and only need to define the translation into XML via instanciating IsXML. This would have to be done in the user modules, so overlap across module boundaries are essential for this to work. :-) /Niklas [1] http://www.cs.chalmers.se/~d00nibro/hsp/
Niklas Broberg wrote:
Ben Rudiak-Gould wrote:
Are there uses of overlapping instances for which this isn't flexible enough?
Certainly!
Hmm... well, what about at least permitting intra-module overlap in Haskell' (and in GHC without -foverlapping-instances)? It's good enough for many things, and it's relatively well-behaved.
instance (Show a) => IsXML a where toXML = toXML . show
The intention of the latter is to be a default instance unless another instance is specified.
I can see how this is useful, but I'm surprised that it's robust. None of the extensions people have suggested to avoid overlap would help here, clearly. Are there uses of overlapping instances for which the single-module restriction isn't flexible enough, but extensions that avoid overlap are flexible enough? -- Ben
Hello Ben, Wednesday, March 1, 2006, 6:23:00 PM, you wrote:
instance (Show a) => IsXML a where toXML = toXML . show
The intention of the latter is to be a default instance unless another instance is specified.
BRG> I can see how this is useful, but I'm surprised that it's robust. None of BRG> the extensions people have suggested to avoid overlap would help here, clearly. no problem: precedence 1 : instance (Show a) => IsXML a where ... precedence 9 : instance IsXML String where ... of overlapping instances, win the one with higher precedence -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Ben Rudiak-Gould wrote:
I think all of these problems would go away if overlap was permitted within a module but forbidden across modules. Are there uses of overlapping instances for which this isn't flexible enough?
I dislike this on principle. I like the idea that modules can be refactored easily. But I'm not a big fan of overlapping instances anyway, and don't turn on the option. This makes it easier to reason about instances, as they always apply to their complete domains. I'm much more interested in allowing non-overlapping instances such as: class C a instance C Bool instance (Num a) => C a However, I'm aware this is hard for the type-checker. In general, I think there's a consensus on what the type-checker should allow in a perfect world (assuming one has made a decision on whether to allow overlapping instances etc.). It seems the problem is how much of perfection can be implemented. It might be worth collecting examples of "things that don't compile but should" on a HaskellWiki page.
there were a couple of issues Simon raised that I hadn't responded to in my earlier reply. since no-one else has taken them on so far, either, ..
- Haskell would need to be a lot more specific about exactly where context reduction takes place. Consider f xs x = xs == [x] Do we infer the type (Eq a) => [a] -> a -> Bool? Thereby committing to a particular choice of instance? Or do we (as GHC does) infer the type (Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type Char, then an instance Eq [Char] instance would apply. GHC is careful to do the latter.
my general idea about that would be never to commit unless we know it is the only choice. which seems to be in line with what GHC is doing in this case. of course, it follows that we'd like to be able to specify choices unambiguously, to avoid delayed committs.
Concerning using the instance context, yes, it's attractive, but it involves *search* which the current mechanism does not. Presumably you have in mind that the type system should "commit" only when there is only one remaining instance declaration that can fit. You need to be very careful not to prune off search branches prematurely, because in a traditional HM type checker you don't know what all the type are completely. And you need to take functional dependencies into account during the search (but not irrevocably). I have not implemented this in GHC. I don't know anyone who has. I don't even know anyone who has specified it.
search, yes, but with deterministic result (similar to HM inference). so the main issue is that we need to be able to perform inferences without committing to their conclusions, or setting up encapsulated inference processes with their own assumptions. which isn't surprising given that we're dealing with implications, or type class functions, where the usual proof rule is "if we can prove the conclusions assuming the prerequisites, then we have proven the implication". that may be substantially more complicated to implement, but is just what Prolog, or even simple HM type inference for functions, have been doing for a long time. and it is a pain to see the current situation, where Haskell implementations treat the conclusions as if there were no pre-requisites (Haskell: these instances are overlapping; Programmer: no, they are not, just look at the code!). can we agree, at least in principle, that in the long term this needs to change? since the general implementation techniques aren't exactly new, are there any specific reasons why they couldn't be applied to type classes? we'd have a state for the constraint store, and a backtracking monad with deterministic result for the inference, just as we have for implementing HM inference. if we want a more efficient, more low-level implementation, we could use the WAM's idea of variable trails (proceed as if there was no search, but record all variable substitutions, so that we can undo them if it turns out that this branch fails). or is there a pragmatic issue with current implementations of those type classes, having grown out of simpler type class beginnings, and having grown so complex that they couldn't go in that direction without a major rewrite? in the short term, I'd be quite willing to aim for a compromise, where we'd not look at all constraints in the context, but just at a few specific ones, for which we know that the search involved will be very shallow. whether to do that via strictness annotations in contexts, as Bulat has suggested, or by reserving a separate syntactic position for constraints known to have shallow proofs, is another question. the outstanding example of this would be type inequalities, which I'd really like to see in Haskell', because they remove a whole class of instance overlaps. and with FDs, one can build on that foundation. I'm not sure I have a good handle on understanding when or how searches could be hampered by incomplete types. naively, I'd expect residuation, ie, delaying partially instantiated constraints until their variables are specific enough to proceed with inference. I think CHR already does this. if that means that instance context constraints cannot be completely resolved without looking at concrete uses of those instances, then we'd have a problem, but no more than at the moment. and I suspect that problem will not be a showstopper. on the contrary, it may help to keep those searches shallow. from my experience, it seems quite possible to arrange instance contexts in such a way that even such incomplete resolution will be sufficient to show that they ensure mutual exclusion of their instances (type inequality, type-level conditional, FDs, closed classes, ..). which would be all that was needed at that point. once we start looking, we could probably find more ways to help such incomplete inferences along. eg, if there was a built-in class Fail a (built-in only so that the system could know there can be no instances), then we could declare mutual exclusion like this: instance (Num a, Function a) => Fail a [an exclusion which, incidentally, some folks might disagree with;-] and, independent of the specific a, just by looking at the classes mentioned in the instance context, and the instances visible in the current module, the system could infer that the following instance constraints are mutually exclusive, hence the instances cannot be overlapping: instance (Num a,..other constraints..) => MyClass a where .. instance (Function a, .. other constraints..) => MyClass a where.. Oleg, eg, has shown how such is-a-function constraint could be used to solve several problems, but his code depends on ghc-specific tricks from HList, iirc. cheers, claus
- Haskell would need to be a lot more specific about exactly where context reduction takes place. Consider f xs x = xs == [x] Do we infer the type (Eq a) => [a] -> a -> Bool? Thereby committing to a particular choice of instance? Or do we (as GHC does) infer the type (Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type Char, then an instance Eq [Char] instance would apply. GHC is careful to do the latter.
is there actually anything unusual about this example? you're saying that there are at least two instances for Eq: instance Eq a => Eq [a] instance Eq [Char] and best-fit overlap resolution demands that we never apply the first if the second fits, too. we just can't apply any rules unless we have established that there are no more specific rules. GHC enables overlap resolution on a pre-module basis, Hugs on a per-session basis, so this means that we can never apply any rules unless they have ground heads (no variables), or we've seen the whole program. which is somewhat of an obstacle, suggesting that we would want to be more specific about enabling overlap resolution, and use any trick we know to figure out when we no longer have to wait for further, more specific instances (or be content to delay most of instance inference to the compilation of Main). in "functional logic overloading", POPL 2002, Neubauer et al suggested to enable overlap resolution on a per-class basis, which seems sensible. even enabling overlap on a per-instance basis might be worth looking into (that is, we would annotate those non-ground instance declarations which we want to be allowed to be overridden by more specific declarations elsewhere). with such finer control, all unannotated instances/classes might become fair game for earlier rule applications. we can further limit the scope of overlaps by using the module system to close a set of class instances (this is useful independent of overlaps, as it allows us to infer when there will be no instance for a given constraint): a set of instances for a class is closed if the class is neither exported nor imported, and if, for any instances with instance contexts, the context constraints are closed as well. [if the class isn't available outside this module, there can't be any direct instances outside, and if the instance context constraints are closed as well, there can't be any indirect instances generated from outside (*)]. of course, simply annotating a class or class export as "closed", and letting the compiler ensure that there are no further direct instances, would be somewhat simpler. I'm not sure what to do about further indirect instances in this case? cheers, claus (*) what do I mean by indirect instances: module A () where { class Closed a; instance X a => Closed a} module B where { import A; instance X t } even if Closed is not exported, creating instances for X indirectly creates instances for Closed.
participants (9)
-
Ashley Yakeley -
Ben Rudiak-Gould -
Bulat Ziganshin -
Claus Reinke -
John Meacham -
Martin Sulzmann -
Niklas Broberg -
Simon Peyton-Jones -
Taral