Suggestion: refine overlap handling for instance declarations

Thu Mar 16 17:47:25 EST 2006

>>     (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.