This post is dedicated to George Pollard and Ivan Towlson, for starting me on the scary path to category theory.
Series: Your Clean Architecture Has a Dirty Secret
This is Part 5 of a 6-part series on separating intent from process in real-world C#.
- Your Clean Architecture Has a Dirty Secret
- The Algebra of Intent
- Intent You Can See (and Optimize)
- Two Sides of the Same Coin
- Standing on the Shoulders of Giants ← you are here
- The Strangler Fig
Standing on the Shoulders of Giants
Over four posts, we diagnosed a coupling (intent fused with process), built two solutions (algebra-first and data-first), and discovered they’re dual. But two questions remain:
Why do they work? And can we trust them?
Fair warning. This post is the victory lap for the mathematically curious. Everything you need to build these systems was in Posts 2 and 3. Everything you need to choose between them was in Post 4. This post is about why it all works — monads, free constructions, the Yoneda lemma, algebraic effects. If category theory isn’t your thing, you can stop here with full confidence in the tools you’ve already built. But if you want to see the foundations — the reason your interpreters compose, your optimizers preserve meaning, and your tests are trustworthy — this is for you.
- Standing on the Shoulders of Giants
- The Monad Laws — Your Correctness Guarantee
- The Free Monad — Why “Free”?
- And the Trampoline from 2020? That was
Free<Thunk, T>.SuspendwasImpure.executewas the interpreter. - Tagless Final and Yoneda — Why “Final”?
- Algebraic Effects — The Synthesis
- The Callback to This Blog’s History
- Standing on the Shoulders of Giants
The Monad Laws — Your Correctness Guarantee
In Posts 2 and 3, we built Done/Pure and Then/Bind. In Post 3, we implemented SelectMany for LINQ syntax. These aren’t arbitrary implementations — they satisfy three laws, and those laws are what make everything else work.
Left Identity
\[\text{Done}(a).\text{SelectMany}(f) = f(a)\]In English: wrapping a value in Done and immediately binding it to a function is the same as calling the function directly. “If you already have the answer, just use it.”
For our order flow: lifting a value into the program and immediately continuing is the same as continuing directly. There’s no overhead, no extra layer.
Right Identity
\[m.\text{SelectMany}(\text{Done}) = m\]In English: binding a program to Done — “take the result and wrap it” — gives back the same program. “Wrapping and unwrapping are inverses.”
For our order flow: if the last step of your program is just select x (which compiles to .Select(x => x), which is .SelectMany(x => Done(x))), it doesn’t change the program.
Associativity
\[(m.\text{SelectMany}(f)).\text{SelectMany}(g) = m.\text{SelectMany}(x \Rightarrow f(x).\text{SelectMany}(g))\]In English: it doesn’t matter whether you group compositions left or right. “Parenthesization doesn’t matter.”
For our order flow: you can break a workflow into sub-workflows and compose them, and the result is identical to writing the whole thing flat. This is why you can write PlaceOrder using smaller building blocks like ValidateAndPrice and ChargeAndReserve and compose them freely without worrying about subtle ordering bugs.
Why These Laws Matter in Practice
These aren’t abstract niceties. They’re correctness guarantees:
-
Refactoring safety: Associativity means you can extract sub-workflows, inline them, regroup them — and the behavior is identical. No hidden ordering dependencies.
-
Optimizer correctness: When the batching optimizer from Post 3 rewrites the AST, associativity guarantees the rewritten program produces the same result as the original. Without this law, optimization would be unsafe.
-
Interpreter interchangeability: The identity laws guarantee that the production interpreter and test interpreter, given the same inputs, see structurally the same program. No “works in test, fails in prod” surprises caused by the plumbing itself.
-
Composition: Left identity says “lifting doesn’t add overhead.” Right identity says “the identity continuation is a no-op.” Together, they mean
DoneandSelectManyform a well-behaved unit — like 0 and + for addition, or 1 and × for multiplication. You can compose freely without worrying about edge cases in the plumbing.
This is the same framework from the Trampoline post where we proved the Trampoline satisfies these laws, and from This is not a Monad Tutorial where we derived monads from practical composition needs. The laws are always the same. The effects change; the guarantees don’t.
The Free Monad — Why “Free”?
In Post 3, we built OrderProgram<T> — a data structure with Done, Failed, and Then cases. We implemented SelectMany for it. We proved (by construction) that it satisfies the monad laws. Then we wrote LINQ programs against it.
This construction has a general form:
\[\text{Free}(F, A) = \text{Pure}(A) \mid \text{Impure}(F(\text{Free}(F, A)))\]Where $F$ is any functor — our effect type. In our case, $F$ = OrderStep. So:
Done<T>(value)isPure(A)— a finished computationThen<T, TNext>(step, continue)isImpure(F(Free(F, A)))— one layer of effect wrapping the rest of the computation
Why “Free”?
The word “free” has a precise mathematical meaning. In algebra, a free construction is the most general structure that satisfies a set of laws and nothing else. The free group over a set of generators is the group you get by doing nothing except what the group axioms force you to do — no additional relations, no simplifications.
The Free Monad over a functor $F$ is the most general monad you can build from $F$. It satisfies the monad laws (left identity, right identity, associativity) and nothing else. No extra laws. No built-in interpretation. Pure syntax.
This is why:
OrderProgram<T>captures every possible order workflow — it doesn’t bias toward any particular interpretation- The same AST can be interpreted by production, test, dry-run, narrative, and saga interpreters — because the AST commits to no interpretation
- Optimizers can freely rewrite the AST — because the only laws are the monad laws, which associativity preserves
Free Monads are well-studied. Their properties are proven — not “believed to work” or “seems correct in practice.” When you build one, you get a correct monad for free (hence the name). The math community has been stress-testing these structures since the 1970s.
Our OrderProgram<T> from Post 3 is literally Free<OrderStep, T>.
And the Trampoline from 2020? That was Free<Thunk, T>. Suspend was Impure. execute was the interpreter.
Tagless Final and Yoneda — Why “Final”?
In Post 2, we defined the order flow as a generic function over an algebra: PlaceOrder<TResult>(IOrderAlgebra<TResult> alg, ...). The program is the function. Different interpreters (implementations of IOrderAlgebra) give it different meanings.
Why does this work? Why is a program defined by “what all interpreters do with it” the same as a program defined by “the AST of its steps”?
The answer is the Yoneda lemma — arguably the most important result in category theory, dating to 1954.
The Yoneda Lemma (Intuition)
A thing is completely determined by how it interacts with all other things.
A natural number isn’t Zero | Succ n. A natural number is what you can do with it: add, multiply, compare, use as a loop counter. If two things support the same operations in the same way, they’re the same thing.
More precisely, for a category $\mathcal{C}$ and an object $A$, the Yoneda lemma says:
\[\text{Nat}(\text{Hom}(A, -), F) \cong F(A)\]The set of natural transformations from the hom-functor $\text{Hom}(A, -)$ to a functor $F$ is in bijection with $F(A)$. The “abstract” description (all possible morphisms out of $A$) determines the “concrete” value ($F(A)$) and vice versa.
What This Means for Us
Tagless Final is the Yoneda perspective on DSLs.
A Tagless Final program is a natural transformation: for every interpreter (every choice of TResult), it produces a TResult. The program is its set of possible interpretations. Not “the program has interpretations” — the program is defined as the function from interpreters to results.
The Yoneda lemma guarantees that this function-from-all-interpreters determines a unique abstract program. If two Tagless Final programs give the same result for every interpreter, they’re the same program. Conversely, every abstract program corresponds to exactly one such function.
This is why both encodings represent the same abstract program:
- Free Monad (Post 3): the program is a concrete data structure — an element of $F(A)$
- Tagless Final (Post 2): the program is a natural transformation — an element of $\text{Nat}(\text{Hom}(A, -), F)$
- Yoneda: these are the same thing
The theorem gives us confidence to write programs in Tagless Final style (Post 2) knowing they capture exactly the same information as the Free Monad AST (Post 3). When we convert between them (the ToFreeMonad interpreter from Post 4), no information is lost. Yoneda guarantees it.
Why “Final”?
In the duality from Post 4:
- Initial = the Free Monad = defined by constructors (how to build programs)
- Final = Tagless Final = defined by observations (how to interpret programs)
“Tagless” because there’s no runtime tagging — the types enforce correctness. “Final” because the program is defined by its final observations, not by its initial construction. The terminology comes directly from the algebra: initial objects are characterized by unique morphisms out; final objects are characterized by unique morphisms in.
Algebraic Effects — The Synthesis
We’ve seen two ways to separate intent from process:
- Tagless Final: effects declared as interface methods, handled by implementing the interface
- Free Monad: effects declared as data constructors, handled by pattern matching in an interpreter
There’s a third approach gaining traction in programming language research that synthesizes both.
Algebraic effects let you:
- Declare effects as operations (like Tagless Final — interface methods)
- Handle them with access to the continuation (like the Free Monad — you can inspect, resume, branch, or discard)
- Write programs in direct style — no LINQ, no computation expressions, just
perform CheckStock(items)in the middle of normal code
Here’s what our order flow would look like in a language with native algebraic effects (pseudocode):
effect Order {
CheckStock : List<Item> -> StockResult
CalculatePrice : List<Item> * Coupon? -> PriceResult
ChargePayment : PaymentMethod * decimal -> ChargeResult
ReserveInventory : List<Item> -> ReservationResult
SendConfirmation : Customer * PriceResult -> Unit
}
fun placeOrder(request: OrderRequest): OrderResult {
val stock = perform CheckStock(request.items)
if (!stock.isAvailable) return OrderResult.Failed("Out of stock")
val price = perform CalculatePrice(request.items, request.coupon)
val charge = perform ChargePayment(request.paymentMethod, price.total)
if (!charge.succeeded) return OrderResult.Failed("Payment failed")
perform ReserveInventory(request.items)
perform SendConfirmation(request.customer, price)
return OrderResult.Success(charge.transactionId)
}
Look at that. It’s almost the same as the original PlaceOrder from Post 1 — direct, readable, imperative-looking code. But the perform keyword turns each operation into an algebraic effect that can be intercepted by a handler:
handler ProductionHandler {
return(x) -> x
CheckStock(items, k) -> k(inventory.checkStockAsync(items))
ChargePayment(m, a, k) -> k(payment.chargeAsync(m, a))
// ... each effect maps to real I/O, k is the continuation
}
handler TestHandler {
return(x) -> x
CheckStock(items, k) -> k(StockResult(available: true))
ChargePayment(m, a, k) -> k(ChargeResult(succeeded: true, txnId: "test"))
// ... each effect maps to a deterministic value
}
// Swap handlers — same as swapping interpreters
val result = with ProductionHandler { placeOrder(request) }
val testResult = with TestHandler { placeOrder(request) }
The handler gets the continuation k — meaning it can:
- Resume normally:
k(result)— like a normal interpreter - Resume multiple times:
k(result1); k(result2)— exploring multiple paths - Not resume at all: return early, like
Failed - Inspect before resuming: the optimization passes from Post 3, naturally
- Stack handlers: compose effects from different domains
This is the best of both worlds:
- Syntax as clean as Tagless Final — no AST construction, no
Lift, direct-style code - Power of the Free Monad — the handler has the continuation, so it can inspect, transform, batch, compensate
- Composable — stack handlers for different effect types (logging + execution + timing)
Where Does This Exist?
Several languages have algebraic effects, either natively or experimentally:
- Koka — Microsoft Research, designed around algebraic effects
- OCaml 5 — added native effect handlers in 2023
- Eff — a research language built entirely around effects
- Unison — abilities (their term for effects) are first-class
And in .NET? Not yet. C# doesn’t have algebraic effects. But that’s the point of Posts 2 and 3 — you don’t need language support. We proved that you can encode both styles in standard C# using interfaces and records. Language support would make the separation frictionless, but the separation itself is achievable today.
If you want to think about where .NET could go: the async/await machinery in C# is already a limited, single-purpose algebraic effect handler. The await keyword performs an effect (Suspend), and the runtime handler decides whether to resume synchronously or schedule a continuation. Generalizing this to arbitrary effects — that’s the direction.
The Callback to This Blog’s History
This entire blog, it turns out, has been circling the same idea.
2018: A Tale of Two Languages — A prototype Free Monad for Q#. We built an AST of quantum operations and interpreted it. The seed of programs-as-data.
2020: Bouncing around with Recursion — The Trampoline. Bounce | Done | Call. We built a stack-safe recursion scheme by reifying continuations as data — without knowing we were building Free<Thunk, A>. The first instance.
2022: This is not a Monad Tutorial — Monads as “composing functions in context.” We derived Bind from practical needs: composing A → M<B> functions. The framework for understanding why composition works.
2025: Tagless Final series — DSLs, interpreters, verification in F#. The Frog DSL. Six posts building up the Final encoding, culminating in model verification. The final encoding explored in depth.
2026: The Trampoline is a Monad — The revelation that the 2020 Trampoline was a Free Monad all along. Suspend = Impure. execute = fold. The connection that tied Free Monads to our earlier work.
2026: This series — Applying both Tagless Final and Free Monads to real-world C# architecture. Diagnosing the intent-vs-process coupling. Building both solutions. Discovering the duality. The unification.
It was all the same idea.
Separate what from how. Express intent. Defer process. Interpret.
Different languages (F#, C#, Q#, Python). Different domains (games, recursion, errors, orders, quantum). Different techniques (computation expressions, LINQ, pattern matching). But always the same pattern: define what you want, then choose how to do it, and keep them separate.
Standing on the Shoulders of Giants
The patterns we built in C# — with LINQ queries and interfaces — aren’t clever tricks. They’re instances of mathematical structures studied for half a century.
| Structure | Dates to | Our use |
|---|---|---|
| Monads | Eilenberg & Mac Lane, 1945; Moggi, 1989 (for computation) | SelectMany / Bind composition in Posts 2 and 3 |
| Free constructions | Universal algebra, 1930s–1970s | OrderProgram<T> as Free<OrderStep, T> in Post 3 |
| F-algebras / F-coalgebras | Lambek, 1968 | Initial = Free Monad, Final = Tagless Final (Post 4) |
| Yoneda lemma | Yoneda, 1954 | “A program is determined by its interpretations” (Post 4) |
| Tagless Final | Carette, Kiselyov & Shan, 2007 | IOrderAlgebra<TResult> in Post 2 |
| Algebraic effects | Plotkin & Power, 2002; Plotkin & Pretnar, 2009 | The synthesis that combines both (this post) |
These aren’t ivory-tower abstractions disconnected from practice. They’re the reason:
- Our interpreters compose correctly — naturality (1940s) guarantees that swapping an interpreter doesn’t change the program’s meaning
- Our optimizers preserve meaning — the monad laws (1945) guarantee that rewriting an AST by associativity gives the same result
- Our tests are trustworthy — the Yoneda lemma (1954) guarantees that the Tagless Final program and the Free Monad AST carry the same information
- Our duality is real — Lambek’s lemma (1968) guarantees that initial algebras and final coalgebras are isomorphic
- Our LINQ programs are correct — the Free construction (1970s) guarantees that any functor gives rise to a monad that satisfies the laws automatically
We’re not inventing something new. We’re applying decades of proven, stress-tested mathematical theory to a practical engineering problem — separating what from how in real-world C# applications.
The next time someone asks “why should I trust that swapping this interpreter gives the same result?” — the answer isn’t “it worked in our tests.” The answer is “naturality guarantees it.” The next time someone asks “can this optimizer change the result?” — the answer isn’t “we haven’t found a bug yet.” The answer is “associativity proves it can’t.”
That’s what standing on the shoulders of giants gives you. Not just working code — code you can reason about. Code with mathematical guarantees. Code that’s correct not because you tested enough, but because the structure makes it so.
The dirty secret — intent fused with process — turned out to have a clean mathematical solution. Two solutions, in fact, that are duals of each other. And behind those solutions: half a century of mathematics, patiently waiting for working developers to find it useful.
I hope this series has made it useful.
Next: The Strangler Fig — the Monday morning migration plan. How to get your legacy codebase from fused intent-and-process to separated, one service at a time, without a rewrite.
Companion code: The complete working implementation for the entire series is available in three languages:
Language What it demonstrates Tests C# The primary language of the series — IOrderAlgebra<T>, LINQ-based Free Monad, execution plan analyzer, saga interpreter45 F# Computation expressions, structural analysis, monad laws 27 Haskell The native habitat — type classes are Tagless Final, GADTs are the Free Monad, do-notation is LINQ. No HKT workarounds, no boxing, no ceremony. 29 The blog’s code is simplified for teaching. The companion code compiles, runs, and passes all 101 tests across three languages.
This is Part 5 of the series “Your Clean Architecture Has a Dirty Secret.” The full series:
- Your Clean Architecture Has a Dirty Secret — the diagnosis
- The Algebra of Intent — Tagless Final
- Intent You Can See (and Optimize) — Free Monads
- Two Sides of the Same Coin — the duality
- Standing on the Shoulders of Giants — the foundations
- The Strangler Fig — the migration
For the F# perspective on Tagless Final, see the six-part Tagless Final series. For the Free Monad story that started it all, see Bouncing around with Recursion and The Trampoline is a Monad.