Simple logical unification in Haskell / a really terrible datalog system. It appears to work!

unification.hs

import Data.Maybe (isNothing)
import Data.Monoid ((<>))
import Data.List (nub, union)
import Control.Monad (forM_)

-- * The propositional language

-- | Term grammar
data Term
    = V Int  -- ^ Variable with unique numeric identifier
    | K String  -- ^ A constant value (strings for simplicity)
    | L [Term]  -- ^ A list of 'Term's
    deriving (Eq, Show)

-- | A list of variable-value bindings that have been deduced
newtype Frame = Frame {
    getBindings :: [ (Term, Term) ]
    } deriving (Show, Eq)

instance Monoid Frame where
    mempty = Frame []
    Frame l1 `mappend` Frame l2 = Frame $ l1 <> l2

-- | A rule says that the head 'Term' (the left-hand side) is true if all of the
-- body 'Term' values (the right-hand side) are also true.
-- A fact is a rule with an empty body, not a separate type.
data Rule = Term :- [ Term ]
    deriving (Eq, Show)

-- * Unification

-- | Uses a given frame to unify two terms, augmenting the frame
unify :: Term -> Term -> Maybe Frame -> Maybe Frame
unify p1 p2 frame
    | isNothing frame = Nothing -- stop if we've already failed
    | p1 == p2        = frame -- tautology
    | otherwise       = go p1 p2 frame
    where
        -- If either of the terms are variables unify them as such
        go p1@(V _) p2 frame = unify_var p1 p2 frame
        go p1 p2@(V _) frame = unify_var p2 p1 frame

        -- Two constants must be equal to unify
        go p1@(K _) p2@(K _) frame
            | p1 == p2 = frame
            | otherwise = Nothing

        -- A list cannot unify with a constant
        -- (we have already ruled out p1 as a variable)
        go _ p2@(K _) _ = Nothing

        -- Two lists unify if their members recursively unify
        go p1@(L (x1:xs1)) p2@(L (x2:xs2)) frame =
            unify (L xs1) (L xs2) $ unify x1 x2 frame

-- | Attempts to unify two variables as one given a frame
unify_var :: Term -> Term -> Maybe Frame -> Maybe Frame
unify_var var val frame
    | var == val = frame
    | otherwise = case bindingInFrame var frame of
          -- The variable isn't bound yet.
          Nothing -> if occurs_check var val frame
                        then addBinding var val frame
                        else Nothing

          -- The variable is already bound. Check its value.
          Just val' -> unify val' val frame

-- | Prevents unifying a variable with a term containing it.
-- The result says whether or not the terms pass the check, NOT whether the
-- first term occurs in the second.
occurs_check :: Term -> Term -> Maybe Frame -> Bool
occurs_check var@(V x) val frame = go val where
    go (K _) = True
    go p@(V _)
        | var == p = False
        | otherwise = case bindingInFrame p frame of
              Nothing -> True
              Just v' -> go v'
    go (L (x:xs)) = and [go x, go (L xs)]
    go (L []) = True

-- | Checks for the existence of a variable in the head of a 'Rule'
variableInHead :: Rule -> Bool
variableInHead ((L h) :- _) = or $ map check h
    where check (V _) = True
          check _       = False
variableInHead ((V _) :- _) = True
variableInHead _ = False

-- | Generate new facts from a list of rules and a list of facts.
forwardChain :: [ Rule ] -> [ Rule ] -> [ Rule ]
forwardChain [] fs = fs
forwardChain rs fs =
    if length newFacts > 0
        then forwardChain rs (newFacts `union` fs)
        else filter (not . variableInHead) fs
    where
        newFacts = filter (\n -> not (elem n fs)) $
            nub $
            concatMap (\r -> consequences r fs) rs

-- | Given a rule and some foldable container of facts, generate any new facts
-- as a consequence of applying this rule
consequences :: Rule -> [ Rule ] -> [ Rule ]
consequences (_ :- []) facts = facts
consequences r fs = go r fs [] where
    go (_ :- []) _ newFacts = newFacts
    go (h :- (b:bs)) facts newFacts = concatMap
        (\(fact :- _) -> case unify b fact (Just mempty) of
                --Nothing -> go (h :- bs) facts newFacts
                Nothing -> [] -- I think the previous line was wrong
                Just fr -> case apply fr (h :- bs) of
                    f@(_ :- []) -> go f facts $ nub $ f : newFacts
                    r           -> go r facts newFacts
        ) facts

-- | Use a frame to substitute any variables with known constants
apply :: Frame -> Rule -> Rule
apply (Frame bindings) ((L h) :- bs) = (L (map check h)) :- go where
    go = map L $ map (map check) bs'
    bs' = map (\(L x) -> x) bs
    check item = case lookup item bindings of
        Just val -> val
        Nothing -> item

-- | Determines if a term is bound in a given frame.
bindingInFrame :: Term -> Maybe Frame -> Maybe Term
bindingInFrame x (Just (Frame xs)) = lookup x xs
bindingInFrame _ Nothing = Nothing

-- | Binds two terms in a frame.
addBinding :: Term -> Term -> Maybe Frame -> Maybe Frame
addBinding var val (Just (Frame xs)) = Just . Frame $ (var, val) : xs
addBinding var val _ = Just . Frame $ [(var, val)]

-- * Examples

test_1 = unify
    (L [K "F", V 4, K "b"])
    (L [K "F", K "5", K "b"]) $ Just mempty

-- Abner is Betty's parent, Betty & Billy are Charles' parents
facts = [ L [ K "parent", K "abner", K "betty" ] :- []
        , L [ K "parent", K "betty", K "charles" ] :- []
        , L [ K "parent", K "billy", K "charles" ] :- []
        ]

-- You're an ancestor of someone if you are their parent
-- You are also an ancestor if you are an ancestor of their parent

rules =  [ L [ K "ancestor", V 1, V 2] :- [ L [ K "parent", V 1, V 2 ] ]
         , L [ K "ancestor", V 1, V 2] :- [ L [ K "parent", V 1, V 3 ]
                                          , L [ K "ancestor", V 3, V 2 ] ] ]

cool_rule = L [ K "cool", V 1 ] :-
            [ L [ K "has_a_bike", V 1 ]
            , L [ K "has_shades", V 1 ] ]

cool_facts = [ L [ K "has_a_bike", K "gatlin" ] :- []
             , L [ K "has_a_bike", K "kyle" ] :- []
             , L [ K "has_shades", K "kyle" ] :- [] ]

-- these are problematic but they were tested examples from
-- http://cs.nyu.edu/faculty/davise/ai/datalog.html
ruler_rules =
    [ L [ K "father", V 1, V 2 ] :- [ L [ K "parent", V 1, V 2 ]
                                    , L [ K "male", V 1 ] ]
    , L [ K "parent", V 1, V 2 ] :- [ L [ K "father", V 1, V 2 ] ]
    , L [ K "male", V 1 ] :- [ L [ K "father", V 1, V 2 ] ]
    , L [ K "mother", V 1, V 2 ] :- [ L [ K "parent", V 1, V 2 ]
                                    , L [ K "female", V 1 ] ]
    , L [ K "parent", V 1, V 2 ] :- [ L [ K "mother", V 1, V 2 ] ]
    , L [ K "female", V 1 ] :- [ L [ K "mother", V 1, V 2 ] ]
    , L [ K "parent", V 2, V 1 ] :- [ L [ K "child", V 1, V 2, V 3 ] ]
    , L [ K "parent", V 3, V 1 ] :- [ L [ K "child", V 1, V 2, V 3 ] ]
    , L [ K "child", V 1, V 2, V 3] :- [ L [K "son", V 1, V 2, V 3 ] ]
    , L [ K "male", V 1 ] :- [ L [ K "son", V 1, V 2, V 3 ] ]
    , L [ K "son", V 1, V 2, V 3 ] :- [ L [ K "male", V 1 ]
                                      , L [ K "child", V 1, V 2, V 3 ] ] ]

ruler_facts = [ L [ K "male", K "philip" ] :- []
              , L [ K "female", K "elizabeth" ] :- []
              , L [ K "son", K "charles", K "philip", K "elizabeth" ] :- [] ]

main = do
    forM_ (forwardChain rules facts) $ putStrLn . show
    putStrLn . show $ test_1
    forM_ (forwardChain [cool_rule] cool_facts) $ putStrLn . show
    putStrLn "***"
    forM_ (forwardChain ruler_rules ruler_facts) $ putStrLn . show