Prolog in Haskell - Introduction and simple predicates

Nearly 15 years ago, I was waiting on my engineering school's front stairs, waiting for the bus.

I have used this time to start reading Prolog - Programmation par l'exemple, and I have found it beautiful.

Prolog is a 1970s' first order logic programming language.

The programming by itself has four terms:

• atoms: such as x, tomato, 'some atom'
• numbers
• variables: atom-like starting with an uppercase such as X, Fruit; they can be prefixed by _ to use it as placeholder, such as _Ingredient
• compound term: starts with an atoms called functor, and arguments, for example fruit(tomato); the number of arguments is called arity

By itself, Prolog is a fact database, they can be defined at the top-level as follows:

fruit(tomato).
fruit(melon).

sweet(melon).

We can also declare rules, implying other predicates (rules or facts), call goals, which should be true to make the rule true, as follows:

fruits_alad(X) :- fruit(X), sweet(x).

arity and predicate should match, for example sweet/1 and sweet/3 are two distinct predicates.

Once all predicates are set, we can query them, as follows:

?- fruit(tomato).
Yes

?- fruits_alad(tomato).
No

Prolog look up each predicate, from top to bottom, and left to right for the goals, until one is valid.

We can go further, asking open-ended questions:

?- fruits_alad(X).
X = melon

It works thanks to a process called unification, it enumerates all possible values.

Let's write a simple interpreter.

We will focus on atoms for the moment, we can define the following types:

newtype Atom
  = Atom {unAtom :: String}
  deriving stock (Eq, Ord, Show)

data Predicate = Predicate
  { functor :: Atom,
    arity :: Int,
    clauses :: NonEmpty ([Atom], [Goal])
  }

data Goal = Goal
  { functor :: Atom,
    arity :: Int,
    arguments :: [Atom]
  }

Sadly, [Atom] does not ensure the arity is matching, we can lift it to the type-level as follows:

data Predicate
  = forall (arity :: Nat).
  (Arity arity) =>
  Predicate
  { functor :: Atom,
    arityProxy :: Proxy arity,
    clauses :: NonEmpty (Args arity, [Goal])
  }

data Goal
  = forall (arity :: Nat).
  (Arity arity) =>
  Goal
  { functor :: Atom,
    arityProxy :: Proxy arity,
    arguments :: Args arity
  }

class (KnownNat a, Eq (Args a)) => Arity (a :: Nat) where
  type Args a :: Type

instance Arity 0 where
  type Args 0 = ()

instance Arity 1 where
  type Args 1 = Atom

instance Arity 2 where
  type Args 2 = (Atom, Atom)

instance Arity 3 where
  type Args 3 = (Atom, Atom, Atom)

The next step is to draft a runtime, we aim to evaluate only atoms, it should be simpler as we only have to find matching functor and arity, then do an equality check, as follows:

hasGoal :: [Predicate] -> Goal -> Bool
hasGoal ps (Goal gFunctor gArity gArgs) = any go ps
  where
    go (Predicate pFunctor pArity pClauses) =
      case eqTypeRep (typeOf gArity) (typeOf pArity) of
        Just HRefl
          | gFunctor == pFunctor ->
              any (\(cArgs, _) -> cArgs == gArgs) pClauses
        _ -> False

We can add some tests to ensure this, as follows:

spec :: Spec
spec =
  describe "Prolog" $ do
    it "atom-based facts and atom-based should be valid" $
      hasGoal [fruit] (Goal (Atom "fruit") (Proxy @1) (Atom "tomato")) `shouldBe` True
    it "atom-based facts and atom-based should be invalid" $
      hasGoal [fruit] (Goal (Atom "fruit") (Proxy @1) (Atom "carrots")) `shouldBe` False

fruit :: Predicate
fruit =
  Predicate
    { functor = Atom "fruit",
      arityProxy = Proxy @1,
      clauses = (Atom "tomato", []) :| [(Atom "melon", [])]
    }