Keean Schupke wrote: > implementation of unify? For example can the algorithm be simplified > from my nieve attempt? Most importantly is it correct?
It will not be correct without occurs check. You may also get different terms for the same variable in your substitution list. The simplest form of unification does not take a substitution as input and uses functions to compose two substitutions and to apply a substitution to a term. > unify :: Subst -> (Term,Term) -> [Subst] Do you ever get real lists? The result type "Maybe Subst" is more appropriate. > unify' s [] [] = [s] > unify' s (t0:ts) (u0:us) = case unify s (t0,u0) of > s@(_:_) -> unify' (concat s) ts us > _ -> [] input lists of different lengths should not cause a runtime error but only a unification failure (indicated by "Nothing" or "[]" in your case.) HTH Christian Here's a part of my version: unify' (t0:ts) (u0:us) = do s1 <- unify (t0,u0) s2 <- unify' (map (applySubst s1) ts) (map (applySubst s1) us) return (composeSubst s1 s2) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe