Unification Algorithm in Haskell

Unifier.hs

module Main where

import Data.List (intersperse)

type Name = String
type Equations = [(Expr,Expr)]

data Expr
  = Func Name [Expr] -- if [Expr] is [], then it's a constant
  | Var Name
  deriving (Eq)

instance Show Expr where
  show (Var name) = name
  show (Func name []) = name
  show (Func name args) = concat $ [ name, "(", shownArgs, ")"]
    where shownArgs = concat $ intersperse "," $ map show args

{-
  The unification algorithm from wikipedia:
  - https://en.wikipedia.org/wiki/Unification_(computer_science)
  - we ought to change this to return a Maybe or an Either or Failure
-}
unify :: Equations -> Equations
unify eqns = unify' [] eqns
  where -- here we use g, a set of equations we have already transformed
        -- to accumulate the result
    -- delete
    unify' g ((t1, t2) : xs)
      | t1 == t2 = unify' g xs
    -- decompose
    unify' g ((Func name1 args1, Func name2 args2) : xs)
      | name1 == name2 && length args1 == length args2
          = unify' g $ (args1 `zip` args2) ++ xs
    -- conflict
      | otherwise = [] -- fail, function names or arg lengths don't match
    -- swap
    unify' g ((f@(Func _ _), v@(Var _)) : xs) = unify' g ((v,f) : xs)
    -- eliminate
    unify' g ((Var x, t) : xs)
      | not (x `elem` vars t) = unify' ((Var x, t) : subst x t g) (subst x t xs)
    -- check
    unify' g ((Var x, t@(Func _ _)) : xs)
      | x `elem` vars t = []
    -- does this next case ever actually happen? (Var x, Var y), so yes
    unify' g (x : xs) = unify' (x : g) xs -- do we recycle x for later?
    unify' g [] = g

subst :: Name -> Expr -> Equations -> Equations
subst x t = map substPair
  where substPair (ex1, ex2) = (subst' ex1, subst' ex2)
        subst' (Func name exps) = Func name (subst' `map` exps)
        subst' (Var name)
          | x == name = t
          | otherwise = Var name

vars :: Expr -> [Name]
vars (Func _ exprs) = exprs >>= vars
vars (Var name) = [name]

main :: IO ()
main = do putStrLn $ display exampleInput
          putStrLn " -> "
          putStrLn $ display $ unify exampleInput
  where exampleInput = [(Func "list" [Var "y"]   , Var "x"),
                        (Func "list" [lit "int"] , Var "x"),
                        (Func "f" [Var "z", Func "g" [Var "w"]],
                          Func "f" [lit "1", Func "g" [Var "z" ]])]

        lit n = Func n []
        display = let displayEqn (g,h) = (show g) ++ " = " ++ (show h)
                  in concat . intersperse "\n" . map displayEqn