the MPTC Dilemma (please solve)
ross at soi.city.ac.uk
Sun Feb 19 20:33:01 EST 2006
On Sat, Feb 18, 2006 at 12:26:36AM +0000, Ross Paterson wrote:
> Martin Sulzmann <sulzmann at comp.nus.edu.sg> writes:
> > Result2:
> > Assuming we can guarantee termination, then type inference
> > is complete if we can satisfy
> > - the Bound Variable Condition,
> > - the Weak Coverage Condition,
> > - the Consistency Condition, and
> > - and FDs are full.
> > Effectively, the above says that type inference is sound,
> > complete but semi-decidable. That is, we're complete
> > if each each inference goal terminates.
> I think that this is a little stronger than Theorem 2 from the paper,
> which assumes that the CHR derived from the instances is terminating.
> If termination is obtained via a depth limit (as in hugs -98 and ghc
> -fallow-undecidable-instances), it is conceivable that for a particular
> goal, one strategy might run into the limit and fail, while a different
> strategy might reach success in fewer steps.
Rereading, I see you mentioned dynamic termination checks, but not
depth limits. Can you say a bit more about termination? It seems to
be crucial for your proofs of confluence.
More information about the Haskell-prime