[Haskell-cafe] embedding prolog in haskell.

[Christian Maeder]

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)