In the previous posts, we modeled untyped applicative calculi using magmas and coalgebras. The raw syntax was a free magma, reduction was a retraction, and execution was a coalgebraic observation of states. It was a clean picture, but the untyped universe is entirely flat: any term can be applied to any other term.
What happens when we introduce types? The flat magma shatters into a category-like structure. But because raw application is not associative, we do not get a strict category. Instead, we get a Magmoid—a multi-sorted algebraic structure where objects are types, and morphisms are raw syntactic terms.
By shifting our perspective to this typed magmoid, the artificial boundary between “values” and “functions” disappears. Furthermore, we will see that we do not need to hack fixed-point combinators into the type system to achieve recursion. If the magmoid possesses a specific topological property—diagonal closure—recursion emerges naturally from the geometry of the paths.
Let our objects be types, constructed inductively from base types and the curried arrow (\(\to\)).
Instead of a single set of terms, we define \(L(A, B)\) as the set of raw syntactic expressions that transition a state from type \(A\) to type \(B\). A traditional “closed value” of type \(A\) is simply a morphism from the terminal object, living in \(L(1, A)\).
Application is no longer an arbitrary binary operation; it is categorical composition. If you have an expression \(a \in L(A, B)\) and an expression \(b \in L(B, C)\), you can juxtapose them to form a path \(ab \in L(A, C)\).
This composition is strictly non-associative. At the syntactic level, the path \(a(bc)\) is structurally distinct from \((ab)c\). The language \(L\) is therefore a Free Magmoid, representing the universe of un-evaluated abstract syntax trees.
To execute the program, we introduce the reduced state space \(R\), which forms a partial magmoid. The reduction map is a family of functions:
\[\beta_{A,B} : L(A, B) \longrightarrow R(A, B)\]
In this framework, computation is literally path collapse. If you have a reduced state \(a \in R(A, B)\) and feed it into a reduced state \(b \in R(B, C)\), the raw syntax \(ab\) sits in \(L(A, C)\). The reduction map \(\beta\) grinds this sequence down into a single, direct state transition:
\[A \xrightarrow{\ a\ } B \xrightarrow{\ b\ } C \quad \implies \quad \beta(ab) \in R(A, C)\]
Type safety is no longer a separate compilation step; it is a physical requirement of the magmoid. You cannot apply \(a \in R(A, B)\) to \(c \in R(D, E)\) because the topological edges do not align.
This strict geometry immediately raises a problem: how do we implement recursion? In the untyped \(\lambda\)-calculus, we rely on self-application (\(xx\)). But in our magmoid, an arrow \(x \in R(B, C)\) cannot compose with itself unless \(B = C\).
Instead of artificially injecting a typed Y-combinator, we ask if the calculus itself can internalize duplication across valid type boundaries.
We define our typed calculus to be diagonally closed if, for every \(a \in R(A, B)\), there exists a duplicator \(d_a \in R(A, B)\) such that for every endomorphism \(x \in R(B, B)\), the following holds:
\[\beta(a(xx)) = \beta(d_a x)\]
Let us verify the geometry. On the left, \(x\) is applied to \(x\) (forming a path in \(R(B, B)\)), and the result is prefixed by \(a \in R(A, B)\). The entire path maps \(A \to B \to B\), resolving to \(R(A, B)\). On the right, \(d_a \in R(A, B)\) is composed with \(x \in R(B, B)\), mapping \(A \to B \to B\), which also resolves to \(R(A, B)\). The type boundaries are perfectly respected.
Because the calculus is diagonally closed over endomorphisms, we can conjure recursion mathematically without leaving the rules of the magmoid.
Assume \(A = B\). We are looking for a loop for some starting path \(a \in R(B, B)\). By our closure definition, there exists a \(d_a \in R(B, B)\) such that for any \(x \in R(B, B)\), the equivalence \(\beta(a(xx)) = \beta(d_a x)\) holds.
Since \(x\) can be any endomorphism in \(R(B, B)\), and \(d_a\) is itself in \(R(B, B)\), we can substitute \(x = d_a\):
\[\beta(a(d_a d_a)) = \beta(d_a d_a)\]
Let \(p = \beta(d_a d_a)\). Because \(d_a \in R(B, B)\), the composition \(p\) also lives cleanly in \(R(B, B)\). Substituting \(p\) back into our equation yields:
\[\beta(ap) = p\]
We have materialized a fixed point \(p\) strictly from the topology of the paths. No external combinators or recursive types were required.
With diagonal closure providing Turing completeness, the composition map \(\beta\) can theoretically trace an infinite path (\(p = ap = aap = \dots\)). To handle non-termination without breaking the mathematics, we upgrade our types to pointed sets.
Every hom-set \(R(A, B)\) now contains a bottom element \(\bot_{A \to B}\), representing divergence. This allows \(\beta\) to remain a total function: if an un-evaluated syntactic path represents an infinite loop, \(\beta\) simply maps it directly to \(\bot\).
Crucially, the product of these pointed sets must be the Cartesian product, not the smash product. If we used the smash product, a diverging sub-path would behave like a black hole, collapsing the entire state machine: \((x, \bot) = \bot\). This would force a strictly strict (call-by-value) semantics.
By retaining the Cartesian product, the state \((x, \bot)\) remains mathematically distinct. A diverging path is isolated to its own coordinate. This enables lazy evaluation. For example, the constant combinator \(K\) can safely transition the state machine without evaluating the divergent branch:
\[\beta(K \circ a \circ \bot) = a\]
By combining typed magmoids, structural diagonal closure, and Cartesian pointed sets, we arrive at a remarkably disciplined foundation. Computation is categorical path collapse, recursion is an intrinsic topological property, and laziness is guaranteed by the geometry of divergence.