I have code that successfully detects illegal behavior and refuses to compile when I give incompatible combinations of string-literal encoded types, but only when those types are predefined as variables. When they are inlined at the same site, the code compiles and no errors are reported.
I’m attempting to model propositional logic on the type level. Scastie. Scastie - An interactive playground for Scala.
We model propositions with an OO hierarchy
Proposition
├── Atomic(String)
├── Negation(Proposition)
└── Compound(Proposition, Proposition)
├── Implication
├── Disjunction
└── Conjunction
abstract class Proposition:
val expression: String
case class Atomic(expression: String) extends Proposition
abstract class Compound extends Proposition:
val left: Proposition
val right: Proposition
val operation: "∧" | "⋁" | "->"
val expression = s"${left.expression} ${operation} ${right.expression}"
case class Implication(left: Proposition, right: Proposition) extends Compound:
val operation = "->"
case class Disjunction(left: Proposition, right: Proposition) extends Compound:
val operation = "⋁"
case class Conjunction(left: Proposition, right: Proposition) extends Compound:
val operation = "∧"
case class Negation(proposition: Proposition) extends Proposition:
override val expression = s"¬(${proposition.expression})"
And inference rules as functions of (Proposition, Proposition) -> Proposition.
Previously, I was implementing these inference rules through runtime checks, as most simple logic solvers do – they consisted of if statements that would optionally return some derived conclusion or none if it was being misapplied
def modusponens(p1: Proposition, p2: Proposition): Option[Proposition] =
p1 match
case p1: Implication =>
if p2 == p1.left then
Some(p1.right)
else None
case _ => None
While this does make brute-forcing all possible conclusions easier (you can throw any two propositions into modusponens and see if it returns something) I felt it was less correct definitionally. This approach allows you to call modusponens in nonsensical scenarios.
Instead, I want the domain and range of inference rules to be dependently typed, such that they are guaranteed by the compiler to be correct before they are allowed to be called, removing any need for runtime checks. Once you have written p -> q for the first proposition, the only acceptable second proposition - per the definition of modus ponens - is p, and the return type is guaranteed to be q.
I can successfully do this for the most part. I encode the string literal that each Atomic proposition represents as part of the type, using String & Singleton, such that every wrapped expression is considered it’s own distinct type, which is then also captured by all Compound propositions upwards as Left and Right generic arguments.
case class Atomic[S <: String & Singleton](expression: S) extends Proposition
val p = Atomic("p")
// p: Atomic["p"]
val q = Atomic("q")
// q: Atomic["q"]
case class Implication[L <: Proposition, R <: Proposition](
left: L, right: R
) extends Compound
val p1 = Implication(p, q)
// p1: Implication[Atomic["p"], Atomic["q"]]
val p2 = Atomic("p")
// p2: Atomic["p"]
Now the inference rules no longer have any need for runtime checks, as the types contain all the information needed. They can be defined simply in terms of the form (shuffling leftside/rightside elements) as pure transformations, which I think is a more faithful implementation.
def modusponens[L <: Proposition, R <: Proposition](
p1: Implication[L, R], p2: L
): R =
p1.right
val p1 = Implication(Atomic("p"), Atomic("q"))
val p2 = Atomic("p")
val conclusion = modusponens(
p1,
p2
)
// conclusion: Atomic["q"]
A neat result of this is that the compiler and IDE will stop you if you even attempt to apply modusponens incorrectly, real-time feedback as you write.
val p1 = Implication(Atomic("p"), Atomic("q"))
val p2 = Atomic("q") // <- now q, fallacy of affirming the consequent
val conclusion = modusponens(
p1,
p2 // Error! Expected Atomic("p"), not Atomic("q")
)
However, the problem I’ve found is that this behavior stops working if you attempt to inline the arguments
// inline
val conclusion = modusponens(
Implication(Atomic("p"), Atomic("q")),
Atomic("q") // should error. does not. Code compiles
)
// predefined
val a = Implication(Atomic("p"), Atomic("q")),
val b = Atomic("q")
val conclusion_ = modusponens(
a,
b // error as expected.
)
And I’m not sure why. It seems like the literal type resolution is only able to occur when they are split up into separate toplevel value definitions which is disappointing.
Is it a limitation of Scala, or intended behavior? Is it specific to how I’m working with string literals & Singleton? Is it possible to fix this to get my desired behavior?
