In earlier posts, I described applicative calculi as parsed magmas, the coalgebraic decomposition of terms, and the typed recursion schemes behind normalization. I also explained how adjoining operators and root rules produces a noncommutative ordered product. This post develops the corresponding Scala scaffold.
The guiding idea is close to Guy Steele’s Growing a Language: begin with a small core, then grow it by adjoining self-contained linguistic components. Here those components are applicative calculi, and their composition is explicit in both the mathematics and the code.
An applicative calculus has a set of terms with a total binary application operation. For the formal languages considered here, the carrier is the free magma on an alphabet of operators and indeterminates.
enum Magma[+A]:
case Gen(a: A)
case App(left: Magma[A], right: Magma[A])Thus Magma[A] implements the free magma \(\mathrm{Free}(A)\). A term is either a
generator or a binary application tree.
The covariance annotation +A is important. If an
alphabet \(A\) is enlarged to the union
type A | B, then a term of type Magma[A] is
already usable as a term of type Magma[A | B]. No explicit
injection or cast is needed.
A calculus supplies a partial root rewriting map. The parsing coalgebra of the free magma then extends it to a deterministic contextual one-step operation: try the root first, then the left branch, then the right branch.
import scala.annotation.tailrec
object Reduction:
def contextStep[A](
m: Magma[A]
)(
rootRule: Magma[A] => Option[Magma[A]]
): Option[Magma[A]] =
rootRule(m).orElse {
m match
case Magma.App(l, r) =>
contextStep(l)(rootRule)
.map(Magma.App(_, r))
.orElse(contextStep(r)(rootRule).map(Magma.App(l, _)))
case _ => None
}
def normalize[A](
step: Magma[A] => Option[Magma[A]],
term: Magma[A],
fuel: Int = 5000
): Option[Magma[A]] =
@tailrec
def loop(current: Magma[A], remaining: Int): Option[Magma[A]] =
step(current) match
case None => Some(current)
case Some(_) if remaining <= 0 => None
case Some(next) => loop(next, remaining - 1)
loop(term, fuel)contextStep is not the full nondeterministic compatible
closure of rewriting. It implements one fixed strategy: root-first and
then left-to-right.
normalize iterates that strategy until no step is
available. The fuel bound makes the evaluator total as a Scala function;
returning None means only that the budget was exhausted,
not that the term has no normal form.
A formal calculus provides its root map uniformly over every larger alphabet containing its own operators.
trait Calculus[C]:
def head[T >: C](m: Magma[T]): Option[Magma[T]]
final def step[T >: C](m: Magma[T]): Option[Magma[T]] =
Reduction.contextStep(m)(t => head[T](t))
final def normalize[T >: C](
m: Magma[T],
fuel: Int = 5000
): Option[Magma[T]] =
Reduction.normalize(t => step[T](t), m, fuel)The bound T >: C is the key. A calculus whose own
alphabet is C can apply its rules inside any larger
language whose alphabet contains C.
The ordered product is implemented by by:
extension [A](base: Calculus[A])
infix def by[B](ext: Calculus[B]): Calculus[A | B] =
new Calculus[A | B]:
def head[T >: A | B](m: Magma[T]): Option[Magma[T]] =
ext.head[T](m).orElse(base.head[T](m))The carrier alphabet becomes A | B. At the root, the
right-hand factor is tried first; the left-hand factor is used only if
the right-hand one is undefined. This is the noncommutative ordered
product \(\mathcal C\odot\mathcal
D\).
An inert calculus has no root rules:
def constants[A]: Calculus[A] = new Calculus[A]:
def head[T >: A](m: Magma[T]): Option[Magma[T]] = Noneconstants[A] adjoins inert generators of type
A. The actual monoidal unit is the empty-alphabet instance,
constants[Nothing].
A calculus is operator-headed when every root redex begins with one of its own operators. Adjoining such a calculus does not introduce new one-step reductions on old terms, so the extension is strictly conservative on the original language.
Here are the S, K, and I
calculi.
enum SK:
case S, K
object SkCalc extends Calculus[SK]:
def head[T >: SK](m: Magma[T]): Option[Magma[T]] = m match
case Magma.App(Magma.App(Magma.Gen(SK.K), x), _) =>
Some(x) // K x y → x
case Magma.App(
Magma.App(Magma.App(Magma.Gen(SK.S), x), y),
z
) =>
Some(Magma.App(Magma.App(x, z), Magma.App(y, z)))
// S x y z → x z (y z)
case _ => None
enum IComb:
case I
object ICalc extends Calculus[IComb]:
def head[T >: IComb](m: Magma[T]): Option[Magma[T]] = m match
case Magma.App(Magma.Gen(IComb.I), x) => Some(x) // I x → x
case _ => NoneIf variables are represented by
case class Var(name: String)then the SKI calculus is assembled as follows:
val skiCalc = constants[Var] by SkCalc by ICalcAdding ICalc does not change any reduction of an old SK
term: an I-rule cannot apply to a term containing no
I.
The same interface accommodates other combinatory systems. Explicit duplication is a one-rule calculus.
enum Dup:
case D
object DupCalc extends Calculus[Dup]:
def head[T >: Dup](m: Magma[T]): Option[Magma[T]] = m match
case Magma.App(Magma.Gen(Dup.D), x) =>
Some(Magma.App(x, x)) // D x → x x
case _ => NonePriority matters when root rules overlap. In the quotation–evaluation calculus, the specific rule must precede the general one.
enum Quote:
case Q, E
object QuoteCalc extends Calculus[Quote]:
def head[T >: Quote](m: Magma[T]): Option[Magma[T]] = m match
case Magma.App(
Magma.Gen(Quote.E),
Magma.App(Magma.Gen(Quote.Q), x)
) =>
Some(x) // E (Q x) → x
case Magma.App(Magma.Gen(Quote.E), x) =>
Some(x) // E x → x, used only when the previous clause fails
case _ => NoneThe second pattern is syntactically general, but pattern matching reaches it only after the quotation-specific clause has failed. Reversing the clauses changes the root map and therefore changes the equational theory generated by rewriting.
The de Bruijn lambda calculus requires computed right-hand sides rather than a fixed rearrangement of matched subterms.
enum Lambda:
case Lam
case Idx(n: Int)
object LamCalc extends Calculus[Lambda]:
import Magma.{Gen, App}
import Lambda.{Lam, Idx}
private def shift[T >: Lambda](
d: Int,
cutoff: Int,
t: Magma[T]
): Magma[T] = t match
case Gen(Idx(k)) =>
if k >= cutoff then Gen(Idx(k + d)) else t
case App(Gen(Lam), body) =>
App(Gen(Lam), shift(d, cutoff + 1, body))
case App(l, r) =>
App(shift(d, cutoff, l), shift(d, cutoff, r))
case _ => t
private def subst[T >: Lambda](
j: Int,
s: Magma[T],
t: Magma[T]
): Magma[T] = t match
case Gen(Idx(k)) =>
if k == j then s else t
case App(Gen(Lam), body) =>
App(Gen(Lam), subst(j + 1, shift(1, 0, s), body))
case App(l, r) =>
App(subst(j, s, l), subst(j, s, r))
case _ => t
def head[T >: Lambda](m: Magma[T]): Option[Magma[T]] = m match
case App(App(Gen(Lam), body), arg) =>
Some(shift(-1, 0, subst(0, shift(1, 0, arg), body)))
// (λ body) arg → body[0 := arg]
case _ => NoneLamCalc is operator-headed, so adjoining it is strictly
conservative on old combinatory terms. The intended binding semantics
still requires the usual well-scoping discipline: the free magma
contains all formal trees, including malformed or open de Bruijn
expressions.
A structural translation between free magmas is determined by its action on generators and extended recursively through application.
def translate[A, B](
m: Magma[A]
)(
rules: PartialFunction[A, Magma[B]]
): Option[Magma[B]] =
m match
case Magma.Gen(a) =>
rules.lift(a)
case Magma.App(l, r) =>
for
tl <- translate(l)(rules)
tr <- translate(r)(rules)
yield Magma.App(tl, tr)The use of PartialFunction and Option makes
omissions explicit. When rules covers every source
generator, translate is the unique total magma homomorphism
extending that generator map.
For example, suppose lamS, lamK, and
lamI are the usual de Bruijn lambda encodings. Then:
val skiToLam: PartialFunction[SK | IComb | Var, Magma[Lambda | Var]] =
case SK.S => lamS
case SK.K => lamK
case IComb.I => lamI
case v: Var => Magma.Gen(v)Because the recursive extension preserves application exactly, this
is a structural translation. It preserves the parsing coalgebra only
laxly: a source generator such as S is sent to a composite
lambda term, so the target exposes decompositions that did not exist in
the source.
Operational preservation is weaker than one-step preservation. A source root reduction may require several target beta steps. The natural requirement is eventual simulation: the translated redex must reduce in finitely many target steps to the translation of its source reduct.
The reverse passage, from lambda terms to SKI by bracket abstraction,
is not a magma homomorphism on the full free magma. The translation must
recognize the compound form Lam body and process the body
as a binder scope.
type Comb = SK | IComb | Lambda | Var
def lamToSki(t: Magma[Comb]): Magma[Comb] = t match
case Magma.App(Magma.Gen(Lambda.Lam), body) =>
bracket(lamToSki(body))
case Magma.App(l, r) =>
Magma.App(lamToSki(l), lamToSki(r))
case other => other
private def bracket(t: Magma[Comb]): Magma[Comb] = t match
case Magma.Gen(Lambda.Idx(0)) =>
Magma.Gen(IComb.I)
case Magma.Gen(Lambda.Idx(n)) =>
Magma.App(
Magma.Gen(SK.K),
Magma.Gen(Lambda.Idx(n - 1))
)
case Magma.App(l, r) =>
Magma.App(
Magma.App(Magma.Gen(SK.S), bracket(l)),
bracket(r)
)
case atom =>
Magma.App(Magma.Gen(SK.K), atom)For well-scoped closed lambda terms, bracket abstraction eliminates all de Bruijn indices and produces an SKI term. Its soundness is proved by the usual bracket-abstraction lemma, not by the universal property of a generator map.
The point of the scaffold is that extensions remain small and local. Begin with SKI:
val skiCalc = constants[Var] by SkCalc by ICalcAdd explicit duplication:
val skiDupCalc = skiCalc by DupCalcThen add quotation and evaluation:
val extendedCalc = skiDupCalc by QuoteCalcEach factor contributes an alphabet and a root map. Their ordered product places them in one free magmatic language, while the contextual strategy allows their reductions to interleave inside mixed terms.
The product is deliberately noncommutative: in C by D,
the rules of D have root priority over those of
C. For operator-headed factors with disjoint alphabets,
this priority does not alter reductions of old terms, but it remains
part of the combined calculus and matters whenever root domains
overlap.
This gives a precise version of language growth: extend the syntax by a free product of alphabets, extend the root semantics by priority composition, and derive the combined evaluator by contextual closure. The language grows without replacing its core.