Dependent Types in Pure Nix

There is a tradition of small dependent type checkers: Mini-TT in ~400 lines of Haskell (Coquand et al. 2009), Kovács' elaboration-zoo growing through progressive tutorials from ~200 to ~1000 lines, Weirich's pi-forall at ~2000. These systems implement real Martin-Löf Type Theory (dependent functions, dependent pairs, identity types, universes) with normalization by evaluation and bidirectional type checking. They're educational but also genuine: the proof theory is sound, the algorithms are the same ones running inside Agda and Idris.

nix-effects adds an entry to this lineage in an unexpected host language. It embeds a full MLTT proof checker in pure Nix (~3000 lines, no evaluator patches, no external tools) with HOAS elaboration, cumulative universes, algebraic effects via freer monads, and verified extraction of plain Nix functions from proof terms. The whole system runs at nix eval time.

Two facts make this more than a curiosity. Pedrot & Tabareau's (2020) Fire Triangle theorem says dependent types are sound in any language without observable effects, and Nix evaluation is pure. Meanwhile, builtins.genericClosure can be repurposed as a general-purpose trampoline, giving us the deep recursion that type checking demands in a language with no tail-call optimization. The theory says it's safe; the trampoline makes it feasible.

This post walks through what you can prove, how the kernel works, and where the approach falls short. The code blocks are from the repository; you can run every example yourself.

Follow Along

git clone https://github.com/kleisli-io/nix-effects
cd nix-effects

# Run all tests, including every proof in this post
nix flake check

The four example files we'll be working through:

• examples/proof-basics.nix: computational equality, dependent witnesses, eliminators
• examples/equality-proofs.nix: J eliminator, congruence, symmetry, transitivity, transport
• examples/verified-functions.nix: type-checked functions extracted as plain Nix values
• examples/typed-derivation.nix: kernel-verified build configuration with records and strings

Each file takes { fx, ... } and uses fx.types.hoas for the HOAS surface language. To add your own, use the same pattern:

# my-proof.nix
{ fx, ... }:
let
  H = fx.types.hoas;
  inherit (H) nat eq checkHoas natLit refl succ zero;
in {
  # your proofs here
  myProof = (checkHoas (eq nat (succ zero) (natLit 1)) refl).tag == "refl";
}

nix eval --expr 'let fx = (builtins.getFlake (toString ./.)).lib;
                 in import ./my-proof.nix { inherit fx; }'

What You Can Prove

The HOAS surface uses Nix functions to represent binders. lam "x" nat (x: ...) creates a lambda where the Nix variable x stands for the object-language variable. The elaborator converts HOAS to de Bruijn indexed terms, the kernel checks them, and checkHoas runs the full pipeline: elaborate, type-check, return the normal form.

Computational Equality

The simplest class of proofs: both sides of an equation normalize to the same value, so Refl (reflexivity of identity) witnesses the equality. The kernel evaluates both sides via NbE, quotes them to normal forms, and checks structural identity.

# 3 + 5 = 8
checkHoas (eq nat (add (natLit 3) (natLit 5)) (natLit 8)) refl

add is defined by primitive recursion on naturals using the NatElim eliminator, the same elimination principle that Agda's pattern matching compiles to:

# add(m, n) = NatElim(λ_.Nat, n, λk.λih.S(ih), m)
# Base case: add(0, n) = n
# Step case: add(S(k), n) = S(add(k, n))
add = m: n:
  ind (lam "_" nat (_: nat)) n
    (lam "k" nat (_: lam "ih" nat (ih: succ ih))) m;

The motive λ_.Nat says the result type is Nat regardless of the scrutinee. The base case returns n. The step case takes the predecessor k, the inductive hypothesis ih = add(k, n), and returns S(ih). When the kernel evaluates add(3, 5), it unfolds three S constructors, hits the base case, and produces 8. Same 8 on the right side of the equation. Refl checks.

This scales to multiplication, list operations, anything computable:

# mul(3,4) = 12, multiplication via NatElim + add
mul = m: n: ind (lam "_" nat (_: nat)) zero
  (lam "k" nat (_: lam "ih" nat (ih: add n ih))) m;

checkHoas (eq nat (mul (natLit 3) (natLit 4)) (natLit 12)) refl
# → accepted

# length([1,2,3]) = 3, structural recursion via ListElim
length = xs:
  listElim nat (lam "_" (listOf nat) (_: nat)) zero
    (lam "h" nat (_: lam "t" (listOf nat) (_:
      lam "ih" nat (ih: succ ih)))) xs;

checkHoas (eq nat (length list123) (natLit 3)) refl
# → accepted

# append([1,2], [3]) = [1,2,3], ListElim rebuilds the spine
checkHoas (eq (listOf nat) (append list12 list3) list123) refl
# → accepted

All of these are computational equalities: the kernel normalizes both sides, they agree, Refl proves it. The proof-basics.nix file has seven such proofs, including sum([1,2,3]) = 6 via a fold and not(not(true)) = true via BoolElim.

Dependent Witnesses

Σ types (dependent pairs) pack a value with evidence of a property. In logic, Σ(x:A).P(x) reads "there exists an x of type A such that P(x) holds." The pair carries both the witness and the proof. You can't claim existence without exhibiting the thing.

# (8, Refl) : Σ(x:Nat). 3+5 = x
# "There exists a natural number x such that 3+5 = x. It's 8."
ty = sigma "x" nat (x: eq nat (add (natLit 3) (natLit 5)) x);
tm = pair (natLit 8) refl ty;
checkHoas ty tm  # → accepted

The kernel checks the first component (8 : Nat), substitutes it into the dependent type to get Eq(Nat, add(3,5), 8), normalizes both sides, and accepts Refl. The dependency is real: the type of the second component depends on the value of the first. Change 8 to 7 and the proof fails; add(3,5) normalizes to 8, not 7, so Refl is rejected.

A more interesting dependent witness, double negation on a concrete boolean:

# (true, Refl) : Σ(b:Bool). not(not(b)) = b
ty = sigma "b" bool (b: eq bool (not_ (not_ b)) b);
tm = pair true_ refl ty;
checkHoas ty tm  # → accepted

The kernel evaluates not(not(true)) to true, confirms it equals true, done. This is a ground-instance proof of involution for a specific boolean. A universal statement would require induction over Bool (which BoolElim handles).

Eliminators

Every inductive type in MLTT has an eliminator: a recursion principle that is the only way to consume values of that type. Without eliminators, you could pattern-match into arbitrary computations; with them, all cases are handled and recursive calls decrease structurally.

nix-effects implements the standard Martin-Löf eliminators:

NatElim, primitive recursion on natural numbers:

# double(n) = NatElim(λ_.Nat, 0, λk.λih.S(S(ih)), n)
double = n: ind (lam "_" nat (_: nat)) zero
  (lam "k" nat (_: lam "ih" nat (ih: succ (succ ih)))) n;

checkHoas (eq nat (double (natLit 4)) (natLit 8)) refl  # → accepted

BoolElim, case analysis on booleans (the dependent if):

# if true then 42 else 0 = 42
result = boolElim (lam "_" bool (_: nat)) (natLit 42) zero true_;
checkHoas (eq nat result (natLit 42)) refl  # → accepted

ListElim, structural recursion on lists:

# map succ [0,1,2] = [1,2,3]
mapSucc = xs: listElim nat (lam "_" (listOf nat) (_: listOf nat))
  (nil nat)
  (lam "h" nat (h: lam "t" (listOf nat) (_:
    lam "ih" (listOf nat) (ih: cons nat (succ h) ih)))) xs;

checkHoas (eq (listOf nat) (mapSucc list012) list123) refl  # → accepted

SumElim, case analysis on coproducts (A + B):

# case Right(true) of { Left n → n; Right b → if b then 1 else 0 } = 1
scrut = inr nat bool true_;
result = sumElim nat bool (lam "_" (sum nat bool) (_: nat))
  (lam "n" nat (n: n))
  (lam "b" bool (b: boolElim (lam "_" bool (_: nat)) (natLit 1) zero b))
  scrut;

checkHoas (eq nat result (natLit 1)) refl  # → accepted

Each eliminator takes a motive, a function from the scrutinee to a type. The motive is what makes elimination dependent. The motive λ_.Nat above is constant (the result is always Nat), but dependent motives are supported: the result type of a NatElim can depend on the natural number being eliminated. In Agda, pattern matching compiles to exactly these eliminators. Here you write them by hand, which is verbose but leaves nothing hidden.

Universe Polymorphism and Logical Reasoning

Two proofs that show the system handles type-level reasoning, not just computation over data.

The polymorphic identity function quantifies over types:

# Π(A:Type₀). A → A
ty = forall "A" (u 0) (a: forall "x" a (_: a));
tm = lam "A" (u 0) (a: lam "x" a (x: x));
checkHoas ty tm  # → accepted

u 0 is Type₀, the universe of small types. The function takes a type A as its first argument and a value x : A as its second. This is universe-polymorphic: the identity works at any small type. The kernel checks that A inhabits Type₀, that x inhabits A, and that the return type matches.

Ex falso quodlibet: from a proof of falsehood, derive anything.

# Π(A:Type₀). Void → A
ty = forall "A" (u 0) (a: forall "x" void (_: a));
tm = lam "A" (u 0) (a: lam "x" void (x: absurd a x));
checkHoas ty tm  # → accepted

Void is the empty type. It has no constructors, so absurd is its eliminator. Given a proof of Void (which can never be constructed), absurd produces a value of any type. This is ⊥ → A for all A. The kernel type-checks it, and nobody can ever call it. That's the point. The fact that absurd type-checks at Void → A for arbitrary A is a strong signal that the elimination rules are right.

The J Eliminator: Equational Reasoning

The J eliminator (identity elimination) is the fundamental proof tool for equalities in Martin-Löf type theory. Everything else (congruence, symmetry, transitivity, transport) is derived from J.

J takes a type A, a center point a : A, a motive P : Π(y:A). Eq(A,a,y) → Type, a base case pr : P(a, refl), a target b : A, and a proof eq : Eq(A,a,b). The computation rule: when the proof is refl, J returns the base case directly. The equality-proofs.nix file implements the standard combinators.

Congruence: if x = y, then f(x) = f(y).

# cong : Π(A B:U₀). Π(f:A→B). Π(x y:A). Eq(A,x,y) → Eq(B,f(x),f(y))
cong = lam "A" (u 0) (a: lam "B" (u 0) (b:
  lam "f" (forall "_" a (_: b)) (f:
    lam "x" a (x: lam "y" a (y:
      lam "p" (eq a x y) (p:
        j a x
          (lam "y'" a (y': lam "_" (eq a x y') (_: eq b (app f x) (app f y'))))
          refl y p))))));

The J motive says: "given y' equal to x, produce a proof that f(x) = f(y')." At the base case (y' = x), that's f(x) = f(x), which is refl. J carries this through to y.

Symmetry: if x = y, then y = x.

# sym : Π(A:U₀). Π(x y:A). Eq(A,x,y) → Eq(A,y,x)
sym = lam "A" (u 0) (a: lam "x" a (x: lam "y" a (y:
  lam "p" (eq a x y) (p:
    j a x
      (lam "y'" a (y': lam "_" (eq a x y') (_: eq a y' x)))
      refl y p))));

Transitivity: if x = y and y = z, then x = z.

# trans : Π(A:U₀). Π(x y z:A). Eq(A,x,y) → Eq(A,y,z) → Eq(A,x,z)
trans = lam "A" (u 0) (a: lam "x" a (x: lam "y" a (y: lam "z" a (z:
  lam "p" (eq a x y) (p: lam "q" (eq a y z) (q:
    j a y
      (lam "z'" a (z': lam "_" (eq a y z') (_: eq a x z')))
      p z q))))));

Transport: if x = y and P(x) holds, then P(y) holds.

# transport : Π(A:U₀). Π(P:A→U₀). Π(x y:A). Eq(A,x,y) → P(x) → P(y)
transport = lam "A" (u 0) (a: lam "P" (forall "_" a (_: u 0)) (bigP:
  lam "x" a (x: lam "y" a (y:
    lam "p" (eq a x y) (p: lam "px" (app bigP x) (px:
      j a x
        (lam "y'" a (y': lam "_" (eq a x y') (_: app bigP y')))
        px y p))))));

Transport is arguably the most important: it says that equal things are interchangeable in any type-level context. The motive is type-valued (P : A → Type₀), so this is a genuinely dependent elimination. The concrete test transports a value along a dependent type family P(b) = BoolElim(λ_.U₀, Nat, Bool, b): when b is true, P(b) is Nat; when b is false, P(b) is Bool. Zero inhabits Nat = P(true), and transport carries it along Eq(Bool, true, true) to produce a value of P(true). Still Nat, still zero, but the type-checker verified the transport path.

All four combinators type-check with fully abstract variables; the kernel proves the reasoning valid for all inputs, not just concrete examples. The equality-proofs.nix file also includes a combined proof chaining congruence with symmetry: derive succ(add(2,1)) = succ(3) via cong, then reverse it to succ(3) = succ(add(2,1)) via sym. Two J applications, nested.

From Proofs to Nix Functions

A proof checker that only checks proofs is a novelty. The v.verify pipeline closes the loop: write a term in HOAS, type-check it against a specification, evaluate it, and extract a plain Nix function. The proof is erased. What comes out is an ordinary Nix value.

# Verified addition: Nat → Nat → Nat
addFn = v.verify
  (H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat)))
  (v.fn "m" H.nat (m: v.fn "n" H.nat (n:
    v.match H.nat m {
      zero = n;
      succ = _k: ih: H.succ ih;
    })));

addFn 2 3  # → 5, as a plain Nix integer

v.verify elaborates the HOAS to de Bruijn, runs the bidirectional type checker against the Pi type, evaluates the result, and extracts a Nix value. The kernel, the proof term, the type annotation: all erased. What remains is a two-argument Nix function that computes addition.

This inverts the traditional extraction pattern. Coq extracts to OCaml, Haskell, or Scheme; you write in the proof language and generate executable code. Idris 2 uses QTT quantitative annotations to erase proof-irrelevant terms at compile time. nix-effects goes the other direction: you write Nix, apply a proof-checking layer at eval time, and the proofs disappear. The configuration keeps running. The checking was a gate.

The verified combinator library (v.fn, v.match, v.matchList, v.if_, v.matchSum, v.field, v.strEq, v.strElem) provides eliminators and primitives with automatically inferred constant motives, so you don't need to write the raw kernel term language. More examples from verified-functions.nix:

# Verified successor: Nat → Nat
succFn = v.verify (H.forall "x" H.nat (_: H.nat))
                  (v.fn "x" H.nat (x: H.succ x));
succFn 5  # → 6

# Verified boolean negation: Bool → Bool
notFn = v.verify (H.forall "b" H.bool (_: H.bool))
                 (v.fn "b" H.bool (b:
                   v.if_ H.bool b { then_ = v.false_; else_ = v.true_; }));
notFn true  # → false

# Verified predecessor: pred(0) = 0, pred(S(k)) = k
predFn = v.verify (H.forall "n" H.nat (_: H.nat))
                  (v.fn "n" H.nat (n:
                    v.match H.nat n {
                      zero = v.nat 0;
                      succ = k: _ih: k;
                    }));
predFn 5  # → 4

The list combinators work at the collection level. v.map, v.filter, v.fold each build the correct ListElim term, verify it against the kernel, and extract a Nix list:

# Verified map: increment every element
v.verify (H.listOf H.nat)
  (v.map H.nat H.nat (v.fn "x" H.nat (x: H.succ x)) myList)
# → [1 2 3]

# Verified filter: keep only zeros
v.verify (H.listOf H.nat)
  (v.filter H.nat
    (v.fn "n" H.nat (n: v.match H.bool n {
      zero = v.true_; succ = _k: _ih: v.false_; }))
    myList)
# → [0 0]

# Verified fold: sum a list
v.verify H.nat
  (v.fold H.nat H.nat (v.nat 0) addCombine myList)
# → 6

These compose. The verified-functions.nix file includes a pipeline that filters a list to remove zeros, then folds to sum the remainder, all in one verified expression:

# Input:  [0, 3, 0, 2, 1]
# Filter: [3, 2, 1]    (remove zeros)
# Sum:    6
composedResult =
  let
    filtered = v.filter H.nat nonZero input;
    addCombine = v.fn "a" H.nat (a: v.fn "acc" H.nat (acc:
      v.match H.nat a {
        zero = acc;
        succ = _k: ih: H.succ ih;
      }));
  in v.verify H.nat (v.fold H.nat H.nat (v.nat 0) addCombine filtered);

composedResult  # → 6

The kernel verifies the entire composed term (filter and fold) in one pass. If the types don't line up at any point in the pipeline, elaboration fails.

The combinator library extends beyond naturals and lists. v.field projects named fields from record types (internally nested Σ types), v.strEq compares strings in the kernel, and v.strElem checks list membership. These are the primitives that let the kernel reason about the kind of data that configuration actually contains.

Applied: Proof-Gated Derivations

The typed-derivation.nix example connects the type checker to actual Nix builds. To be upfront: this example is ad-hoc. You could enforce the same policy with a few assert statements. The point isn't the policy itself; it's that the kernel normalizes and checks it as a proof obligation rather than a runtime boolean. The interesting question is whether this scales to things assert can't express, like kernel-verified composition invariants across NixOS modules. The module system already supports value-dependent option types via config references; what it lacks is formal reasoning about whether those modules compose soundly. That isn't working yet.

The example defines a ServiceConfig record type with five string fields (bind address, port, protocol, log level, name) and a policy that the kernel evaluates as an HOAS term:

ServiceConfig = H.record [
  { name = "bind";     type = H.string; }
  { name = "logLevel"; type = H.string; }
  { name = "name";     type = H.string; }
  { name = "port";     type = H.string; }
  { name = "protocol"; type = H.string; }
];

The policy validates each field against an allowed list via v.strElem and enforces a cross-field invariant: if the bind address is 0.0.0.0 (public-facing), the protocol must be https. This logic is an HOAS term; the kernel normalizes it via NbE, not Nix's evaluator.

A second verified function computes the effective protocol. Public binds force HTTPS by construction, regardless of what the config says:

effectiveProtocol = v.verify (H.forall "s" ServiceConfig (_: H.string))
  (v.fn "s" ServiceConfig (s:
    v.if_ H.string (v.strEq (v.field ServiceConfig "bind" s) (v.str "0.0.0.0")) {
      then_ = v.str "https";
      else_ = v.field ServiceConfig "protocol" s;
    }));

The builder gates derivation construction on a proof. For each concrete config, it encodes the Nix attrset as HOAS via elaborateValue, applies the policy, and demands Refl : Eq(Bool, policy(cfg), true):

mkVerifiedService = cfg:
  let
    cfgHoas  = elaborateValue ServiceConfig cfg;
    applied  = H.app policyAnn cfgHoas;
    proofTy  = H.eq H.bool applied H.true_;
    checked  = H.checkHoas proofTy H.refl;
    protocol = effectiveProtocol cfg;
  in if checked ? error
    then throw "service '${cfg.name}' violates policy"
    else pkgs.writeShellScriptBin cfg.name ''
      echo "${cfg.name} listening on ${protocol}://${cfg.bind}:${cfg.port}"
    '';

The kernel normalizes policy(cfg) for the concrete attrset. If every field passes and the cross-field invariant holds, the result is true, Refl checks, and the derivation is built. If any check fails (say, binding 0.0.0.0 with protocol http), the result normalizes to false, the proof obligation becomes Refl : Eq(Bool, false, true), and the kernel rejects it. Nothing is built.

# Builds: localhost HTTP on port 8080 satisfies all constraints
api-server = mkVerifiedService {
  name = "api-server"; bind = "127.0.0.1";
  port = "8080"; protocol = "http"; logLevel = "info";
};

# Eval aborts: public bind with HTTP violates the cross-field invariant
insecure-public = mkVerifiedService {
  name = "insecure-public"; bind = "0.0.0.0";
  port = "80"; protocol = "http"; logLevel = "debug";
};

The proof doesn't return a boolean for someone to check later. It gates the build. An invalid config never produces a derivation. The kernel verified the policy at eval time; the extracted effectiveProtocol function runs without it. This is where dependent types meet the Nix ecosystem: a verification layer inside Nix itself that proves your configuration invariants and then gets out of the way.

The Gap: Types in the Nix Ecosystem

For context on why this matters:

Language	Type system	Dependent types	Runs in Nix	Turing-complete
Dhall	System Fω	No	No (compiles to Nix)	No
Nickel	Gradual + contracts	No	No (separate language)	Yes
CUE	Lattice unification	No	No (separate language)	No
NixOS modules	mkOption + lib.types	No	Yes	N/A
nix-effects	MLTT	Yes	Yes	Yes

Dhall deliberately excludes dependent types; System Fω does not permit mappings from values to types (Gonzalez 2016). Nickel explicitly rejects dependent types in favor of ease-of-use. CUE's lattice unification is orthogonal to type theory entirely. The NixOS module system can express value-dependent option types via config references, but doesn't lend itself to formally reasoning about whether modules compose soundly; it also silently discards addCheck validators during type merging (NixOS/nixpkgs#396021).

All three external languages require leaving Nix. nix-effects stays inside: pure Nix attribute sets and functions, checked by a kernel that is itself pure Nix.

Why This Is Sound

The Fire Triangle

Pedrot & Tabareau (2020) proved that a type theory cannot simultaneously have all three of: unrestricted substitution, dependent elimination, and observable effects. Any two are safe. All three yield inconsistency. If a closed Bool term can be observably effectful (neither true nor false), dependent elimination constructs a type family P with P(false) = Void, and the effectful term produces an inhabitant of the empty type.

Nix evaluation is pure. No mutable state, no continuations, no catchable exceptions during evaluation, no I/O at eval time. Every closed boolean reduces to exactly true or false. So the effects vertex of the triangle is empty, and embedding full MLTT in Nix is sound: the host language satisfies the purity precondition that the Fire Triangle demands.

This isn't an accident we're exploiting; it's a structural property of Nix's evaluation model. In Python or JavaScript, where side effects are everywhere, the same embedding would be unsound. Among pure functional configuration languages, Dhall and Nix are the natural hosts for dependent types, but only Nix has the laziness and general recursion needed to actually implement a kernel.

The Kernel Architecture

The type checker follows the Mini-TT architecture (Coquand et al. 2009) as refined by Kovács' elaboration-zoo: de Bruijn indices for terms, de Bruijn levels for values, closures as (env, body) pairs, syntax-directed normalization by evaluation. Three core functions:

eval  : Env → Term → Value      # interpret terms as semantic values
quote : Level → Value → Term    # read back values as normal forms
conv  : Level → Value → Value → Bool  # definitional equality via quotation

In Nix, eval maps de Bruijn terms to values represented as attribute sets. A lambda becomes { tag = "VLam"; closure = { env, body }; }, a neutral term becomes { tag = "VNe"; level; spine; } accumulating eliminations that can't reduce. quote inverts this, converting levels back to indices. conv checks definitional equality by quoting both values and comparing normal forms structurally.

NbE fits Nix's lazy evaluation naturally. When eval encounters a closure application, Nix's own evaluation mechanism shares work; the host language's laziness provides memoization of intermediate normal forms for free. Gould & Bowman (2025) confirmed that syntax-directed NbE (no type information during quotation) is 3.4× faster than type-directed variants, which is the strategy nix-effects uses.

Type checking is bidirectional (Pierce & Turner 2000): infer synthesizes a type from a term, check verifies a term against a known type. The switch between modes is driven by the syntax: lambdas are checked, applications are inferred, annotations switch from checking to inference. Felicissimo (2023) proved that this combination is sound, complete, and decidable for all normalizing dependent type theories.

Cumulative universes follow Kovács (2022): Type₀ : Type₁ : Type₂ : ... with strict subtyping between levels. A type at level i is automatically a type at level i+1. The well-foundedness of the natural number ordering on levels prevents Girard's paradox.

Effects as Data

The kernel's effect system uses Kiselyov & Ishii's (2015) freer monad encoding. Computations are either pure values or effect requests paired with continuations:

Eff r a = Pure a | Impure (Union r x) (x → Eff r a)

With a continuation queue (van der Ploeg & Kiselyov 2014), bind is O(1). Handlers follow Plotkin & Pretnar's (2013) deep handler semantics. For the proof story, what matters is this: effects are plain Nix attribute sets, first-class data rather than control flow. You can inspect an effect trace as a Nix list without executing anything. When the type checker encounters an error, handlers thread blame context through each effect, accumulating diagnostics instead of aborting.

Making It Fast Enough

Nix has no tail-call optimization. Recursion maps directly to C++ stack frames. A type checker that normalizes terms needs deep recursion; NatElim on a natural with value 100 requires 100 recursive calls through eval. This should make the whole project impossible.

The solution: builtins.genericClosure, Nix's package dependency worklist algorithm, repurposed as a trampoline. The iteration happens in C++, achieving O(1) Nix stack depth. Sternenseemann (2022) first demonstrated this but called it "pretty much useless" because thunks accumulate in non-key fields and overflow the stack when forced. The fix is embedding builtins.deepSeq in the key field:

key = builtins.deepSeq newState (step.key + 1);

This forces full evaluation at each step, preventing thunk chain formation. The result: over 1,000,000 iterations at O(1) stack depth. The NbE evaluator, the elaborator, the effect handler interpreter: all run on this trampoline. We published a detailed treatment of the technique in Trampolining Nix with genericClosure.

The kernel dispatches to the trampoline for NatElim and ListElim specifically, the eliminators that recurse over potentially large inductive values. When eval sees a successor or cons cell as the scrutinee, it converts recursive elimination into iterative worklist processing via genericClosure.

What nix-effects Doesn't Do (Yet)

Not total. The kernel uses a fuel parameter (default 10M steps) to bound normalization. If evaluation exceeds the limit, type checking fails conservatively. This makes nix-effects a partial proof checker. It verifies proofs up to a depth bound but cannot guarantee termination of all well-typed programs the way Agda or Coq do. For configuration-scale proofs the fuel is generous, but general theorem proving hits the wall.

No inductive families. The kernel supports natural numbers, booleans, lists, sums, strings, and the unit/void types as built-in inductives. User-defined inductive types and indexed families (vectors, finite sets) are not yet supported. Adding them is the main missing feature for serious proof work.

No IDE support. No language server, no jump-to-definition, no inline errors. Error messages come from nix eval with blame context threaded through the handler. Workable for small proofs, painful for anything bigger.

No parametricity in HOAS. Nix is untyped, so the HOAS encoding can't enforce parametricity at the host-language level the way Chlipala's (2008) PHOAS does in Coq. Exotic terms that a parametric host would reject can be constructed. They'll fail at type-checking time, but the failure is later than it would be in a typed host.

No scoped effects. The effect system implements flat (non-scoped) algebraic effects following Plotkin & Pretnar (2013). Scoped constructs like catch and local (Wu, Schrijvers & Hinze 2014) are not expressible.

Future work. Broekhoff & Krebbers (ICFP 2025) provide the first comprehensive formal semantics for Nix, mechanized in Rocq. A verified Nix semantics hosting a verified type checker is the natural end state. Closer to the ground: user-defined inductives, integration with NixOS mkOption for dependent module types, and the builtins.trampoline proposal (NixOS/nix#8430) for native loop support.