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

[Claus Reinke]

>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