Prolog in Haskell - Unification-related predicates

In the previous log, we have reached a basic naive Prolog implementation, but Prolog comes with predicates changing/impacting the unification:

• fail/0 which make unification fail
• !/0, called cut, which freeze backtracking, all other clauses won't be evaluated

They are often used together, it's called cut-fail, for example, we can prevent salty-fruits salad as follows:

fruit(tomato).
fruit(melon).

sweet(melon).

salty(tomato).

fruits_salad(X) :- salty(X), !, fail.
fruits_salad(X) :- fruit(X), sweet(x).

We cannot implement these predicates directly as they have a different unification mechanism, we have to redefine Predicate to carry it, as follows:

newtype Predicate = Predicate (Substitution -> [Predicate] -> Goal -> Logic Substitution)

Names and arguments, if any, will be checked by the Predicate, which simplifies query as follows:

query :: Substitution -> [Predicate] -> Goal -> Logic Substitution
query ss ps g = do
  Predicate f <- lift ps
  f ss ps g

We have to move the rest of the logic in predicate, as follows:

predicate :: (Args args) => String -> (args, [Goal]) -> [(args, [Goal])] -> Predicate
predicate name firstClause otherClauses =
  Predicate $ \ss ps (Goal gFunctor gArgs) -> do
    guard (gFunctor == Atom name)

    freshnessIndex <- get
    put (freshnessIndex + 1)

    (rawArgs, rawBody) <- lift $ firstClause : otherClauses
    let cArgs = rename freshnessIndex rawArgs
        body  = map (renameGoal freshnessIndex) rawBody
        solveGoals :: Substitution -> [Goal] -> Logic Substitution
        solveGoals ss' =
          \case
            [] -> lift [ss']
            (g : gs) -> do
              ss'' <- query  ss' ps g
              solveGoals ss'' gs

    case eqTypeRep (typeOf gArgs) (typeOf cArgs) of
      Just HRefl -> do
        ssa <- lift $ maybeToList $ unify ss cArgs gArgs
        solveGoals (ss <> ssa) body
      Nothing -> lift []

The smart constructor here helps us to only have a local change, our tests are still passing!

Defining fail is as trivial as follows:

failP :: Predicate
failP =
  Predicate $ \_ _ (Goal gFunctor _) -> do
    guard (gFunctor == Atom "fail")
    empty

However !, cut, is a bit more involved, we have to track the current level of unification and the last "cut-level", it should be part of our state we can plainly define as follows:

type Logic = StateT State []

data State = State
  { freshness :: Int,
    depth :: Int,
    cutDepth :: Int
  }

initialState :: State
initialState =
  State
    { freshness = 0,
      depth = 0,
      cutDepth = -1
    }

nextFreshessIndex :: Logic Int
nextFreshessIndex = do
  s <- get
  put s {freshness = s.freshness + 1}
  pure s.freshness

Then, for each query, we have to:

• Check the depth against cutDepth (skip otherwise), increment depth, go through each clause, decrement depth as follows:

query :: Substitution -> [Predicate] -> Goal -> Logic Substitution
query ss ps g = do
  s <- get
  guard $ s.cutDepth < s.depth
  put s {depth = s.depth + 1}
  Predicate f <- lift ps
  ns <- f ss ps g
  s' <- get
  put s' {depth = s'.depth - 1}
  pure ns

Then, we can easily define cut as follows:

cut :: Predicate
cut =
  Predicate $ \ss _ (Goal gFunctor _) -> do
    guard (gFunctor == Atom "!")
    s <- get
    put s {cutDepth = s.depth}
    pure ss

We can add the following tests:

spec :: Spec
spec =
  describe "Prolog" $ do
    describe "hasGoal" $ do
      it "rule fact with cut-fail the arg should be valid" $
        hasGoal [failP, cut, fruit, salty, fruitSalad2] ("fruitSalad" @ atom "melon") `shouldBe` True
      it "rule fact with cut-fail the arg should be invalid" $
        hasGoal [failP, cut, fruit, salty, fruitSalad2] ("fruitSalad" @ atom "tomato") `shouldBe` False
    describe "runQuery" $ do
      it "rules facts, based on cut-fail and atom-based goal should be valid" $
        runQuery [fruit, failP, cut, fruitSalad2] ("fruitSalad" @ var "F") `shouldBe` [Map.singleton (Var "F") (atom "melon")]

-- * Fixtures

fruit :: Predicate
fruit =
  predicate "fruit" (atom "tomato", []) [(atom "melon", [])]

salad :: Predicate
salad =
  predicate "salad" (atom "melon", []) []

fruitSalad :: Predicate
fruitSalad =
  predicate "fruitSalad" (var "X", ["fruit" @ var "X", "salad" @ var "X"]) []

eq :: Predicate
eq =
  predicate "eq" ((var "X", var "X"), []) []

salty :: Predicate
salty =
  predicate "salty" (atom "tomato", []) []

fruitSalad2 :: Predicate
fruitSalad2 =
  predicate "fruitSalad" (var "X", ["salty" @ var "X", "!" @ (), "fail" @ ()]) [(var "X", ["fruit" @ var "X"])]

This is mostly it for our implementation, next time we will see "higher order predicates".