(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.
_______________________________________________
Haskell-prime mailing list
[email protected]
http://haskell.org/mailman/listinfo/haskell-prime
