Re: overlapping instances and constraints
- 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.
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
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
Re: overlapping instances and constraints
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
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. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
On 2/28/06, Ben Rudiak-Gould [EMAIL PROTECTED] wrote: 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/ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
RE: overlapping instances and constraints
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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: overlapping instances and constraints
[ 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 Stringwhere 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
Re: overlapping instances and constraints
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⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
