Note: some words can be hovered over! They don't have any different formatting from other things.

This is a simple? guide on understanding a very small implementation of Prolog in Haskell. I cannot be sure if this will be similar to any serious Prolog implementation, but I can tell you that this is based primarily off NanoProlog, with a touch of "prolog" , specifically for how Var's tags are built into the data itself "A Machine-Oriented Logic Based on the Resolution Principle" may or may not related to this.

To start off, we can first instantiate the data of some grammar in Prolog.

import qualified Data.Map as M

type Sym = String -- a symbol
data Term =
	Var Sym -- X, Hello
	| Fun Sym [Term] -- true, test(X, Y), bob
	deriving Eq
data Rule =
	Term -- head function; any head must be true for function to be
	:- [Term] -- clauses; all must be true for head to be
	deriving Eq
type Env = M.Map Sym Term -- variables, and what they stand for (bindings)
data Res =
	Yes Env -- goal is satisfied under these bindings
	| Do [(Rule, Res)] -- for each rule listed, using the rule...
	deriving Eq

Now, let's write our first function, subst. Given a binding environment and a term, it replaces all variables in the term with functions using the bindings. It does so as much as it can (so not simply looking it up once), and also recursively.

subst :: Env -> Term -> Term -- substitiution
subst e v@(Var x) = maybe v (subst e) (M.lookup x e)
subst e (Fun x cs) = Fun x (map (subst e) cs)

Since M.lookup is of type Maybe, we can use that to fall back in case of failure. This allows us to repeat lookups multiple times, so that the result, if it is there, is in a sense "atomic".

Next up is unify. Given two terms and a binding environment, it may, if the two terms could be equal to each other, create a new environment, adding the required bindings to do so.

import Data.Foldable (foldrM)

unify :: (Term, Term) -> Env -> Maybe Env
unify (t, u) e = subst e t ? subst e u where
	(?) :: Term -> Term -> Maybe Env
	Var x ? y = Just (M.insert x y e)
	x ? Var y = Just (M.insert y x e)
	Fun x xc ? Fun y yc
		| x == y && length xc == length yc
		= foldrM unify e (zip xc yc)
	_ ? _ = Nothing

Let me walk through this one.

1. Both terms are turned into a substituted form, so the function can deal with just free variables, so it can bind them.
2. If one of the terms is a variable, then it can be binded to the other term. If this is the case, an environment can be returned that is just the give one with the extra binding.
3. If both terms are the same function with the same amount of inputs, There is an attempt to unify each corresponding pair of arguments, and make sure they all are able to equal each other.
   • The action that foldrM (which actually uses foldl in its definition!) does is effectively:

     let [(a, a'), (b, b')...(y, y'), (z, z')] = zip xc yc in do
     	e0 <- unify (z, z') e
     	e1 <- unify (y, y') e0
     	...
     	e'1 <- unify (b, b') e'2
     	e' <- unify (a, a') e'1
     	e'

   • If any of the calls to unify inside of ? cannot return an environment, ? can't bind that argument, so it can't bind the function either.
4. If none of the above is true, then nothing else can be done, so an environment is not returned.

However, perhaps we want to make sure we don't get into infinite loops like:

X :- X.
f(X) :- f(f(X)).

(-?>) :: Sym -> Term -> Bool -- occurs-check (negated)
x -?> Var y = x /= y
x -?> Fun _ y = all (x -?>) y

unify :: (Term, Term) -> Env -> Maybe Env
unify (t, u) e = subst e t ? subst e u where
	(?) :: Term -> Term -> Maybe Env
	Var x ? y | x -?> y = Just (M.insert x y e)
	x ? Var y | y -?> x = Just (M.insert y x e)
	Fun x xc ? Fun y yc
		| x == y && length xc == length yc
		= foldrM unify e (zip xc yc)
	_ ? _ = Nothing

Now for the function with the biggest job: solve. Given a set of rules to use, a set of terms to prove, and a binding enviroment, If unify was the rising action, this is the climax.

import Data.Maybe (catMaybes)

solve :: [Rule] -> [Term] -> Env -> Res
solve _ [] e = Yes e
solve rs (t:ts) e = Do (catMaybes
	[(r,) . solve rs <$> unify (t, c) e | r@(c :- cs) <- rs])

This is really concise, so let's expand it.

solve :: [Rule] -> [Term] -> Env -> Res
solve _ [] env = Yes env
solve rules (term : rest_terms) env =
	Do [x | Just x <- [do
		new_env <- unify (term, head) env
		Just (this_rule, solve rules (body ++ rest_terms) new_env)
		| this_rule@(head :- body) <- rules]]

I think I will leave the understanding of this function as an exercise for the reader.

However, what I won't leave out is how there is a major flaw with how the program is currently written, back when M.insert was used. If a variable has the same name as a differently binded variable, which can happen for example in a recursive function, the newer variable overwrites the older variable.

To fix this, we use a different definition for variables, that uses "tags":

type Tag = Int
type VarD = (Sym, [Tag]) -- Var data
data Term = Var VarD | Fun Sym [Term] deriving Eq
type Env = M.Map VarD Term

class Tagged t where tag :: Tag -> t -> t -- variable renaming apart
instance Tagged Term where
	tag t (Var (x, y)) = Var (x, t:y)
	tag t (Fun x y) = Fun x (map (tag t) y)
instance Tagged Rule where tag t (c :- cs) = tag t c :- map (tag t) cs

solve :: [Rule] -> [Term] -> Tag -> Env -> Res
solve _ [] _ e = Yes e
solve rs (t:ts) tg e = Do (catMaybes
	[(r,) . solve rs (cs ++ ts) (succ tg) <$> unify (t, c) e | r@(c :- cs) <- map (tag tg) rs])

From this point, things calm down. Next is strip, which takes all the Yeses and compiles them, leaving just the variable bindings.

strip :: Res -> [Env]
strip (Yes y) = [y]
strip (Do x) = x >>= strip . snd

When the result is Do, it takes all the results that can follow, stripping them for environments, and combining the outputs together.

A set of shorthands can also be defined for using the main functions.

var x = Var (x, [])
sym x = Fun x []
fact x y = Fun x y :- []
query x y = solve x [y] 0 M.empty

Something can be noticed here: since any variable not provided by the user will be tagged at some point, that means that the user's variables can be identified by an empty tag list. We can write a function to show environments in a Prolog-like way using this, so that the user won't see any intermediate variables that were binded.

showEnv :: Env -> String
showEnv x = unlines ("YES":[v ++ " <- " ++ show (subst x (Var s)) | (s@(v, []), _) <- M.toList x])

Of course, in order to use this function, we need to write Show instances for some other datatypes first. Along the way, we can also write a function to sequence the strings into a sort of pager.

import Data.List (intercalate)

instance Show Term where
	show (Var (x, [])) = x
	show (Var (x, t)) = x ++ show t
	show (Fun x []) = x
	show (Fun x y) = x ++ '(' : intercalate ", " (map show y) ++ ")"
instance Show Rule where
	show (x :- y) = show x ++ " :- " ++ intercalate ", " (map show y) ++ "."
page :: [String] -> IO ()
page = foldr (\x -> (putStr x >> getLine >>)) (putStrLn "NO")

While I haven't implemented Read instances yet, at least we are now able to write programs in Prolog-like structures in Haskell!

rules = [
  fact "edge" [sym "a", sym "b"],
  fact "edge" [sym "b", sym "c"],
  Fun "path" [var "X", var "Y"] :- [Fun "edge" [var "X", var "Y"]],
  Fun "path" [var "X", var "Y"] :- [Fun "edge" [var "X", var "Z"], Fun "path" [var "Z", var "Y"]]
  ]
goal = Fun "path" [sym "a", var "X"]
solution = strip (query rules goal)
main = page (map showEnv solution)

~/bin/l/hs$ runghc PrologE.hs
YES
X <- b
Enter
YES
X <- c
Enter
NO
~/bin/l/hs$ 

And that's it! We have made a simple Prolog interpreter that safely handles variables, unifies, and solves for goals, in 100 lines!

~/bin/l/hs$ nl Prolog*

I have split the functions into two seperate files, and there are a few extra things in those version of the files I've written, so it's probably less for you.

One thing I haven't added is negation as failure, but I suppose I will add that when I revisit this.