[Haskell-cafe] My Unification Sorrows
procyon112 at gmail.com
Thu Apr 5 00:22:22 EDT 2007
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 <stefanor at cox.net> wrote:
> 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.".
More information about the Haskell-Cafe