Simple unification.

Test.hs

module Test where

import Unify

import Data.List
import Data.Maybe

atom :: String -> Term
atom t = Term t []

term :: String -> [Term] -> Term
term = Term

(===) :: Term -> Term -> Unify Term
(===) = unify

test0 :: Bool
test0 = isJust . eval $ do
    x <- fresh
    let a = term "a"
    let b = atom "b"
    r <- a [x, x, x] === a [b, b, b]
    apply r

test1 :: Bool
test1 = isJust . eval $ do
    x <- fresh
    y <- fresh
    z <- fresh
    x === y
    y === z
    z === x
    apply x

test2 :: Bool
test2 = isJust . eval $ do
    x <- fresh
    y <- fresh
    let a  = term "a" [atom "b"]
    let a' = term "a" [x]
    let b  = term "b" [x, y]
    let b' = term "b" [atom "b", atom "b"]
    a === a'
    b === b'
    apply b

test3 :: Bool
test3 = not . isJust . eval $ do
    x <- fresh
    let a = term "a"
    x === a [x, x]
    apply x

test4 :: Bool
test4 = not . isJust . eval $ do
    x <- fresh
    y <- fresh
    let a = term "a"
    let b = term "b"
    x === a [y, y]
    y === b [x]
    apply x

tests :: [Bool]
tests =
    [ test0
    , test1
    , test2
    , test3
    , test4
    ]

main :: IO ()
main =
    case findIndex not tests of
        Just i  -> putStrLn $ unwords ["Test", show i, "failed."]
        Nothing -> putStrLn $ "All tests were successful."

Unify.hs

module Unify where

import Control.Monad.State
import qualified Data.IntMap as IM

data Term
    = Term String [Term]
    | Var Int
    deriving Show

data Binding = Binding
    { next     :: Int
    , bindings :: IM.IntMap Term
    }

type Unify a = StateT Binding Maybe a

eval :: Unify a -> Maybe a
eval = (`evalStateT` Binding 0 IM.empty)

fresh :: Unify Term
fresh = do
    v <- next <$> get
    modify (\s -> s { next = v + 1 })
    return $ Var v

lookupVar :: Int -> Unify (Maybe Term)
lookupVar v = gets (IM.lookup v . bindings)

bind :: Int -> Term -> Unify ()
bind v t = modify (\s -> s { bindings = IM.insert v t (bindings s) })

occurs :: Int -> Term -> Bool
occurs v (Term t ts) = any (occurs v) ts
occurs v (Var v')    = v == v'

apply :: Term -> Unify Term
apply (Term t ts) = do
    ts <- traverse apply ts
    return $ Term t ts
apply (Var v) = do
    t <- lookupVar v
    case t of
        Just t -> do
            guard $ not (occurs v t)
            t <- apply t
            bind v t
            return t
        Nothing -> return $ Var v

unify :: Term -> Term -> Unify Term
unify t t' = do
    t  <- apply t
    t' <- apply t'
    case (t, t') of
        (Var v, Var v')
            | v == v' -> return $ Var v
        (Var v, t) -> do
            bind v t
            return $ Var v
        (t, Var v) -> do
            bind v t
            return $ Var v
        (t, t') -> match t t'

zipExact :: [a] -> [b] -> Unify [(a, b)]
zipExact [] []         = return []
zipExact (x:xs) (y:ys) = ((x, y) :) <$> zipExact xs ys
zipExact _ _           = mzero

match :: Term -> Term -> Unify Term
match (Term t ts) (Term t' ts') = do
    guard (t == t')
    ts <- zipExact ts ts'
    ts <- traverse (uncurry unify) ts
    return $ Term t ts
match t t' = unify t t'