Martin Sulzmann <[EMAIL PROTECTED]> 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. > 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. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
