Suggestion: refine overlap handling for instance declarations
overlapping instances with best-fit overlap resolution are useful because they give us an alternative way to write programs that we cannot write directly as long as current Haskell isn't expressive enough: (a) we can't specify that two types in an instance are not equal; but we can use overlap resolution to ensure that equal types are handled by another, more specific instance (b) we can't enable library users to add instances for their types, yet ensure that there will be some instance for every type; but we can use overlap resolution to provide a default instance, to be overridden by more specific instances in library and user code (c) we can't rely on mutual exclusion properties specified in instance contexts to be used to select the appropriate instance because Haskell only looks at instance heads; but we can sometimes wrap our types in extra constructors so that the mutual exclusion is reflected in more and less specific instance heads, with overlap resolution choosing the right one (this is a real pain, brittle against change, and not always possible..) (d) ..this seems to cover most uses discussed so far, but I don't claim this list to be complete. if you know of examples not covered by a-c, please add them by reply! there hasn't been any enthusiasm about changing (c) for Haskell', which isn't to my liking, but nothing I can do much about. I would, however, like to continue arguing in favour of refining overlap handling until we get at least some progress into Haskell' (and addenda). so I propose to add the something like the following to Haskell': ---------- we know how to handle (a) [no overlap needed]: syntax: permit type inequalities as guards in instance declarations: <topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>] <ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>] semantics (sketch): - add inequality guards from an instance as guards to the rules for that instance in the CHR - add inequality guards as attributes to the typevars after successful guard evaluation and rule commit remarks: - we only need the extra guard syntax because of (c) above - we restrict inequalities to variables on lhs to simplify semantics - attributed variables are logic programming folklore: variable attributes are simply goals to be reexamined whenever the attributed variable is instantiated; we need them here to ensure that after we have selected a CHR rule based on an inequality, that inequality is not violated by later instantiations -------------------- we can make (b) more explicit: instead of enabling overlapping instances and overlap resolution on a per-module or per-session basis, we can specify which instances we want to use only as defaults: syntax: <topdecls> -> .. | ['default'] 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>] semantics (sketch): - default instances may be overridden by more specific instances including other default instances, but no such overlap is permitted unless there is a single most specific instance - default instances only apply if there can be no more specific instances; the easiest way to model this is by collecting all instances for the class, select those that are more specific than some default instance, and add type inequality guards that exclude those instantiations from the rule for the default instance - no other instances are affected by overlap resolution remarks: - by declaring all instances as 'default', we could recover the current, indiscriminate overlap handling; but we hardly ever want that, as declaring default instances allows us to be more precise, limiting the impact of overlap handling - once we have type inequality guards in the language, we can be a bit stricter about ruling out overlaps than GHC is at the moment (see Simon's earlier example) - default instances with ground heads (no variables) can be treated like non-default instances (there can't be any more specific instances) - without further analysis, application of default instances has to be delayed until the whole program is visible; that does not prevent separate compilation, it only prevents early application of some instances (those marked as defaults); in other words, separately compiled modules are parameterized by the set of more specific instances for their default instances - we don't want to go through all that trouble for every instance in every class, which is the motivation for being very specific about where we want overlaps to be permitted and resolved cheers, claus
Claus Reinke wrote:
overlapping instances with best-fit overlap resolution are useful because they give us an alternative way to write programs that we cannot write directly as long as current Haskell isn't expressive enough:
(a) we can't specify that two types in an instance are not equal;
but we can use overlap resolution to ensure that equal types are handled by another, more specific instance ...
permit type inequalities as guards in instance declarations:
<topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]
<ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>]
I'm afraid things might be a bit more complex. First of all, we may want several types of disequality (just as we want several equality relations on types). For example, let 'a' and 'b' be type variables. Does 'a' equal to 'b'? It depends. We may define two types t1 and t2 dis-equal if in any possible interpretation (for any assignment to type variables that may occur free in t1 and t2) the types are syntactically dissimilar. Under this definition, 'a' is not equal to 'b'. OTH, we may say that two types are disequal if there exists an interpretation (i.e., an assignment to type variables) that makes the types dissimilar. Both definitions can be useful, in different circumstances. Furthermore, sometimes we wish for a type equality constraint, sometimes we wish for a type equality predicate. The latter can be either total or partial. The type equality predicate typeEq in HList is partial: it can tell if two ground types are identical or not; in some situations, it can tell if two unground types are unequal (e.g., [a] is definitely not equal to Maybe a). OTH, it can't tell if [a] is equal to [a] -- until the type variable a is instantiated. For such unground types, the typeEq remains an unresolved constraint and floats out. Eventually the type variables get instantiated and the constraint is resolved. If they are not, we get the unresolved constraint type error (which often is the right thing). In addition to typeEq predicate (which instantiates no type variables), we often need (partial) type equality constraints that do instantiate type variables (typeCast in HList). The _full_ HList technical report discusses these issues in detail (Section 9 and Appendix D).
(a) we can't specify that two types in an instance are not equal;
but we can use overlap resolution to ensure that equal types are handled by another, more specific instance ... permit type inequalities as guards in instance declarations:
<topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]
<ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>]
first, I need to point out an oversight of mine here: restricting the lhs of inequalities to typevars was meant to simplify the semantics, but if we do that, we also need disjunctions of inequalities (eg, the negation of (a,b)==(Int,Bool) is (a/=Int || b/= Bool) ). that is not an unnatural requirement, but no longer simpler than just stating the full inequality ( (a,b)/=(Int,Bool) ). so I'm no longer sure which alternative to prefer?
I'm afraid things might be a bit more complex. First of all, we may
great, a second reader!-) about time that someone started to raise issues. that can only be helpful. yes, there are different variations on equality and disequality. your examples on equalities seem to hinge on the question of whether or not to permit substitutions, so we'd get unification (substitutions on both sides), matching (substitution on one side), equality (no substitutions). you also mention the possibility of asking for substitutions that make two types unequal (instead of asking for substitutions that make two types equal, then negating the result), but I'll take that as a general remark (useful when one needs to demonstrate that two terms are separable by substitution), not as something specifically relevant for the present context. for negated equalities, the difference between permitting or not permitting variable substitutions in the equality check is reversed: unification equates more terms than syntactic equality, so negated unification rejects more term pairs than negated syntactic equality. however, we also need to take into account that in our current context syntactic equality should cause residuation rather than giving the answer false for terms involving variables: - consider a/=Int (that is: not (a=Int)). with negated unification, this guard fails, because a could be instantiated to Int, so a rule with this guard won't apply. but if a is later instantiated to Bool by some FD, the guard becomes Bool/=Int, which succeeds, so the rule is now applicable. if a is instead instantiated to Int, the guard becomes Int/=Int, which fails. with negated equality, this guard cannot be decided, so the decision is delayed (residuation). if a is later instantiated to Bool, the guard is woken up, and succeeds, so the rule is now applicable. if a is instead instantiated to Int, the guard is woken up, and fails, so the rule is no longer applicable. - consider a/=b (that is: not (a=b)). with negated unification, this guard fails, because either variable could be instantiated to the other, so a rule with this guard won't apply. if the variables are instantiated later, the guard will change, and rule applicability changes. with negated equality, this guard cannot be decided, so the decision is delayed. if a or b are instantiated later, the guard is woken up, and retried. comparisons of more complicated structures reduce to these and ground comparisons. so it looks as if there isn't that much difference, but we need to be careful about when rules are suspended/woken up, or fail and are retried, and when guards are decided. so we certainly need to be careful about which disequality to choose as default, even if we are only interested in replacing overlaps. I'm not yet decided about which one is the "right" default for our problem. (of course, one might want to permit others, but I'm only looking for one at the moment;-).
variables. Does 'a' equal to 'b'? It depends. We may define two types t1 and t2 dis-equal if in any possible interpretation (for any assignment to type variables that may occur free in t1 and t2) the types are syntactically dissimilar. Under this definition, 'a' is not equal to 'b'. OTH, we may say that two types are disequal if there exists an interpretation (i.e., an assignment to type variables) that makes the types dissimilar. Both definitions can be useful, in different circumstances.
these two variations appear to be the same, though?
The _full_ HList technical report discusses these issues in detail (Section 9 and Appendix D).
and many other issues relevant to the present discussion. I've already referred to it as being full of examples illustrating why the current situation is unacceptable, and had been hoping that the authors would be among those arguing in favour of searching a more consistent picture here and now, avoiding the need for such hacks. after all, that's what you wrote at the end of Appendix D, two years ago!-) cheers, claus btw, said appendix D compares typeCast :: TypeCast a b => a -> b (with FDs: a ->b, b -> a) to foo :: a -> b foo x = x which might be slightly misleading in that the former does not have two independent type variables (once either is determined, the other is, too), and the second has a complete type declaration that conflicts with the inferred type (if, on the other hand, the type declaration was partial, it could be refined to the inferred type). apart from that, I'd agree with the argument: there is a difference between FDs excluding type errors a priori and FDs determining types that may or may not match with the actual types they are compared with. the latter is often more expressive/useful.
Hello Claus, Friday, March 17, 2006, 1:47:25 AM, you wrote: CR> - consider a/=Int (that is: not (a=Int)). CR> - consider a/=b (that is: not (a=b)). CR> comparisons of more complicated structures reduce to these CR> and ground comparisons. so it looks as if there isn't that much CR> difference, but we need to be careful about when rules are CR> suspended/woken up, or fail and are retried, and when guards CR> are decided. so we certainly need to be careful about which CR> disequality to choose as default, even if we are only interested CR> in replacing overlaps. may be we can solve all the problems just by using prolog-style programming, with unification and backtracking? at least type inference by itself is unification process. with overlapping instances it turns into the unification with backtracking, i'm right? type of function that is a part class interface can be also viewed as partially defined term. when we start unification process, we have partially defined terms, during the unification process we find a rule which allows to completely define all types involved. in this respect type class is just a Prolog-style relation: type Ref :: ( m :: Monad , r :: ** , newRef :: a -> m (r a) , readRef :: r a -> m a , writeRef :: r a -> a -> m () ) type Ref (IO, IOURef, newIOURef, readIOURef, writeIOURef) where Unboxed(a) Ref (IO, IORef, newIORef, readIORef, writeIORef) Ref (ST s, STRef s, newSTRef, readSTRef, writeSTRef) type specifications in first sentence define overall type structure of each function (i mean newRef/readRef/writeRef). instance declarations allow to find function implementations depending on context. so, in the following definition: test :: IO Int test = do x <- newRef 0 readRef x `readRef x` should return "IO Int", so we construct partially defined term and pass to the `Ref` relation (because readRef is a part of Ref definition). this term matches on the first line and gives us readRef = readIOURef x :: IOURef Int type of `x` determines result type of `newRef 0` expression, we again pass this type into the Ref relation and determine that newRef = newURef 0 :: Int we can write type functions what uses type relations (classes): type MonadRef :: Monad -> ** MonadRef m | Ref (m,r...) = r type function defined in this style can be used as any ordinal type constructor. data StrBuffer m = StrBuffer (MonadRef m Int) (MonadRef m String) this defines data structure that holds two references, to Int and String, mutable in monad 'm'. it seems that i written large text without much sense, but at least: 1) we can't live without unification, relations and backtracking. it will be great to define type computation rules just using Prolog's calculus. excluding for FDs, it seems that all we want to use just fit in this old and well-known computation model. 2) we want to see type functions and use type relations in them. it will be great to mix types and plain data in such definitions but that is more complex question. at least, we can work in type functions with type constructors (List in my first example). we can use classes as "types of types" 3) after all this syntax experiments i can propose continue to use type classes to define type relations, but allow to use plain values, type functions and predicates together with type classes in instance declarations: instance Binary Int where ... instance (Integral a, a/=Int) => Binary a where ... instance (Enum a, !Integral a) => Binary a where ... instance (Binary a) => Binary (MonadRef IO a) where ... instance (Binary a, r = MonadRef IO, r/=IORef) => Binary (r a) where ... instance (MArray a e IO) => Binary (MArray a e IO) where ... these instances can be seen as Prolog rules that direct the search. each type variable can be "free", "assigned", or "restricted". in the last case it contains the list of "prohibitions", i.e. values it CAN'T be assigned (a/=Int, a/=b, "!Integral a" and "!Ref m r" all lead to such prohibitions). when compiler tries to assign value to restricted type variable, it checks all the prohibitions associated with this variable. if all ok, the variable can be assigned new value. of course, when there is no variants, backtracking occurs and in appropriate points assignments and restrictions are cancelled. we can see instance searching as logical program with complete searching algorithm, while "-fallow-undecidable-instances" switches to depth-first searching algorithm. another idea - priority assigned to each instance. this priorities used to define search order for the depth-first algorithm. may be this algorithm should be enabled on each class individually? if any instance of this class includes "priority" clause then this algorithm should be used for this class. type functions still should be able to use classes as type relations: class Ref m r ... type MonadRef m | Ref m r = r -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
participants (3)
-
Bulat Ziganshin -
Claus Reinke -
oleg＠pobox.com