On Wed, Apr 04, 2007 at 07:16:35PM -0700, Paul Berg wrote: > I believe I may have found a solution (I *think* it's correct): > > The occurs check needs to stay, but be modified for infinite types. > When the occurs check is true, instead of failing, we should keep the > constraint, but skip performing substitution on the rest of the list > of constraints. This allows us to not fall into the trap of an > infinite substitution loop. So, unify becomes, in the case of > infinite types: > > -- | Given a list of constraints, unify those constraints, > -- finding values for the type variables > unify :: (Monad m, Functor m) => [Constraint] -> m [Constraint] > unify [] = return [] > unify ((t1 , t2) :rest) > | t1 == t2 = unify rest > unify ((tyS, tyX@(TVar _)) :rest) > -- | tyX `occursIn` tyS = fail "Infinite Type" > | tyX `occursIn` tyS = fmap ((tyX,tyS):) (unify rest) > | otherwise = fmap ((tyX,tyS):) (unify > $ substinconstr tyX tyS rest) > unify ((tyX@(TVar _), tyT) :rest) = unify $ (tyT,tyX) : rest > unify ((tyS1 :-> tyS2,tyT1 :-> tyT2):rest) = unify $ (tyS1,tyT1) : > (tyS2,tyT2) : rest > unify _ = fail "Unsolvable"
I honestly don't understand the algorithm. (And I don't have tapl!!) So, ... quickcheck! You've seen my occurs-free unifier; now write an Arbitrary instance for trees and check that they always give the same result. "The chance of a common bug is neglible.". Stefan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe