Coverage is a sufficient condition to maintain termination. Though, Coverage is also sufficient to maintain confluence. Hence, we propose Weak Coverage which we know maintains confluence under some conditions. The main focus of the FD paper is how to restore confluence which is important for complete inference. We don't say much about termination (once Coverage is broken). Therefore, we either assume CHRs are terminating or check whether CHRs are terminating for a particular goal (e.g. by imposing a limit on the number of CHR steps). Hence, the inference methods in the FD paper are complete but semi-decidable. As you point out, Mul a (Vec b) b should be rejected, cause there can never by any ground instance, unless we allow for "infinite" types. Here's a more complicated example: Mul a (Vec b) c, Mul a (Vec c) b The cycle involves two constraints. Another one: Mul a (Vec b) c, Mul a (Vec c) d, Foo d b where rule Foo d b <==> d=b What I'm trying to demonstrate here is that only during inference (ie. applying CHRs) we may come across cycles. Hence, the quest is to come up with *dynamic* termination methods. I think that's what you are interested in? FYI, in a technical report version of the FD paper, we already address such issues, briefly. I believe there's a huge design space for dynamic termination methods. For example, in some email exchanges between Stefan Wehr, Oleg and myself on Haskell Cafe, we observed that some "simple" FD/AT programs were non-terminating. Non-termination wasn't due to "infinite types". No, types grew "bigger" due to improvement conditions which fired in between instance reduction steps. As in case of the Mul example, instances itself are terminating. I suggested some conditions which guarantee *static* termination. Though, this may rule out some reasonable programs (recall: the Mul example is also ruled out once we enforce Coverage). Hence, we need yet another kind of dynamic termination check. What's in there for Haskell'? The confluence story (i.e. complete inference) is fairly settled. Though, termination is still a very subtle problem, regardless whether we use FDs, ATs or whatever type class improvement mechanism. In fact, I don't think there will ever be a good answer to the termination problem unless we consider specific cases. Martin Claus Reinke writes:
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):1-54, 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 apparently-conservative rules is entirely non-trivial. It's one of those areas in which it is easy to suggest a plausible-sounding 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 plausible-sounding 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 non-terminating 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 non-termination.
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 non-terminating 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 non-terminating 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 occurs-checks (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 (non-productive) cyclic program at the type-level, 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=FD-Mul a b), then the constraint asks for:
b=FD-Mul a (Vec b))
which should trigger a (generalised, conservative) occurs-check error (pending more refined tests).
for the purposes of termination in this kind of example, the non-recursive 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 FD-C 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 non-terminating, whereas I think that generalising the standard occurs-check 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 type-level 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 best-fit 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
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime