Kernel Architecture — nix-effects

This chapter describes the type-checking kernel: its pipeline, its primitives, and how to write verified implementations that the kernel checks and extracts back to usable Nix functions.

Two kernels

nix-effects combines an effects kernel with a type-checking kernel:

The effects kernel (src/kernel.nix, src/comp.nix, src/queue.nix) implements the freer monad with FTCQueue. It defines the Computation ADT (Pure a | Impure (Effect x) (FTCQueue x a)) and the monadic operations pure, impure, send, bind, map, seq, pipe, kleisli.
The type-checking kernel (src/tc/) implements Martin-Löf type theory with normalization by evaluation and bidirectional checking. Core modules define terms, values, evaluation, quotation, conversion, and checking; adjacent HOAS, elaboration, generic, and ornament modules provide the user-facing structure.

The type-checking kernel's higher layers use the effects kernel for error reporting. When check or infer rejects a term, it does not throw — it calls send "typeError" { msg; expected; got; term; }, producing an Impure computation. Handlers in src/effects/typecheck.nix (strict, collecting, and others) interpret that request with different strategies: strict throws on the first error, collecting accumulates errors into handler state. The TCB (eval, quote, conv) never sends effects — it only throws on kernel-invariant violations.

Type system API (src/types/)
  Record, ListOf, DepRecord, refined, Pi, Sigma, ...
       |
       | elaboration (src/tc/elaborate/, src/tc/hoas/)
       v
Type-checking kernel (MLTT, src/tc/)
       |
       | typeError sent as effect request
       v
Effects kernel (freer monad + FTCQueue, src/kernel.nix)
       |
       | handler (strict / collecting / ...) interprets effects
       v
Pure Nix

Every fx.types type carries a _kernel field — a HOAS tree that elaborates to a kernel type. .check is derived from decide(_kernel, v); .validate wraps decide in a typeCheck effect so handlers can do blame-annotated reporting; .prove type-checks HOAS proof terms; verifyAndExtract runs the full pipeline (check → eval → extract) to produce a Nix value from a HOAS implementation. Refinement types add a guard predicate that runs alongside the kernel check (check = kernelDecide(v) ∧ guard(v)), handling constraints the kernel cannot express.

The kernel pipeline

The kernel implements normalization by evaluation (NbE) with bidirectional type checking. The core pipeline has one responsibility per module family:

term.nix --> eval/ --> value.nix
                              |
                          quote.nix --> term.nix
                              |
                          conv.nix
                              |
                          check/

Module	Function	Signature
`term.nix`	Term constructors	`mkVar`, `mkPi`, `mkLam`, `mkApp`, ...
`eval/`	Evaluation	`Env × Tm -> Val`
`value.nix`	Value constructors	`VLam`, `VPi`, `VPair`, `VMu`, ...
`quote.nix`	Quotation	`ℕ × Val -> Tm`
`conv.nix`	Conversion checking	`ℕ × Val × Val -> Bool`
`check/`	Type checking	`Ctx × Tm × Val -> Tm` / `Ctx × Tm -> Tm × Val`

Terms (Tm) are the syntax — de Bruijn indexed expressions with explicit binding structure. Values (Val) are the semantics — fully normalized forms where lambdas carry defunctionalized closures. The TCB does not use Nix lambdas as semantic closures. Evaluation converts terms to values. Quotation reads values back to terms. Conversion checks whether two values are definitionally equal by comparing their semantic structure.

The type checker is bidirectional:

check(Γ, t, T) — check that term t has type T (type-directed)
infer(Γ, t) — infer the type of term t (term-directed)
checkTypeLevel(Γ, T) — compute the universe level of a type

Trust model

The kernel has three layers with decreasing trust requirements:

Layer 0 — Trusted Computing Base. eval, quote, conv. Pure functions. No side effects. No imports from the effect system. Bugs here compromise soundness.

Layer 1 — Semi-trusted. check, infer, checkTypeLevel. Uses the TCB and sends effects for error reporting. Bugs may produce wrong error messages or reject valid terms, but cannot cause unsoundness.

Layer 2 — Untrusted. The elaborator (hoas/, elaborate/). Translates surface syntax to core terms. Can have arbitrary bugs without compromising safety — the kernel verifies the output.

Axiomatized primitives

The kernel understands eight Nix primitive types as axioms. Each has a type former, a literal constructor, and a typing rule. None have eliminators — the kernel says "String is a type at level 0" and "a string literal inhabits String" but cannot structurally decompose these values.

Nix type	Kernel type	Literal
`string`	`String`	`StringLit(s)`
`int`	`Int`	`IntLit(n)`
`float`	`Float`	`FloatLit(f)`
`set`	`Attrs`	`AttrsLit`
`path`	`Path`	`PathLit`
`derivation`	`Derivation`	`DerivationLit`
`lambda`	`Function`	`FnLit`
(any)	`Any`	`AnyLit`

Path is decided by builtins.isPath; Derivation is decided by (v: builtins.isAttrs v && (v.type or null) == "derivation"). The two share no values: Path rejects attrsets, Derivation rejects strings and non-derivation attrsets.

The structural type formers with kernel introduction and elimination rules are Unit, Sigma, Pi, bootstrap identity/coproduct infrastructure, propositional truncation (Squash), universe lifting, function extensionality as an axiom, and the indexed-description family (Desc I, μ, interpD, allD, everywhereD, desc-ind). Public Nat, List, Sum, Bool, Eq, Fin, Vec, and W are generated through descriptions and the datatype macro. Their eliminators are generated adapters over desc-ind.

This gives the kernel enough structure to compute with generated inductive families, pairs, and functions, while treating strings, integers, and other Nix-native types as opaque tokens.

Axiomatized primitives are critical for real-world use. Without them, verified modules can only work over Nat/Bool/List/Sigma/Sum. With them, modules can handle target classes (String), dependency counts (Int), declaration records (nested Sigma/Attrs), and so on.

HOAS: the surface API

Writing de Bruijn indexed terms by hand is error-prone. The HOAS (Higher-Order Abstract Syntax) layer lets you use Nix lambdas for variable binding. The public API is fx.types.hoas.

Type combinators

H = fx.types.hoas;

H.nat                         # Nat
H.bool                        # Bool
H.string                      # String
H.int_                        # Int
H.float_                      # Float
H.unit                        # Unit (nullary product)
H.void                        # Void (empty type)
H.listOf H.nat                # List Nat
H.sum H.nat H.bool            # Nat + Bool
H.forall "x" H.nat (_: H.bool)  # Π(x : Nat). Bool
H.sigma "x" H.nat (_: H.bool)   # Σ(x : Nat). Bool
H.u 0                         # U₀ (universe of small types)

Term combinators

# Lambda: λ(x : Nat). x
H.lam "x" H.nat (x: x)

# Application
H.app f arg

# Natural number literals
H.zero                        # 0
H.succ H.zero                 # 1
H.natLit 42                   # 42 (sugar for 42 succs)

# Boolean literals
H.true_
H.false_

# Pairs
H.pair fst snd

# Projections
H.fst_ p
H.snd_ p

# Sum injections
H.inl leftTy rightTy term
H.inr leftTy rightTy term

# String / Int / Float literals
H.stringLit "hello"
H.intLit 42
H.floatLit 3.14

# Type annotation
H.ann term type

Eliminators

# Natural number induction
H.ind motive base step scrut

# Boolean elimination (k : Level is the motive's universe level)
H.boolElim k motive onTrue onFalse scrut

# List elimination
H.listElim elemType motive onNil onCons scrut

# Sum elimination
H.sumElim leftTy rightTy motive onLeft onRight scrut

# Equality elimination (J)
H.j type lhs motive base rhs eq

How HOAS compiles

Binding combinators produce HOAS markers — lightweight attrsets that stand for bound variables at a specific depth. The elaborate function (in hoas.nix) converts these to de Bruijn indexed Tm terms:

H.lam "x" H.nat (x: H.succ x)
  │
  │ HOAS: x is a marker { _hoas = true; level = 0; }
  │
  ▼ elaborate (depth=0)
  │
  │ marker at level 0 -> T.mkVar(0 - 0 - 1) = T.mkVar(0)
  │
  ▼
Lam("x", Nat, Succ(Var(0)))   ← de Bruijn term

The elaboration of nested binding forms is trampolined via builtins.genericClosure for stack safety on deeply nested terms.

The elaboration bridge

The elaboration bridge (elaborate.nix) connects the user-facing type system to the kernel. It has six operations:

Operation	Signature	Direction
`elaborateType`	`FxType -> HoasTree`	type system -> kernel
`elaborateValue`	`HoasTree × NixVal -> HoasTree`	Nix value -> kernel term
`extract`	`HoasTree × Val -> NixValue`	kernel value -> Nix value
`decide`	`HoasTree × NixVal -> Bool`	decision procedure
`decideType`	`FxType × NixVal -> Bool`	elaborate type, then decide
`verifyAndExtract`	`HoasTree × HoasTree -> NixValue`	full pipeline

elaborateType

Converts an fx.types type into a HOAS tree. Dispatches on three things, in order:

The _kernel field (types built via mkType with kernelType)
Structural fields (Pi: domain/codomain, Sigma: fstType/sndFamily)
Name convention ("Bool" -> H.bool, "String" -> H.string, etc.)

elaborateValue

Converts a Nix value into a HOAS term, guided by a HOAS type. For example, given H.nat and the Nix integer 3, produces H.succ (H.succ (H.succ H.zero)). Given H.string and "hello", produces H.stringLit "hello".

extract — the reverse direction

extract converts kernel values back to Nix values. It is the reverse of elaborateValue. This is where the verification story becomes interesting: you write an implementation as a HOAS term, the kernel verifies it, eval produces a kernel value, and extract converts the result to a usable Nix value.

# extract : HoasTree -> Val -> NixValue
extract H.nat (VDescCon ... <succ payload>)        # -> 2
extract H.bool (VDescCon ... <true payload>)       # -> true
                                                     # H.bool is derived
extract H.string (VStringLit "hi")                 # -> "hi"
extract (H.listOf H.nat) (VDescCon ... <cons ...>) # -> [1 2 3]
extract (H.forall "x" ...) (VLam ...)              # -> Nix function (!)

The Pi case is the most important. Extracting a verified function produces a Nix function that:

Elaborates its argument into a kernel value (Nix -> kernel)
Applies the kernel-verified closure
Extracts the result back (kernel -> Nix)

Correct by construction — the kernel verified the term, eval produced the closure, extract wraps with value conversion at the boundaries.

decide

The decision procedure. Returns true iff both elaboration and kernel type-checking succeed:

decide = hoasTy: value:
  let
    result = builtins.tryEval (
      let
        hoasVal = elaborateValue hoasTy value;
        checked = H.checkHoas hoasTy hoasVal;
      in !(checked ? error)
    );
  in result.success && result.value;

This is the function that mkType uses to derive .check. Every type's .check is v: decide(kernelType, v) — no hand-written predicates.

verifyAndExtract — the full pipeline

Type-check a HOAS term against a HOAS type, then extract the result:

verifyAndExtract = hoasTy: hoasImpl:
  let
    checked = H.checkHoas hoasTy hoasImpl;
  in if checked ? error
    then throw "verifyAndExtract: type check failed"
    else
      let
        tm = H.elab hoasImpl;         # HOAS -> de Bruijn
        val = E.eval [] tm;           # evaluate to Val
      in extract hoasTy val;          # Val -> Nix value

Convenience combinators

Raw HOAS is verbose. The convenience combinator layer (fx.types.verified, accessed as v) provides sugar that produces valid HOAS term trees:

v = fx.types.verified;
H = fx.types.hoas;

Literals

v.nat 5          # H.natLit 5
v.str "hello"    # H.stringLit "hello"
v.int_ 42        # H.intLit 42
v.float_ 3.14    # H.floatLit 3.14
v.true_          # H.true_
v.false_         # H.false_
v.null_          # H.tt (unit)

Binding forms

# Lambda: λ(x : Nat). body
v.fn "x" H.nat (x: body)

# Let: let x : Nat = 5 in body
v.let_ "x" H.nat (v.nat 5) (x: body)

Eliminators with inferred motives

The convenience combinators construct the required motive automatically from the result type. The motive is always constant (non-dependent): λ_. resultTy.

# Boolean: if b then 1 else 0
v.if_ H.nat v.true_ { then_ = v.nat 1; else_ = v.nat 0; }

# Natural number: pattern match on n
v.match H.nat n {
  zero = v.nat 42;
  succ = k: ih: H.succ ih;
}

# List: fold over elements
v.matchList H.nat H.nat list {
  nil = v.nat 0;
  cons = h: t: ih: H.succ ih;   # count elements
}

# Sum: case split
v.matchSum H.nat H.bool H.nat scrut {
  left = x: H.succ x;
  right = _: v.nat 0;
}

Derived combinators

# Map: apply f to each element
v.map H.nat H.nat succFn myList

# Fold: combine elements with accumulator
v.fold H.nat H.nat (v.nat 0) addFn myList

# Filter: keep elements matching predicate
v.filter H.nat isZeroFn myList

Pairs and sums

v.pair fstTerm sndTerm sigmaType
v.fst p
v.snd p
v.inl leftTy rightTy term
v.inr leftTy rightTy term
v.app f arg

The verify pipeline

v.verify wraps verifyAndExtract — type-check and extract in one call:

v.verify type implementation
# = verifyAndExtract type implementation

Writing verified implementations

The key insight: instead of writing Nix functions and trying to elaborate them into kernel terms (which fails for closures), write implementations as HOAS terms and extract Nix functions out. This is the approach taken by Coq (extraction), Idris (compilation), and F*.

Example: verified addition

let
  H = fx.types.hoas;
  v = fx.types.verified;

  addTy = H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat));
  addImpl = 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;
    }));

  # Kernel verifies: addImpl : Π(m:Nat). Π(n:Nat). Nat
  # Then extracts a 2-argument Nix function
  add = v.verify addTy addImpl;
in
  add 2 3    # -> 5

What happens step by step:

v.verify calls H.checkHoas addTy addImpl — the kernel type-checks the HOAS term against the HOAS type
H.elab addImpl converts HOAS to de Bruijn indexed Tm
E.eval [] tm evaluates to a VLam value (a Nix closure via NbE)
extract addTy val wraps the VLam as a Nix function that elaborates arguments at call boundaries

The resulting add is an ordinary Nix function. Call it with Nix integers. At each call, the argument is elaborated into a kernel value, the verified closure runs, and the result is extracted back.

Example: verified list operations

let
  H = fx.types.hoas;
  v = fx.types.verified;

  # Successor function: Nat -> Nat
  succFn = v.fn "x" H.nat (x: H.succ x);

  # Map successor over a list
  input = H.cons H.nat (v.nat 0)
    (H.cons H.nat (v.nat 1)
      (H.cons H.nat (v.nat 2) (H.nil H.nat)));

  result = v.verify (H.listOf H.nat) (v.map H.nat H.nat succFn input);
in
  result    # -> [1 2 3]

Example: verified filter

let
  H = fx.types.hoas;
  v = fx.types.verified;

  # isZero : Nat -> Bool
  isZero = v.fn "n" H.nat (n:
    v.match H.bool n {
      zero = v.true_;
      succ = _k: _ih: v.false_;
    });

  input = H.cons H.nat (v.nat 0)
    (H.cons H.nat (v.nat 1)
      (H.cons H.nat (v.nat 0)
        (H.cons H.nat (v.nat 2) (H.nil H.nat))));

  result = v.verify (H.listOf H.nat) (v.filter H.nat isZero input);
in
  result    # -> [0 0]

The verification spectrum

The architecture supports a spectrum of assurance levels. Each level offers a different trade-off between verification strength and implementation cost.

Level 1: Contract

The baseline. Types check values at introduction via .check (which calls decide under the hood). No HOAS, no proof terms — just write normal Nix code and let the type system validate data at boundaries.

let
  inherit (fx.types) String refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  # Refinement with string guard — kernel checks String, guard checks membership
  LogLevel = refined "LogLevel" String
    (x: builtins.elem x [ "debug" "info" "warn" "error" ]);
in {
  module = TargetClass.check "module"; # true
  fleet = TargetClass.check "fleet"; # false

  info  = LogLevel.check "info";    # true
  trace = LogLevel.check "trace";   # false — not in the allowed set

  # Effectful validation with blame context
  result = fx.run (TargetClass.validate "fleet")
    fx.effects.typecheck.collecting [];
  # result.state = [ { context = "TargetClass"; ... } ]
}

Cost: Zero — write normal Nix. The kernel runs behind the scenes. Refinement types compose: ListOf TargetClass checks that every element is a known renderer class. The kernel elaborates the list, the guard runs per element.

Level 2: Boundary

Data values are checked by the kernel at module interfaces. Types carry kernelType and .check is derived from the kernel's decide procedure. This is what every type does by default.

let
  inherit (fx.types) Bool String ListOf DepRecord refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  # Dependent record: generated aspects must target a known renderer class.
  # The kernel elaborates the record to a Sigma chain, checks each field's type
  # against its kernelType, and the guard on TargetClass validates membership.
  AspectDecl = DepRecord [
    { name = "generated"; type = Bool; }
    { name = "target"; type = self:
        if self.generated then TargetClass else String; }
    { name = "requires"; type = _: ListOf String; }
  ];
in {
  ok = AspectDecl.checkFlat {
    generated = true;
    target = "module";
    requires = [ "toolchain" ];
  };   # true

  bad = AspectDecl.checkFlat {
    generated = true;
    target = "fleet";
    requires = [ ];
  };   # false

  external = AspectDecl.checkFlat {
    generated = false;
    target = "external-renderer";
    requires = [ ];
  };   # true
}

Cost: Low — add kernelType to custom types (built-in types already have it). The dependent record pattern shows how boundary checking scales: the kernel handles structural verification, guards handle domain predicates, and the dependency between fields is resolved at check time.

Level 3: Property

Universal properties verified via proof terms. Write proofs in HOAS that the kernel checks. The proof term is separate from the implementation — you write separate Nix code alongside, and the kernel verifies that the stated property holds.

let
  H = fx.types.hoas;
  inherit (H) nat bool eq forall refl checkHoas;

  # Define addition by structural recursion on the first argument
  add = m: n:
    H.ind (H.lam "_" nat (_: nat)) n
      (H.lam "k" nat (_: H.lam "ih" nat (ih: H.succ ih))) m;

  not_ = b:
    H.boolElim 0 (H.lam "_" bool (_: bool)) H.false_ H.true_ b;
in {
  # Prove: 3 + 5 = 8
  # The kernel normalizes add(3,5) via generated natural induction,
  # then confirms Refl witnesses Eq(Nat, 8, 8).
  arithmetic = (checkHoas
    (eq nat (add (H.natLit 3) (H.natLit 5)) (H.natLit 8))
    refl).tag == "refl";

  # Prove: not(not(true)) = true
  # The kernel evaluates two BoolElim steps and confirms the result.
  doubleNeg = (checkHoas
    (eq bool (not_ (not_ H.true_)) H.true_)
    refl).tag == "refl";

  # Prove: append([1,2], [3]) = [1,2,3]
  # Generated list induction unfolds the first list onto [3].
  listAppend = let
    list12  = H.cons nat (H.natLit 1) (H.cons nat (H.natLit 2) (H.nil nat));
    list3   = H.cons nat (H.natLit 3) (H.nil nat);
    list123 = H.cons nat (H.natLit 1) (H.cons nat (H.natLit 2)
                (H.cons nat (H.natLit 3) (H.nil nat)));
    append = xs: ys:
      H.listElim nat (H.lam "_" (H.listOf nat) (_: H.listOf nat)) ys
        (H.lam "h" nat (h: H.lam "t" (H.listOf nat) (_:
          H.lam "ih" (H.listOf nat) (ih: H.cons nat h ih)))) xs;
  in (checkHoas (eq (H.listOf nat) (append list12 list3) list123) refl).tag == "refl";
}

Cost: Medium — write proofs in HOAS. The proofs are separate from production code, so you can add them incrementally to an existing codebase without rewriting anything.

Level 4: Full

The implementation IS the proof term. Write the entire implementation in HOAS, the kernel verifies it, and extract produces a Nix function that is correct by construction. The extracted function is plain Nix — no kernel overhead at call time.

let
  H = fx.types.hoas;
  v = fx.types.verified;

  AspectDecl = H.record [
    { name = "name";     type = H.string; }
    { name = "target";   type = H.string; }
    { name = "requires"; type = H.listOf H.string; }
  ];

  targets =
    H.cons H.string (v.str "module")
      (H.cons H.string (v.str "file")
        (H.cons H.string (v.str "package")
          (H.cons H.string (v.str "check") (H.nil H.string))));

  # Verified aspect validator: checks that the target class is supported.
  # The kernel type-checks the implementation against AspectDecl -> Bool,
  # verifies field projections, and confirms strElem composes correctly.
  validateAspect = v.verify (H.forall "a" AspectDecl (_: H.bool))
    (v.fn "a" AspectDecl (a:
      v.strElem (v.field AspectDecl "target" a) targets));

  # Verified addition: structural recursion extracted as Nix function
  add = 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;
      })));
in {
  sum   = add 2 3;    # -> 5, correct by construction
  ok    = validateAspect {
    name = "workspace-shell";
    target = "module";
    requires = [ "toolchain" ];
  };   # -> true
  bad   = validateAspect {
    name = "workspace-aspect";
    target = "fleet";
    requires = [ ];
  };   # -> false
}

Cost: High — write the implementation in HOAS. Best reserved for code where the cost is justified by the assurance. See the Proof Guide for a progressive tutorial from simple proofs through the J eliminator to verified extraction of plain Nix functions.

How mkType derives .check

Every type is built by mkType (in foundation.nix). The kernel type IS the type. .check is its decision procedure, derived mechanically:

_kernel : HoasType        ← the type IS this
check : Value -> Bool       ← derived from decide(kernelType, value)
kernelCheck : Value -> Bool ← same as check (legacy alias)
prove : HoasTerm -> Bool    ← kernel proof checking
universe : Int             ← computed from checkTypeLevel(kernelType)

For refinement types, an optional guard adds a runtime predicate on top of the kernel check: check = decide(kernelType, v) && guard(v). The guard handles predicates the kernel cannot express — for example, x >= 0 for natural numbers, or membership in a finite set for validated strings.

Limitations

Nix closures are opaque. decide(H.forall ..., f) can only check builtins.isFunction f. For full function verification, write the function in HOAS and use v.verify to extract.

Refinement predicates are opaque. The kernel cannot represent x >= 0 as a type-level assertion. Refinement types always need a hand-written guard predicate.

builtins.tryEval is limited. It only catches throw and assert false. Cross-type comparison errors, boolean coercion errors, and missing attribute access crash Nix uncatchably. This affects decide for types whose elaboration might trigger such errors.

Dependent extraction is limited. Extracting a dependent Pi or Sigma requires a sentinel test to detect non-dependence. If the type family is truly dependent, extraction throws and requires explicit type annotation.

Opaque types cannot be extracted. Attrs, Path, Derivation, Function, and Any are axiomatized — the kernel knows they exist but discards their payloads. Extracting a value of these types throws. They work for type-checking (deciding membership) but not for the full verify-and-extract pipeline.

Extraction has boundary cost. Extracted functions elaborate their arguments at every call (Nix -> kernel value -> apply -> extract -> Nix). For hot paths, the contract layer's .check fast path is more efficient.