the MPTC Dilemma (please solve)
claus.reinke at talk21.com
Mon Mar 20 09:59:16 EST 2006
> As understand it, you've proposed changes in context reduction to
> restore confluence:
> 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:
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
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.
More information about the Haskell-prime