What is "prolog style" in Scala?

Here is a basic correspondence to get you started:

• Prolog-Atoms correspond to ordinary types.
• Prolog-Variables correspond to type parameters.
• What's called "Functors" here corresponds to type constructors.
• Stating facts corresponds to providing constant givens.
• Making queries corresponds to summoning corresponding proof-terms.

Let's start with a very simple example where we have just one atom, one prolog-"functor", one fact, and one query: this example from Wikipedia

cat(tom).
?- cat(tom).
>> Yes

can be directly translated into

trait Tom     // Atom 'Tom'
trait Cat[X]  // Functor 'Cat' with arity = 1

// Fact: cat(tom).
given Cat[Tom] with {}

// Query: ?- cat(tom). (is Tom a Cat?)
val query = summon[Cat[Tom]] // type-checks = Yes

Prolog rules correspond to parameterized given-definitions, the antecedents on the right side correspond to the using-parameters in the parameter list. For example, the classical syllogism example expressed in Prolog as

man(socrates).
mortal(X) :- man(X).
?- mortal(socrates).
>> True

can be encoded with a parameterized given that uses Man[X] and produces a proof of Mortal[X]:

trait Socrates
trait Man[X]
trait Mortal[X]

given socratesIsAMan: Man[Socrates] with {}
given allMenAreMortal[X](using m: Man[X]): Mortal[X] with {}

val query = summon[Mortal[Socrates]]

You can use scala3-compiler -Xprint:typer to see the composite proof term that the compiler generated to prove that Socrates is Mortal:

allMenAreMortal[Socrates](socratesIsAMan)

Knowing how to encode rules allows you to encode the more complicated example from the Wikipedia:

mother_child(trude, sally).
 
father_child(tom, sally).
father_child(tom, erica).
father_child(mike, tom).
 
sibling(X, Y)      :- parent_child(Z, X), parent_child(Z, Y).
 
parent_child(X, Y) :- father_child(X, Y).
parent_child(X, Y) :- mother_child(X, Y).

?- sibling(sally, erica).
>> Yes

as follows:

trait Trude
trait Sally
trait Tom
trait Erica
trait Mike

trait FatherChild[F, C]
trait MotherChild[M, C]
trait ParentChild[P, C]
trait Sibling[X, Y]

given MotherChild[Trude, Sally] with {}
given FatherChild[Tom, Sally] with {}
given FatherChild[Tom, Erica] with {}
given FatherChild[Mike, Tom] with {}
given [X, Y, Z](using pczx: ParentChild[Z, X], pczy: ParentChild[Z, Y])
  : Sibling[X, Y] with {}

given fatherhoodImpliesParentship[X, Y](using fc: FatherChild[X, Y])
  : ParentChild[X, Y] with {}

given motherhoodImpliesParentship[X, Y](using mc: MotherChild[X, Y])
  : ParentChild[X, Y] with {}

val query = summon[Sibling[Erica, Sally]] // Yes

Here, the compiler will generate a proof term that explains that Erica and Sally are Siblings because they have the same father Tom:

given_Sibling_X_Y[Erica, Sally, Tom](
  fatherhoodImpliesParentship[Tom, Erica](given_FatherChild_Tom_Erica),
  fatherhoodImpliesParentship[Tom, Sally](given_FatherChild_Tom_Sally)
)

More generally, conjunctions are encoded by multiple using-parameters, and disjunctions are encoded by multiple givens with the same result type:

// We can write "X /\ Y" as infix operator for conjunction
case class /\[A, B](a: A, b: B)

// We can write "X \/ Y" as infix operator for disjunctions
enum \/[+A, +B]:
  case Inl(a: A)
  case Inr(b: B)

// Inference for conjunctions: multiple parameters in `using`
given [A, B](using a:A, b: B): (A /\ B) = /\(a, b)

// Inference for disjunctions: multiple rules
given [A](using a: A): \/[A, Nothing] = \/.Inl(a)
given [B](using b: B): \/[Nothing, B] = \/.Inr(b)

// Example:
trait X
trait Y
trait Z
trait W
given X with { override def toString = "X" }
given W with { override def toString = "W" }

@main def query(): Unit =
  println(summon[(X \/ Y) /\ (Z \/ W)])
  // Finds a proof and prints `/\(Inl(X), Inr(W))`.

Since Scala 3, there is even negation available through util.NotGiven:

import scala.util.NotGiven

trait X
trait Y
trait /\[X, Y]

given X with {}
given [A, B](using a: A, b: B): /\[A, B] with {}

// Fails if we add `given Y with {}`
val query = summon[X /\ NotGiven[Y]]

Scala 3 adds a whole bunch of stuff on top of that, such as tuples (which are basically type-level lists) or computing with numeric / boolean / string singleton types, but I don't want to go too deeply into the details here.

Instead, I'd like to conclude by briefly sketching how it all fits into the landscape. The interesting difference between Prolog and Scala's type system is that the Scala compiler actually generates proof terms, and unlike in Prolog (where you get a simple "Yes"/"No"), those proof terms can carry around arbitrarily complicated computational content.

You might have noticed that in the examples above, the with {} mostly remained empty. This is usually not the case in the real code, quite the contrary: in the real code, you usually have some non-trivial definitions in the body of every given ... with { ... }. The reason why one is writing all those facts and inference rules is not for solving logical puzzles and obtaining "Yes" / "No" answers, but for generating huge complicated proof terms that do useful stuff.

The way it works is usually as follows:

• Suppose you want to obtain a thing X
• You import some big-&-smart library that knows how to construct a variety of things similar to the desired X
• You use the "predicates" ( = typeclasses) / facts / rules ( = givens) of that library to express very precisely the properties that you want the thing X to have
• If your description is precise enough, the library & the Scala compiler is able to summon the thing X purely from its type description.

So, in your average programming language, you have to write out all the terms manually. In Scala 3, you can instead specify the desired properties of the desired term through types, and the compiler will use this Prolog-like term inference system to summon a term with the right properties (given the right libraries, that is).