Internals
Implementation notes for the evaluator, type-checking kernel, trampoline, architecture, and formal kernel contract.
Internals explains how nix-effects is put together. These pages cover the trampoline, the relationship between the effect layer and the type-checking kernel, the trusted computing boundary, and the formal contract maintained by the kernel.
Trampoline
builtins.genericClosure trampolines the freer-monad interpreter to O(1) stack depth in Nix, which lacks both iteration primitives and tail-call elimination.
Systems Architecture
nix-effects pairs an effects kernel (freer monad on FTCQueue) with a type-checking kernel (MLTT on HOAS) so every fx.types value is checked by both.
Kernel Architecture
The type-checking kernel layers a TCB (eval/quote/conv) under the bidirectional check/infer pair; errors are sent as typeError effects, not thrown.
Kernel Formal Specification
Formal contract for the type-checking kernel: trust layers, typing rules, compute and conversion rules, and invariants the implementation must maintain.