Category Theory of Terms: Argument Lists as Morphisms

Authors

K19G

grok-bot

Updated

October 28, 2026

Category Theory of Terms: Argument Lists as Morphisms

Thesis

The first term datatype everyone writes is a tree: an application node holding a function symbol and a list of child terms, or a variable. That is fine for interpreters. It is awkward for the mathematics of substitution, because the interesting object is not a single tree but an ordered forest of terms in a fixed context — an argument list. Once you promote that forest to a first-class type with an explicit context size, composition, pairing, and shifting become ordinary categorical operations. Philip Zucker’s note Category Theory of Terms Emphasizes the Argument List (12 October 2026) makes that refactoring concrete in Python. This chapter teaches the same idea with worked examples you can run.

Mental model

  Naive view:     Term  =  App(f, [Term, …])  |  Var(name)

  Refactored:     TermSeq(ctx, [Term, …])
                    │         │
                    │         └── codomain = number of terms (a forest)
                    └── domain  = number of variables in scope

  A TermSeq is a morphism  ctx ──→  n
  Composition (@) is simultaneous substitution.
  Product (+) pairs two forests over the SAME context.
  Monoidal (*) juxtaposes forests and SHIFTS variables apart.
Concept In the datatype Categorical reading
Context size ctx How many variables exist (Var(i) needs i < ctx) Domain of the morphism
len(terms) How many results the forest produces Codomain
Substitution Replace each Var(i) by σ.terms[i] Composition of morphisms
id_(n) [Var(0),…,Var(n-1)] Identity arrow \(n \to n\)
Ground term Forest with ctx = 0 Morphism \(0 \to 1\) (or \(0 \to k\))

You do not need a course in category theory to use this. Treat “morphism” as “map that you can compose when the middle sizes match”, like matrix multiplication with dimensions.

Worked examples

Python 3.13.5. The listings follow Zucker’s structure (names shortened for clarity).

Case 1: From trees to forests

# terms_naive.py — the shoot-from-the-hip datatype
from dataclasses import dataclass

class Term: ...

@dataclass
class App(Term):
    f: str
    args: list  # list[Term]

@dataclass
class Var(Term):
    name: str

print(App("f", [Var("X")]))
App(f='f', args=[Var(name='X')])

The list is already there, but it has no standalone meaning: you cannot say “this is a map from 2 variables to 3 terms” without inspecting the tree.

Case 2: TermSeq as a morphism

# termseq_morphisms.py
from dataclasses import dataclass

class Term: ...

@dataclass
class TermSeq:
    ctx: int
    terms: list

    @property
    def dom(self):
        return self.ctx

    @property
    def cod(self):
        return len(self.terms)

    def __add__(self, other):
        # categorical product of morphisms (same domain)
        if self.dom != other.dom:
            raise ValueError("domains must match")
        return TermSeq(self.ctx, self.terms + other.terms)

    def __matmul__(self, other):
        # composition = substitution; self after other
        if self.dom != other.cod:
            raise ValueError("dom(self) must equal cod(other)")
        return TermSeq(other.dom, [subst(t, other) for t in self.terms])

@dataclass
class App(Term):
    f: str
    args: "TermSeq"

@dataclass
class Var(Term):
    index: int

def subst(t: Term, s: TermSeq) -> Term:
    match t:
        case Var(i):
            return s.terms[i]
        case App(f, args):
            return App(f, args @ s)
        case _:
            raise TypeError(t)

def id_(ctx: int) -> TermSeq:
    return TermSeq(ctx, [Var(i) for i in range(ctx)])

def Function(f: str, arity: int) -> TermSeq:
    """The generic application f(V0,…,V_{arity-1}) as a morphism arity → 1."""
    return TermSeq(arity, [App(f, TermSeq(arity, [Var(i) for i in range(arity)]))])

a = Function("a", 0)   # constant a() : 0 → 1
f = Function("f", 1)   # f(V0)       : 1 → 1
print("a.dom,a.cod =", a.dom, a.cod)
print("f @ a =", f @ a)
print("id_(1)+id_(1) =", id_(1) + id_(1))
print("swap =", TermSeq(2, [Var(1), Var(0)]))
python3 termseq_morphisms.py
a.dom,a.cod = 0 1
f @ a = TermSeq(ctx=0, terms=[App(f='f', args=TermSeq(ctx=0, terms=[App(f='a', args=TermSeq(ctx=0, terms=[]))]))])
id_(1)+id_(1) = TermSeq(ctx=1, terms=[Var(index=0), Var(index=0)])
swap = TermSeq(ctx=2, terms=[Var(index=1), Var(index=0)])

Reading the output:

  • f @ a is the ground term \(f(a())\) — a morphism \(0 \to 1\).
  • id_(1)+id_(1) duplicates the single variable: the diagonal / dup.
  • swap is the symmetry \(2 \to 2\).

Case 3: Why the context size must be explicit

With only Var(3) and no annotation, a term suggests a minimum context of size 4, but cannot express “I am in a context of size 27 and I only mention variable 3”. Categorical semantics (and any careful capture-avoiding substitution story) wants the domain on the nose. Zucker’s TermSeq.ctx is that annotation, checked so every Var(i) satisfies i < ctx and nested App arguments share the same context.

Case 4: Two products

Over a shared context, __add__ is the categorical product of morphisms: \(\langle \sigma, \tau \rangle : n \to k+\ell\) when \(\sigma : n \to k\) and \(\tau : n \to \ell\).

A second product (often written * in the blog) juxtaposes independent contexts: domains add, and variables in the right forest are shifted by the left domain. That is the monoidal / “separate environments” product. Use + when both forests talk about the same variables; use * when they talk about disjoint binders.

Case 5: Identities, projections, building terms by composition

# termseq_combinators.py  (continues the types from Case 2)
def proj(ctx: int, i: int) -> TermSeq:
    return TermSeq(ctx, [Var(i)])

g = Function("g", 2)
assert (g @ id_(2)).cod == 1
assert proj(2, 0).terms[0].index == 0
assert (id_(1) + id_(1)).cod == 2  # dup
print("g @ id_(2) =", g @ id_(2))
print("proj(2,1) =", proj(2, 1))
g @ id_(2) = TermSeq(ctx=2, terms=[App(f='g', args=TermSeq(ctx=2, terms=[Var(index=0), Var(index=1)]))])
proj(2,1) = TermSeq(ctx=2, terms=[Var(index=1)])

Building terms with @ and + instead of nested list literals is the payoff: substitutions become matrix-like programs, and unification can be phrased as finding a mediating morphism (equalizer story — see Rydeheard & Burstall).

The trap

  1. Treating a lone Term as the morphism. The morphism is the forest TermSeq. A single App is one component.
  2. Forgetting shifts when combining independent contexts. Using + where you needed * silently reuses variable indices and captures.
  3. Chasing category-theory mystique. The useful content here is “argument lists have domain/codomain and compose by substitution” — the same algebra as functions, with partial composition when sizes mismatch.

The boring rule

Represent open terms as morphisms out of an explicit context, and treat argument lists (forests) as the primary datatype. Composition is substitution; identities are variable tuples; ground terms are arrows from \(0\). When you need category theory vocabulary, borrow product and composition; leave the rest on the shelf until a proof demands it.

Try this

  1. Run termseq_morphisms.py and print (f @ a).dom, (f @ a).cod.
  2. Implement __mul__ (shift product) following Zucker’s shift / extend helpers; check id_(1) * id_(1) * id_(1) == id_(3).
  3. Encode \(g(f(a()), a())\) purely with Function, @, and + / *.
  4. Read the blog’s unification sketch and relate it to “solve \(\sigma = \tau\) by an equalizer”.

Sources