Prolog in Haskell - High-order predicates

In the previous log, our Prolog implementation has not only the expected behavior, but also some basic predicates which helps to implement cut-fail, but if we look at the following tests:

spec :: Spec
spec =
  describe "Prolog" $ do
    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` []

runQuery is not able to fetch matching values.

To supports this, we have to implement the negation (\+), which, given a goal, succeeds if the goal fails.

We can rework or logic as follows:

fruit(tomato).
fruit(melon).

salty(tomato).

fruits_salad(X) :- fruit(X), \+ salty(X).

Let's add more some tests as follows:

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

fruitSalad3 :: Predicate
fruitSalad3 =
  predicate "fruitSalad" (var "X", ["fruit" @ var "X", neg $ "salty" @ var "X"]) []

neg :: Goal -> Goal
neg g = "\\+" @ TGoal g

negateP is simple: attempts the goal, if it works, negation fails, otherwise, pass along the substitutions, as follows:

negateP :: Predicate
negateP = Predicate $ \ss ps (Goal gFunctor args) -> do
  guard (gFunctor == Atom "\\+")
  case eqTypeRep (typeOf args) (typeRep @Term) of
    Just HRefl ->
      case args of
        TGoal g' -> do
          s <- get
          if null $ evalLogic (query ss ps g') s
            then pure ss
            else empty
        _ -> empty
    Nothing -> empty

Prolog, at least in the standardized ISO version, has few other elements such as dynamic predicates (which is cool) or numbers.

Instead, to conclude the core-part of the series, we will turn our Prolog implementation in a second-order logic programming language.

It only takes the support of variables in the goal name as follows:

fruit(tomato).

% ?- P(tomato).
% P = fruit.

The first step toward is to change Goal to support both Atom and Var, as follows:

data Goal
  = forall args.
  (Args args) =>
  Goal
  { functor :: GoalName,
    arguments :: args
  }

data GoalName
  = GNAtom Atom
  | GNVar Var
  deriving stock (Eq)

Doing so will break compilation, as guard in Predicate use ==, instead we have to unify functor, and inject the result in substitutions, as follows:

matchFunctor :: Substitution -> Atom -> GoalName -> Logic State Substitution
matchFunctor ss t =
  \case
    GNAtom x -> guard (t == x) $> ss
    GNVar x ->
      case substitute ss (TVar x) of
        TVar v -> pure $ Map.insert v (TAtom t) ss
        TAtom a -> guard (t == a) $> ss
        _ -> empty

Finally, we have to propagate it in runQuery, as follows:

runQuery :: [Predicate] -> Goal -> [Substitution]
runQuery ps g@(Goal f gArgs) = ground <$> evalLogic  (query mempty ps g) initialState
  where
    functorVars =
      case f of
        GNVar v -> Set.singleton v
        GNAtom _ -> mempty
    ground ss = Map.fromSet (substitute ss . TVar) (functorVars <> vars gArgs)

In the next log, we will have a quick look at parsing.