This solution is invalid for some edge cases.
Better than quickcheck, I can map eval across all possible trees of
depth n, since growFullTree returns a lazy list of all trees.
On 4/4/07, Stefan O'Rear
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