On Sat, Feb 18, 2006 at 12:26:36AM +0000, Ross Paterson wrote: > Martin Sulzmann <[EMAIL PROTECTED]> 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. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
