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 [failP, cut, fruit, salty, fruitSalad2] ("fruitSalad" @ var "F") `shouldBe` []

-- * 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"])]

If we try to run it, we get the following failures:

 1) Prolog.hasGoal rule fact with cut-fail the arg should be invalid
      expected: False
       but got: True

 2) Prolog.runQuery rules facts, based on cut-fail and atom-based goal should be valid
      expected: []
       but got: [fromList [("F",TAtom "tomato")],fromList [("F",TAtom "melon")]]

The issue comes from the [] Monad instance which comes back to the last working State when an empty occurs.

To get around this, we need to introduce a dedicated type which keeps the last State, as follows:

data Stream s a
  = Nil s
  | Cons a s (Stream s a)

newtype Logic s a = Logic {runLogic :: s -> Stream s a}

In order to keep our current working we have to implement some of the instance StateT has, as follows:

evalLogic :: Logic State a -> State -> [a]
evalLogic (Logic m) s = extract (m s)
  where
    extract =
      \case
        Nil _ -> []
        Cons a _ rest -> a : extract rest

appendStream :: Stream State a -> Stream State a -> Stream State a
appendStream (Nil s) branchB
  | s.cutDepth >= s.depth = Nil s
  | otherwise = branchB
appendStream (Cons a s rest) branchB =
  Cons a s (appendStream rest branchB)

instance Functor (Logic State) where
  fmap f (Logic m) = Logic $ \s ->
    let go (Nil s') = Nil s'
        go (Cons a s' rest) = Cons (f a) s' (go rest)
     in go (m s)

instance Applicative (Logic State) where
  pure a = Logic $ \s -> Cons a s (Nil s)
  (<*>) = ap

instance Monad (Logic State) where

  Logic m >>= f = Logic $ \s ->
    let go (Nil s') = Nil s'
        go (Cons a s' rest) =
          appendStream (runLogic (f a) s') (go rest)
     in go (m s)

instance Alternative (Logic State) where
  empty = Logic Nil

  Logic m1 <|> Logic m2 = Logic $ \s ->
    appendStream (m1 s) (m2 s)

instance MonadPlus (Logic State)

Additionally, to have a total compatibility, we need MonadState and a way to inject lists, as follows:

instance MonadState State (Logic State) where
  get = Logic $ \s -> Cons s s (Nil s)
  put s' = Logic $ \_ -> Cons () s' (Nil s')

liftL :: (Foldable f, Alternative m) => f a -> m a
liftL = foldr (\x acc -> pure x <|> acc) empty

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