the MPTC Dilemma (please solve)

[Claus Reinke]

> As understand it, you've proposed changes in context reduction to
> restore confluence:

yes.

> What is your plan to deal with non-termination (e.g. examples 6 and 16
> of the FD-CHR paper)?

I haven't read all the suggestions that Martin, you, and others have 
made in that area yet (still busy with overlaps), including those in the 
revised FD-CHR paper, so I can't make concrete suggestions yet, 
beyond those I've already posted here:

1 we all want terminating instance inference, but trying to assure that
    via restrictions is bound to be limiting (does GHC still have to build
    part of the hierarchical libs with -fallow-undecidable-instances?).

    I'm not opposed to it, but I'd like Haskell' to document current
    practice, in that we have the option to switch of termination checks
    whenever they are not able to see that our programs are terminating
    (available in Hugs and GHC, and all too often necessary).

2 that said, termination checks can do a lot, and it is certainly useful
    know various methods of checking terminations, as well as terminating
    examples beyond current termination checks.

    the old FD-CHR draft already discussed relaxed FD conditions,
    but was somewhat hampered because confluence checks seemed
    entangled with termination. with confluence problems out of the
    way, the restrictions can focus on termination. was there any other
    reason not to go for the relaxed FD conditions as a start?

3 in http://www.haskell.org//pipermail/haskell-prime/2006-February/000825.html

    I gave two examples that are terminating, but for which the
    current conditions are too restrictive. the first could be cured
    by taking "smaller" predicates into account, in addition to smaller
    types and smaller variable sets, and the second turned out to be 
    a special case of the relaxed coverage condition, I think. I run 
    into both problems all the time (the first is especially annoying as 
    it prevents calling out to simpler "helper" predicates..).

4 example 6, FD-CHR, is vector multiplication Mul. I argued that 
    it is wrong to call the declarations faulty and invalid just because
    there are some invalid calls. I also suggested one way in which
    the declarations can be permitted, while ruling out the faulty call:

    http://www.haskell.org//pipermail/haskell-prime/2006-March/000847.html

    basically, the idea is that FDs specify type-level functions, so
    unless we can demonstrate that those functions are non-strict, we
    need to rule out cyclic type-level programs that feed the range of
    an FD into one of its domain parameters, by a generalized occurs
    check.

    simply looking at the intersection of variables is easy to implement;
    that method is still too conservative (eg, if the range is simly a
    copy of the domain), but adding it to our repertoire of termination 
    checks definitely improves the situation, and is sufficient to permit
    the declarations in example 6, while ruling out the offending call.

5 example 16, CHR, defines an instance that hides an increasing
    type behind an FD. my intuition on that one tells me that we are
    again ignoring the functional character of FDs (as we did in 4). 
    
    instead of ruling out types determined entirely by FDs via the 
    bound variable restriction, as the paper suggests, we could 
    extend the termination check to collect information about 
    FDs. just think of type constructors as simple FDs and try 
    to treat real FDs similarly: 

    adding a constructor around a type variable in the context 
    means we cannot guarantee termination by reasoning about 
    shrinking types. determining a type variable in the context by
    putting it in the range of an FD means we cannot guarantee
    termination by reasoning about shrinking types, unless we
    have some conservative approximation of the relation 
    between domain and range of the FD to tell us so.

    the example case:

        class F a b | a-> b
        instance F [a] [[a]]

    clearly shows the range to be more complex than the domain,
    so we can account for that increase in complexity when we 
    see F t x in an instance context.

    if instead, we only had:

        class F a b | a->b
        instance F [[a]] [a]

    the range would be less complex than the domain, so we could
    permit use of this, even though the bound variable condition
    would treat it the same way - forbid it.

there are whole yearly workshops dedicated to termination.
we shouldn't assume that we can reach any satisfactory solution
by a mere handful of restrictions. which means that we need to
add to our repertoire of termination checks, and to keep open 
the option of switching of those checks.

cheers,
claus