relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[Martin Sulzmann]

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 at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime