the MPTC Dilemma (please solve)
ross at soi.city.ac.uk
Fri Feb 17 19:26:36 EST 2006
Martin Sulzmann <sulzmann at comp.nus.edu.sg> writes:
> - There's a class of MPTC/FD programs which enjoy sound, complete
> and decidable type inference. See Result 1 below. I believe that
> hugs and ghc faithfully implement this class.
> Unfortunately, for advanced type class acrobats this class of
> programs is too restrictive.
Not just them: monad transformers also fall foul of these restrictions.
The restrictions can be relaxed to accomodate them (as you do with the
Zip class), but the rules become more complicated.
> 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.
More information about the Haskell-prime