Applicative Calculi in Scala

In previous explorations, I described how the syntax of applicative calculi can be organized by magmas and catamorphisms. We saw that computation unfolds as a coalgebraic observation of states. We then stripped this down to a minimal, foundational perspective: a calculus is fundamentally a formal language, a sublanguage of reduced terms, and a partial reduction map.

But how do we formally translate between completely different computational universes—like moving from the single-combinator \(\iota\)-calculus to the full untyped \(\lambda\)-calculus—while preserving their mathematical structure? In this post, I will walk through a Scala framework to model the category of applicative calculi and the homomorphisms that bridge them.

The Algebraic Core

To formalize our calculi, we start with the core algebraic definition.

• An applicative language calculus is defined as a triple \(\mathcal{C}=(L,R,\beta)\).
• The component \(L\) is a pointed partial-magmatic language.
• The component \(R \subseteq L\) represents the pointed sublanguage of reduced terms.
• Finally, the map \(\beta: L \to R\) is a totalized reduction map.

The defining axiom for this map is its strict compatibility with application: reducing either input before forming an application must not change the reduced result. In other words, for any terms \(a, b \in L\), the partial expressions \(\beta(ab)\), \(\beta(\beta(a)b)\), \(\beta(a\beta(b))\), and \(\beta(\beta(a)\beta(b))\) must all be strongly Kleene equal. This referential transparency ensures that our evaluation logic is structurally sound.

Let us encode this universal evaluation engine in Scala. By defining a generic Calculus trait, we decouple the evaluation loop from the specific reduction rules of any given language.

trait Calculus:
  type Expr
  
  def app(left: Expr, right: Expr): Expr
  
  extension (left: Expr)
    def apply(right: Expr): Expr = app(left, right)
  
  def reduceStep(expr: Expr): Option[Expr]
  
  import scala.annotation.tailrec
  final def normalize(expr: Expr, depthLimit: Option[Int] = None): Option[Expr] =
    @tailrec def loop(current: Expr, currentDepth: Int): Option[Expr] =
      if depthLimit.exists(limit => currentDepth > limit) then None 
      else
        reduceStep(current) match
          case Some(next) => loop(next, currentDepth + 1)
          case None       => Some(current)

Syntax: Free Magmas and Abstract Grammars

Before we evaluate, we need syntax. The raw syntax of \(\lambda\)-terms before any notion of reduction can be modeled by the free magma freely generated by the set of atomic terms, and within this magmatic structure, the binary operation corresponds directly to application.

For combinatory logic, this is perfectly literal. SKI terms are the free magma on the three generators \(\{S, K, I\}\), and iota terms are the free magma on the single generator \(\{\iota\}\). By building off a generic FreeMagma, we can define both calculi simply by providing their alphabets.

Let us start with the free magma (binary trees):

enum FreeMagma[A]:
  case Leaf(value: A)
  case App(left: FreeMagma[A], right: FreeMagma[A])

Next, the SKI-calculus:

object SKICalculus extends Calculus:
  enum SKI:
    case S, K, I
    
  type Expr = FreeMagma[SKI]
  val S: Expr = FreeMagma.Leaf(SKI.S)
  val K: Expr = FreeMagma.Leaf(SKI.K)
  val I: Expr = FreeMagma.Leaf(SKI.I)
  
  def app(left: Expr, right: Expr): Expr = FreeMagma.App(left, right)
  def reduceStep(expr: Expr): Option[Expr] = expr match
    case FreeMagma.App(FreeMagma.Leaf(SKI.I), x) => 
      Some(x)
    case FreeMagma.App(FreeMagma.App(FreeMagma.Leaf(SKI.K), x), y) => 
      Some(x)
    case FreeMagma.App(FreeMagma.App(FreeMagma.App(FreeMagma.Leaf(SKI.S), x), y), z) => 
      Some(app(app(x, z), app(y, z)))
    case FreeMagma.App(left, right) =>
      reduceStep(left).map(app(_, right)).orElse(reduceStep(right).map(app(left, _)))
    case _ => None

And the \(\iota\)-calculus

object IotaCalculus extends Calculus:
  enum IotaGen:
    case Iota
    
  type Expr = FreeMagma[IotaGen]
  val i: Expr = FreeMagma.Leaf(IotaGen.Iota)
  
  def app(left: Expr, right: Expr): Expr = FreeMagma.App(left, right)
  def reduceStep(expr: Expr): Option[Expr] = None

However, the untyped \(\lambda\)-calculus is not simply a free magma; its abstract syntax tree consists of variables, abstractions, and applications. Because our Calculus trait leaves the Expr type abstract, we can seamlessly define LambdaCalculus with its own native grammar alongside our magmas.

object LambdaCalculus extends Calculus:
  enum LambdaExpr:
    case Var(name: String)
    case Abs(param: String, body: LambdaExpr)
    case App(func: LambdaExpr, arg: LambdaExpr)
    
  type Expr = LambdaExpr
  
  def app(func: Expr, arg: Expr): Expr = LambdaExpr.App(func, arg)

  private def freeVars(expr: Expr): Set[String] = expr match
    case LambdaExpr.Var(name) => Set(name)
    case LambdaExpr.Abs(param, body) => freeVars(body) - param
    case LambdaExpr.App(func, arg) => freeVars(func) ++ freeVars(arg)

  private def substitute(expr: Expr, target: String, replacement: Expr): Expr = expr match
    case LambdaExpr.Var(name) => 
      if name == target then replacement else expr
      
    case LambdaExpr.App(func, arg) => 
      app(substitute(func, target, replacement), substitute(arg, target, replacement))
      
    case LambdaExpr.Abs(param, body) =>
      if param == target then 
        // The bound variable shadows the target; do not substitute inside
        expr 
      else if freeVars(replacement).contains(param) && freeVars(body).contains(target) then
        // Name collision: α-rename the bound variable to a fresh name
        val freshParam = param + "'"
        val renamedBody = substitute(body, param, LambdaExpr.Var(freshParam))
        LambdaExpr.Abs(freshParam, substitute(renamedBody, target, replacement))
      else
        // Safe to substitute directly
        LambdaExpr.Abs(param, substitute(body, target, replacement))

  def reduceStep(expr: Expr): Option[Expr] = expr match
    // Beta Reduction
    case LambdaExpr.App(LambdaExpr.Abs(param, body), arg) => 
      Some(substitute(body, param, arg))
      
    // Evaluate the function position first
    case LambdaExpr.App(func, arg) =>
      reduceStep(func) match
        case Some(reducedFunc) => Some(app(reducedFunc, arg))
        case None => reduceStep(arg).map(app(func, _))
          
    // Evaluate inside abstractions
    case LambdaExpr.Abs(param, body) =>
      reduceStep(body).map(LambdaExpr.Abs(param, _))
      
    case _ => None

Homomorphisms Between Calculi

If we view calculi as objects in a category, we need morphisms to connect them. A morphism of behavioral applicative calculi must preserve the chosen reduction and the reduced applicative product up to behavioral equivalence. In simpler terms, a valid morphism between calculi must respect the reduced applicative structure.

We can define a generic Homomorphism trait that acts as a structural translation between any two calculi. By mapping the generators (or AST nodes) of the source calculus to valid expressions in the target calculus, we preserve the algebraic operations across the boundary.

trait Homomorphism[S <: Calculus, T <: Calculus](val source: S, val target: T):
  def apply(expr: source.Expr): target.Expr

Translating \(\iota\) to SKI

Mapping our pure IotaCalculus into SKICalculus space is a simple substitution of the generator, as \(\iota\) maps cleanly to a predefined SKI topological tree.

object IotaToSKI extends Homomorphism(IotaCalculus, SKICalculus):
  import SKICalculus.{S, K, I}
  
  def apply(expr: source.Expr): target.Expr = expr match
    case FreeMagma.Leaf(IotaCalculus.IotaGen.Iota) => 
      // The mathematical translation of ι into SKI: S (S I (K S)) (K K)
      S(S(I)(K(S)))(K(K))
      
    case FreeMagma.App(left, right) => 
      SKICalculus.app(this.apply(left), this.apply(right))

Translating \(\lambda\) to SKI (Bracket Abstraction)

Translating the \(\lambda\)-calculus to SKI is more complex. We use bracket abstraction, which translates lambda terms to SKI terms. Because \(\lambda\)-terms possess bound variables and pure SKI terms do not, we must algorithmically eliminate the variable bindings bottom-up. The bracket-abstraction theorem gives the exact comparison and equivalence between the two calculi.

To implement this safely in Scala, we use a private intermediate AST (SKIComp) that temporarily holds variables while the bracket abstraction eliminates them, before extracting the pure, variable-free SKI tree.

object LambdaToSKI extends Homomorphism(LambdaCalculus, SKICalculus):
  import LambdaCalculus.LambdaExpr
  import SKICalculus.{S, K, I, app}
  
  // 1. Intermediate AST to hold variables during bracket abstraction
  private enum SKIComp:
    case Comb(expr: SKICalculus.Expr)
    case Var(name: String)
    case App(left: SKIComp, right: SKIComp)
    
  private def freeVars(expr: SKIComp): Set[String] = expr match
    case SKIComp.Comb(_) => Set.empty
    case SKIComp.Var(name) => Set(name)
    case SKIComp.App(l, r) => freeVars(l) ++ freeVars(r)
    
  // 2. The Bracket Abstraction algorithm
  private def abstractVar(param: String, body: SKIComp): SKIComp = 
    if !freeVars(body).contains(param) then
      // If x is not free in M, return K M
      SKIComp.App(SKIComp.Comb(K), body)
    else body match
      case SKIComp.Var(name) if name == param => 
        // If M is just x, return I
        SKIComp.Comb(I)
      case SKIComp.App(l, r) => 
        // If M is (U V), return S (abstract U) (abstract V)
        SKIComp.App(SKIComp.App(SKIComp.Comb(S), abstractVar(param, l)), abstractVar(param, r))
      case _ => 
        throw new IllegalStateException("Invalid state in bracket abstraction")

  // 3. Compile Lambda AST to intermediate AST, eliminating lambdas bottom-up
  private def compile(expr: source.Expr): SKIComp = expr match
    case LambdaExpr.Var(name) => SKIComp.Var(name)
    case LambdaExpr.App(func, arg) => SKIComp.App(compile(func), compile(arg))
    case LambdaExpr.Abs(param, body) => abstractVar(param, compile(body))

  // 4. Extract pure SKI tree (fails safely if open terms are provided)
  private def extract(expr: SKIComp): target.Expr = expr match
    case SKIComp.Comb(e) => e
    case SKIComp.App(l, r) => app(extract(l), extract(r))
    case SKIComp.Var(name) => throw new IllegalArgumentException(s"Unbound free variable: $name")

  def apply(expr: source.Expr): target.Expr = extract(compile(expr))

Behavioral Localization

Why define these strictly typed homomorphisms? Raw syntactic translation is an incomplete account of computation. We seek to formally identify systems that exhibit identical computational behavior, even when their underlying geometric representations differ. Analogous to the localization of weak equivalences in abstract homotopy theory, we define a behavioral weak equivalence as a behavior-respecting morphism that induces a bijection on behavioral quotients. In the Gabriel-Zisman localization of this category, these behavioral weak equivalences are inverted, becoming true isomorphisms.

Within this localized setting, the standard equivalences among classical applicative and concatenative presentations are expressed as precise categorical weak equivalences. Specifically, bracket abstraction, lambda interpretation, and the iota encoding generate inverse behavior classes in the behavioral quotient. Consequently, presentations of the untyped \(\lambda\)-calculus, SKI, and the \(\iota\)-calculus become isomorphic in the behavioral localization of behaviorally diagonally closed applicative calculi.

Through this framework, type safety ceases to be an external compilation step; it becomes a physical requirement of the magmoid structure itself. By decoupling language, semantics, and interpretation, we establish a mathematically rigorous and type-safe environment suitable for exploring the foundational topology of computation.

Examples: Observing the Calculi in Action

To observe this algebraic structure in motion, we can evaluate terms across our three distinct calculi. The Scala implementation executes the formal reductions step-by-step until normal forms are reached, or translates them across homomorphic boundaries.

SKI Calculus Evaluation

In the SKI calculus, we can test the standard identity reduction. The term \(S(K)(K)(I)\) structurally routes the combinators to ultimately collapse into the pure identity combinator \(I\). Applying our normalizer perfectly tracks the reduction rules until the free magma tree resolves to the final state.

import SKICalculus.{S, K, I, apply}

val skiExpr = S(K)(K)(I)
val skiResult = SKICalculus.normalize(skiExpr, Some(100))

println(s"Result:     ${skiResult.get}")

Result:     Leaf(I)

Homomorphic Evaluation of \(\iota\)-Calculus

The pure \(\iota\)-calculus is evaluated homomorphically. Since pure \(\iota\) has no stable single-step reductions without diverging into infinite macro-expansions, we bypass the issue by utilizing our localized weak equivalences. We construct the identity term \(\iota(\iota)\), map it through the IotaToSKI homomorphism into the SKI evaluation engine, reduce it safely there, and seamlessly map the normal form back to \(\iota\). The massive resulting \(\iota\)-tree is the strictly closed mathematical result of the computation.

import IotaCalculus.i

val iotaExpr = i(i)
val mappedToSKI = IotaToSKI(iotaExpr)
val evaluatedSKI = SKICalculus.normalize(mappedToSKI, Some(100))
val resultIota = evaluatedSKI.map(SKIToIota.apply)

println(s"Result:     ${resultIota.get}")

Result:     App(App(App(Leaf(Iota),App(Leaf(Iota),App(Leaf(Iota),App(Leaf(Iota),Leaf(Iota))))),App(Leaf(Iota),App(Leaf(Iota),App(Leaf(Iota),Leaf(Iota))))),App(App(Leaf(Iota),App(Leaf(Iota),App(Leaf(Iota),Leaf(Iota)))),App(Leaf(Iota),App(Leaf(Iota),App(Leaf(Iota),Leaf(Iota))))))

Here is the rewritten section. I have added a narrative that frames these examples as a demonstration of the framework’s power: first verifying native reduction within the \(\lambda\)-calculus, and then proving that our LambdaToSKI homomorphism preserves computational behavior by lifting the term into the SKI magma.

Examples: Observing the Calculi in Action

To observe this algebraic structure in motion, we can evaluate terms across our distinct calculi. The Scala implementation executes the formal reductions step-by-step until normal forms are reached, or translates them across homomorphic boundaries to verify structural equivalence.

Church Booleans in \(\lambda\)-Calculus

To see how the structural translation handles variable binding, we employ Church Booleans. These encodings allow us to represent logical values as higher-order functions within the untyped \(\lambda\)-calculus. We define the logical NOT operator and apply it to TRUE. The engine applies \(\beta\)-reduction with capture-avoiding substitution to traverse the abstract syntax tree and reduce the expression to its canonical form, demonstrating the soundness of our \(\lambda\)-calculus normalization rules[cite: 5].

import LambdaCalculus.*

val True = lam("x", lam("y", v("x")))
val False = lam("x", lam("y", v("y")))
val Not = lam("p", v("p")(False)(True))
val lambdaExpr = Not(True)
val lambdaResult = LambdaCalculus.normalize(lambdaExpr, Some(100))

println(s"Result:     ${lambdaResult.get}")
println(s"Matches Church FALSE? ${lambdaResult.get == False}")

Result:     Abs(x,Abs(y,Var(y)))
Matches Church FALSE? true

Homomorphic Translation to SKI

The true strength of our categorical framework lies in its ability to translate across different computational universes. The LambdaToSKI homomorphism uses the bracket-abstraction algorithm to compile variable-dependent \(\lambda\)-terms into pure, variable-free combinatory logic trees.

By translating lambdaExpr into the SKI magma and normalizing it there, we verify that our translation is a behavioral weak equivalence. Because both the \(\lambda\)-calculus and SKI are combinatorially complete and behaviorally diagonally closed, the result of the converted reduction must be behaviorally equivalent to our initial native result.

val lambdaConverted = LambdaToSKI(lambdaExpr)
val resultConverted = SKICalculus.normalize(lambdaConverted)

println(s"Converted AST: ${lambdaConverted}")
println(s"Normalization successful: ${resultConverted.isDefined}")

Converted: App(App(App(Leaf(S),App(App(Leaf(S),Leaf(I)),App(Leaf(K),App(Leaf(K),Leaf(I)))),App(Leaf(K),App(App(Leaf(S),App(Leaf(K),Leaf(K))),Leaf(I)))),App(App(Leaf(S),App(Leaf(K),Leaf(K))),Leaf(I)))
Normalization successful: true

These examples confirm the theoretical core of the framework: different syntax, same computational behavior, mapped through the prism of structural homomorphisms.