relaxed instance rules spec (was: the MPTC Dilemma (please
solve))
Claus Reinke
claus.reinke at talk21.com
Wed Mar 1 22:53:45 EST 2006
>I urge you to read our paper "Understanding functional dependencies via
>Constraint Handling Rules", which you can find here
>http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/.
Simon,
I had already read that paper briefly, but had moved on to scan some
of the other publications in that area (ats, ..), because I was unhappy
with its limitations, omissions, and what I perceived as overly quick
conclusions. I have now returned to it, and although I still haven't
read it in full, I see that my misgivings were mostly the result of
impatience  it may not be the final word, but, together with:
P. J. Stuckey and M. Sulzmann. A theory of overloading. ACM
Transactions on Programming Languages and Systems (TOPLAS),
27(6):154, 2005.
it does provide a good, and necessary start, and a useful basis for
discussions.
[may I suggest a reference section on the main Haskell' page, listing
these and other important inputs to difficult Haskell' issues?]
>It will tell you more than you want to know about why relaxing
>apparentlyconservative rules is entirely nontrivial. It's one of
>those areas in which it is easy to suggest a plausiblesounding
>alternative, but much harder to either prove or disprove whether the
>alternative a sound one.
what I've read so far tells me less than I want to know, exactly
because I think more relaxations are necessary, but are left for
future work. also, while it is true that plausiblesounding variations
may lead to surprising results, it is unfortunately also true that the
first explanation of such surprises isn't always the best one.
case in point: you replied to my suggestion to relax the coverage
condition to a recursive coverage condition, and the paper you
refer to contains an example which seems to demonstrate that
this wouldn't be safe (example 6):
class Mul a b c  a b > c where..
instance Mul Int Int Int where ..
instance Mul a b c => Mul a (Vec b) (Vec c) where ..
this looks terminating, because it recurses down a finite type in
its second parameter, but it violates the coverage condition in
the second instance, where c is not in {a,b}. as I've argued
in my message, I'd like to think of recursive coverage here,
because c is covered via the FD in the recursive call.
now, the paper presents an example expression that leads
to the following constraint, with a nonterminating inference:
Mul a (Vec b) b {b=Vec c}> Mul a (Vec c) c
and the paper claims that this is a direct consequence of the
violation of the coverage condition!
so, one of us is wrong, either my "plausibility" argument for
recursive coverage, or the paper's claim that recursive coverage
(or, for that matter, any relaxation of coverage that would
permit that instance declaration) leads to nontermination.
but note that the paper says "direct consequence", not
"necessary consequence", and whether or not my informal
argument can be proven, if you just read it side by side with
the nonterminating inference in question, you'll see
immediately that the paper is jumping to conclusions here
(or at least leading the reader to such jumps..):
 Mul recurses down a type in its second parameter
 types in Haskell are finite
 there is a nonterminating Mul inference
the problem is that we have somehow conjured up an infinite
type for Mul to recurse on without end! Normally, such infinite
types are ruled out by occurschecks (unless you are working
with Prolog III;), so someone forgot to do that here. why?
where? how?
well, there is that functional dependency that says that parameters
a and b are inputs and parameter c is an output of Mul, and there
is that initial constraint that says that b contains c! we have managed
to write a (nonproductive) cyclic program at the typelevel, and
while each recursive step strips one layer of its second input, it
also refines it to include an extra layer, via the output and cycle!
imho, the instance is okay, but the constraint should be rejected
because if we write the FD as a function call with result
(c=FDMul a b), then the constraint asks for:
b=FDMul a (Vec b))
which should trigger a (generalised, conservative) occurscheck
error (pending more refined tests).
for the purposes of termination in this kind of example, the
nonrecursive coverage condition appears to be an (overly
conservative) approximation. in fact, even the generalised occurs
check may be overly conservative (a functional dependency is
not a type constructor, so the result of FDC a b may not even
include both a and b).
the paper does discuss this as the (refined) weak coverage
condition, with stronger constraints for confluence (fulfilled here),
and under assumption of other termination proofs (theorem 2).
unfortunately, it still assumes that example 6 is nonterminating,
whereas I think that generalising the standard occurscheck to
account for FDs gives a simple way to dispell that myth.
so, I'll stick to my suggestion, on the grounds that barring cyclic
typelevel programs there are no expressions of infinite types in
Haskell. but I'm open to arguments!)
cheers,
claus
 2. the coverage condition only refers to the instance head. this
 excludes programs such as good old record selection (which
 should terminate because it recurses over finite types, and is
 confluent in fact deterministic because of bestfit overlap
 resolution):

   field selection
 infixl #?

 class Select label val rec  label rec > val where
 (#?) :: rec > label > val

 instance Select label val ((label,val),r) where
 ((_,val),_) #? label = val

 instance Select label val r => Select label val (l,r) where
 (_,r) #? label = r #? label

 now, it is true that in the second instance declaration, "val" is
 not covered in {label,(l,r)}. however, it is covered in the recursive
 call, subject to the very same FD, if that recursive call complies
 with the (recursive) coverage criterion. in fact, for this particular
 task, that is the only place where it could be covered.

 would it be terribly difficult to take such indirect coverage (via
 the instance constraints) into account? there'd be no search
 involved (the usual argument against looking at the constraints),
 and it seems strange to exclude such straightforward "consume
 a type" recursions, doesn't it?

 cheers,
 claus
More information about the Haskellprime
mailing list