Nix has no loops and no tail-call optimization. Every iteration is recursion, recursion costs stack frames, and the evaluator caps call depth at 10,000. For most Nix code that is plenty. But lib.splitString overflows on input past a few hundred lines, and a foldl' that updates an attrset field from the previous accumulator can build a thunk chain that overflows after tens of thousands of steps when forced. Any code whose work scales with its input, a validator, a DSL interpreter, a config transformer, eventually hits the same wall.
nix-effects embeds a Martin-Löf proof checker that runs entirely at nix eval time, no evaluator patches, no external tools. The point of the talk is not to get into the weeds on type theory, and I assume no knowledge of type theory either. Rather, the point is that a type checker is the kind of program where you cannot paper over the evaluator's limits without risking an unsound implementation. Normalization recurses as deep as the proof demands, and every shortcut the language usually leaves open needs to be closed. Building it forced me to solve, by necessity, the problems that ordinary Nix code merely brushes against.

The talk follows those solutions in the order the evaluator extracted them, as a field report on its observable semantics. What it forces, what it leaves suspended, where it spends stack, and where the cost reappears when that stack moves into userland data.

Round one, the stack: builtins.genericClosure was designed to compute package dependency closures; it doubles as a general-purpose trampoline, a million iterations in O(1) stack depth. Round two, the thunks: the naive trampoline hides a trap that made the community shelve the approach in 2022. Laziness silently rebuilds the very stack you eliminated, and the crash surfaces far from the loop that caused it. We break the chain by smuggling eager evaluation through the one field genericClosure is guaranteed to inspect, a technique I have not found documented anywhere else. Round three, the cost of forcing: blanket deepSeq turns out to be a quadratic sledgehammer; sometimes seq is enough, sometimes an integer key is. Round four, the closures, which no amount of forcing can see inside; the answer is defunctionalization, rebuilding the evaluation loop as a CEK-style machine whose continuations are plain data. Round five, stack safety becomes heap pressure. Defunctionalization removes the evaluator stack by turning continuations into ordinary Nix data; the next problem is allocation, retention, and sharing. Each fix relocates the cost. The talk shows where it moves at each stage, and what that means for real Nix programs.

You leave with a drop-in pattern for unbounded iteration in Nix, a working mental model of where thunk chains form in lazy code, a calibrated sense of when plain foldl' is all you need, and the production evidence the stalled builtins.trampoline proposal has been waiting for since 2023. Everything runs live in nix repl.