↝ payload'
──────────────────────
Γ ⊢ DescCon(D, i, payload) ⇐ ty
↝ DescCon(D', i', payload')
```
`checkDescAtAnyLevel(Γ, D)` is the bidirectional bridge: it
elaborates `D` at the most specific admissible level synthesised
from `D`'s structure, returning both the elaborated term and the
inferred `K`. Equivalent to `∃K. Γ ⊢ D ⇐ Desc^K Î`. The bidirectional
discipline at index positions is preserved: canonical intros (`tt`,
`zero`, `refl`, …) at the index slot remain checkable-only.
---
## 8. Universe Rules
### 8.1 Universe formation
```
U(i) : U(i + 1) for all i ≥ 0
```
### 8.2 Type former levels
Universe levels are computed by `checkTypeLevel`, which returns
`{ term; level; }` from the **typing derivation**, not from
post-hoc value inspection. This avoids the problem of unknown
levels for neutral type variables. We write `level(A)` as shorthand
for `checkTypeLevel(Γ, A).level`.
```
checkTypeLevel(Γ, Nat) = { Nat, 0 }
checkTypeLevel(Γ, Unit) = { Unit, 0 }
checkTypeLevel(Γ, String) = { String, 0 }
checkTypeLevel(Γ, Int) = { Int, 0 }
checkTypeLevel(Γ, Float) = { Float, 0 }
checkTypeLevel(Γ, Attrs) = { Attrs, 0 }
checkTypeLevel(Γ, Path) = { Path, 0 }
checkTypeLevel(Γ, Function) = { Function, 0 }
checkTypeLevel(Γ, Any) = { Any, 0 }
checkTypeLevel(Γ, List(A)) = { List(A'), level(A) }
checkTypeLevel(Γ, Sum(A, B)) = { Sum(A',B'), max(level(A), level(B)) }
checkTypeLevel(Γ, Pi(n, A, B)) = { Pi(n,A',B'), max(level(A), level(B)) }
checkTypeLevel(Γ, Sigma(n,A,B))= { Sigma(n,A',B'), max(level(A), level(B)) }
checkTypeLevel(Γ, Eq(A, a, b)) = { Eq(A',a',b'), level(A) }
checkTypeLevel(Γ, U(i)) = { U(i), i + 1 }
-- Fallback: infer type, require VU(i), extract i
checkTypeLevel(Γ, T) = { T', i } where Γ ⊢ T ⇒ VU(i)
```
The fallback handles neutral type expressions (variables,
applications) by inferring their type and requiring it to be a
universe. This correctly propagates levels through type variables:
if `B : U(1)`, then `checkTypeLevel` on `B` infers `VU(1)` and
returns level 1.
### 8.3 Cumulativity
A type `A` at level `i` is also a type at level `j` for all `j > i`.
This is implemented by accepting `conv(d, VU(i), VU(j))` when `i ≤ j`
**in the Sub rule only** (checking mode, when comparing an inferred
universe against an expected universe). The `conv` function itself
uses strict equality `i == j`.
The cumulativity check is in `check`:
```
-- In the Sub rule:
-- If inferredTy = VU(i) and expectedTy = VU(j) and i ≤ j: accept
-- Otherwise: conv(Γ.depth, inferredTy, expectedTy) must hold
```
### 8.4 Universe consistency
The kernel MUST reject `U(i) : U(i)`. This is guaranteed by the
level computation: `level(U(i)) = i + 1`, so `U(i)` lives at level
`i + 1`, not `i`. Self-containing universes cannot be constructed.
This prevents Girard's paradox (Girard 1972), which requires a type
that contains itself. Hurkens (1995) gives the compact MLTT rendering
of the inconsistency proof. Universe stratification is the standard
fix, and it is why the kernel enforces `level(U(i)) = i + 1`.
### 8.5 Level sort
`Level` is a Tarski-style sort of universe levels, with constructors
`zero`, `suc`, and `max`. It inhabits the lowest universe:
```
──────────────────────
Γ ⊢ Level type ↝ Level
──────────────────────
Γ ⊢ Level ⇒ VU(0) ↝ Level
──────────────────────
Γ ⊢ LevelZero ⇐ Level ↝ LevelZero
Γ ⊢ k ⇐ Level ↝ k'
──────────────────────
Γ ⊢ LevelSuc(k) ⇐ Level ↝ LevelSuc(k')
Γ ⊢ a ⇐ Level ↝ a'
Γ ⊢ b ⇐ Level ↝ b'
──────────────────────
Γ ⊢ LevelMax(a, b) ⇐ Level ↝ LevelMax(a', b')
```
Conversion modulo the semilattice laws (idempotence of `max`, `suc`
distribution over `max`, zero absorption) is delegated to `convLevel`
(§6.6); structural conversion on Level values without normalisation
would be too coarse (e.g. `max(zero, k)` and `k` would not compare
equal).
The `Level` sort enables predicative universe polymorphism: the
description type `Desc^k I` and universe `U(k)` quantify over
arbitrary levels via `Π(k:Level). …`. Rank-1 only — `Level` itself
has no eliminator, and admitting one would break parametricity over
the semilattice quotient (any eliminator would be observably
sensitive to the canonical form chosen by `convLevel`).
---
## 9. Fuel Mechanism
### 9.1 Evaluation fuel
Every call to `evalF` receives a fuel parameter and decrements it
by one before evaluating the term. When fuel reaches 0:
```
evalF(fuel=0, ρ, t) = THROW "normalization budget exceeded"
```
The kernel aborts via `throw`. Layer 0 (TCB) has no access to the
effect system by design, so fuel exhaustion and kernel invariant
violations both manifest as Nix-level throws caught by `tryEval`.
Callers should treat any throw from the evaluator as "term not
verified" — the distinction between fuel exhaustion and a kernel bug
is in the error message text, not the failure mechanism.
### 9.2 Default budget
The default fuel budget is 10,000,000 reduction steps. This is
configurable by the caller via `evalF`. No minimum is enforced —
callers may pass arbitrarily low fuel, which will cause immediate
`throw` on the first eval step.
### 9.3 Fuel accounting
Fuel is **per-path**, not a global counter. Each call to `evalF`
captures `f = fuel - 1` and passes `f` to all sub-evaluations of
that term. When evaluating `App(t, u)`, both `evalF(f, ρ, t)` and
`evalF(f, ρ, u)` receive the same `f`. This means fuel bounds the
**depth** of any single evaluation path, not the total work across
all paths.
For a balanced binary tree of N applications, the total work is
O(2^depth × fuel), not O(fuel). This is inherent to pure Nix —
there is no mutable global counter. The fuel mechanism guarantees
termination (every path eventually hits 0) but does not bound total
computation time.
All fuel consumption flows through `evalF`:
- Direct term evaluation (each `evalF` call decrements fuel by 1)
- Beta-reduction in `vApp` consumes fuel indirectly via
`instantiateF`, which calls `evalF`
- Iota-reduction in recursive eliminators (`vNatElimF`,
`vListElimF`, `vSumElimF`) consumes fuel indirectly via `vAppF`
Non-recursive eliminators (`vJ`) complete in O(1) and do not call
`evalF`. Structural operations (building values, pattern matching
on tags) do not consume fuel.
### 9.4 Fuel threading in trampolined eliminators
Trampolined eliminators (`vNatElimF`, `vListElimF`) flatten
recursive chains into `builtins.foldl'` loops. Each fold step
threads fuel through the accumulator:
```
foldl'(λ{acc, fuel}. λi.
if fuel ≤ 0 then THROW "normalization budget exceeded"
else { acc = step(fuel, acc, chain[i]); fuel = fuel - 1; })
{acc = base; fuel = fuel}
[1..n]
```
This ensures that an N-element chain consumes N units of fuel from
the fold, plus whatever fuel each step application consumes
internally. Without this threading, each step would get the
original fuel budget, giving an effective budget of N × fuel.
The worst-case complexity of a threaded fold is O(fuel²): at step
*i*, the inner `vAppF` receives `fuel - i` as its own per-path
budget. Summing over all steps gives Σ(fuel - i) ≈ fuel²/2. To
achieve O(fuel), `vAppF` would need to return remaining fuel — an
invasive signature change. The quadratic residual is inherent to
per-path fuel semantics and is a strict improvement over the
pre-threading O(N × fuel) with unbounded N.
### 9.5 Fuel consumption in constructor chains
Trampolined Succ and Cons evaluation (`eval(ρ, Succ(t))` and
`eval(ρ, Cons(A, h, t))`) flatten chains of n constructors and
deduct n fuel units from the budget before evaluating the base.
A chain of n Succ constructors consumes n+1 fuel (1 for the entry
evaluation, n for the chain deduction). Cons chains additionally
thread remaining fuel through the fold: each fold step evaluates
the element type and head with the current fuel budget, then
decrements by 1 (matching the eliminator fuel threading pattern
from §9.4). This is a third fuel consumption site alongside
`evalF` decrements and eliminator fold steps.
---
## 10. Properties the Implementation Must Satisfy
### 10.1 Soundness (non-negotiable)
If the kernel accepts `Γ ⊢ t : A`, then `t` is a valid term of
type `A` in MLTT with the specified type formers and universe
hierarchy. Formally:
**If `check(Γ, t, A)` succeeds, then `Γ ⊢ t : A` is derivable
in the declarative typing rules of MLTT.**
Equivalently: the kernel never accepts an ill-typed term.
### 10.2 Determinism
For any input `(Γ, t, A)`, the kernel produces the same result
on every invocation. There is no randomness, no system-dependent
behavior, no sensitivity to evaluation order (beyond fuel
exhaustion, which always rejects).
### 10.3 Termination
For any input `(Γ, t, A)`, the kernel terminates. It either:
- Accepts (returns the elaborated term)
- Rejects with a type error (via effect)
- Rejects with fuel exhaustion
- Crashes with a kernel bug diagnostic (throw)
It never loops. The fuel mechanism guarantees this.
### 10.4 Evaluation roundtrip
For any well-typed term `t` and environment `ρ` consistent with
the context:
```
quote(d, eval(ρ, quote(d, eval(ρ, t)))) = quote(d, eval(ρ, t))
```
Evaluation followed by quotation is idempotent. The result is a
normal form.
### 10.5 Conversion reflexivity
For any value `v`:
```
conv(d, v, v) = true
```
### 10.6 Conversion symmetry
For any values `v₁, v₂`:
```
conv(d, v₁, v₂) = conv(d, v₂, v₁)
```
### 10.7 Conversion transitivity
For any values `v₁, v₂, v₃`:
```
conv(d, v₁, v₂) ∧ conv(d, v₂, v₃) ⟹ conv(d, v₁, v₃)
```
### 10.8 Type preservation under evaluation
If `Γ ⊢ t : A` and `eval(Γ.env, t) = v`, then `v` represents a
value of type `A`. This is not directly testable (values don't
carry types) but is ensured by the correctness of the evaluation
rules.
### 10.9 Strong normalization (for well-typed terms)
For any well-typed term `t`, `eval` terminates without exhausting
fuel for a sufficiently large fuel budget. The fuel mechanism is
a practical safeguard, not a theoretical necessity for well-typed
terms.
---
## 11. Derived Test Cases
Every rule in this spec generates at least one positive test (the
rule applies and succeeds) and one negative test (the rule's
premises are violated and the kernel rejects).
### 11.1 Required positive tests (kernel must ACCEPT)
```
-- Identity
⊢ Refl : Eq(Nat, Zero, Zero)
-- Function type
⊢ Lam(x, Nat, Var(0)) : Pi(x, Nat, Nat)
-- Application
f : Pi(x, Nat, Nat) ⊢ App(f, Zero) : Nat
-- Dependent function
⊢ Lam(A, U(0), Lam(x, Var(0), Var(0))) : Pi(A, U(0), Pi(x, A, A))
-- Sigma pair
⊢ Pair(Zero, Tt, Sigma(x, Nat, Unit)) : Sigma(x, Nat, Unit)
-- Nat induction: 0 + 0 = 0
⊢ Refl : Eq(Nat, NatElim(_, Zero, _, Zero), Zero)
-- List
⊢ Cons(Nat, Zero, Nil(Nat)) : List(Nat)
-- Sum injection
⊢ Inl(Nat, Unit, Zero) : Sum(Nat, Unit)
-- Universe hierarchy
⊢ U(0) : U(1)
⊢ U(1) : U(2)
⊢ Nat : U(0)
⊢ Pi(x, Nat, Nat) : U(0)
-- Let binding
⊢ Let(x, Nat, Zero, Var(0)) : Nat
-- Cumulativity: Nat : U(0) should also be accepted at U(1)
-- StrEq: type inference returns the derived H.bool
-- (= μ ⊤ (plus (retI tt) (retI tt)) tt; see §4.11)
⊢ StrEq(StringLit("a"), StringLit("b")) : H.bool
-- StrEq reduction: equal strings reduce to the derived true_ value;
-- unequal strings reduce to false_. Both witnessed via Refl over the
-- derived-bool form. Expressing this rule at the Tm level requires
-- the plus/μ machinery; see the examples/verified-functions.nix
-- fixture `recordStrEqMatch` for an executable test.
```
### 11.2 Required negative tests (kernel must REJECT)
```
-- Type mismatch
⊢ Zero : Unit REJECT
-- Universe violation
⊢ U(0) : U(0) REJECT
-- Refl on unequal terms
⊢ Refl : Eq(Nat, Zero, Succ(Zero)) REJECT
-- Application of non-function
⊢ App(Zero, Zero) REJECT
-- Projection of non-pair
⊢ Fst(Zero) REJECT
-- Wrong eliminator scrutinee
⊢ NatElim(_, _, _, Tt) REJECT (Tt : Unit, not Nat)
-- Unbound variable
⊢ Var(0) (in empty context) REJECT
-- StrEq on non-string
⊢ StrEq(Zero, StringLit("foo")) REJECT (lhs is Nat, expected String)
-- Ill-typed pair
⊢ Pair(Zero, Zero, Sigma(x, Nat, Unit)) REJECT (snd is Nat, expected Unit)
```
### 11.3 Required stress tests
```
-- Large Nat: S^5000(0) : Nat ACCEPT (trampoline)
-- Large List: cons^5000 : List(Nat) ACCEPT (trampoline)
-- NatElim on S^5000(0) ACCEPT (trampoline)
-- ListElim on cons^5000 ACCEPT (trampoline)
-- Succ elaboration: elab-succ-5000 ACCEPT (trampoline)
-- Cons elaboration: elab-cons-5000 ACCEPT (trampoline)
-- Deeply nested Pi: Pi(x₁, ..., Pi(xₙ, Nat, Nat)...) for n=500 ACCEPT
-- Fuel exhaustion: artificially low fuel on complex term REJECT (fuel)
-- Fuel threading: NatElim fold decrements fuel per step ACCEPT
-- Fuel threading: ListElim fold decrements fuel per step ACCEPT
```
### 11.4 Required roundtrip tests
For each value form, verify:
```
quote(d, eval(ρ, t)) = normal_form(t)
```
where `normal_form(t)` is the expected normal form.
---
## 12. Notation Index
| Symbol | Meaning |
|--------|---------|
| Γ | Typing context |
| ρ | Value environment |
| d | Binding depth (for levels ↔ indices) |
| ⊢ | Typing judgment |
| ⇐ | Checking mode |
| ⇒ | Synthesis mode |
| ↝ | Elaborates to |
| ≡ | Definitional equality |
| Π | Dependent function type |
| Σ | Dependent pair type |
| ℕ | Natural numbers |
| 𝔹 | Booleans (derived: `μ ⊤ (plus (retI tt) (retI tt)) tt`) |
| ⊤ | Unit type |
| ⊥ | Void / empty type (derived: `Fin 0`) |
| U(i) | Universe at level i |
| Id_A(a,b) | Identity type |
| TCB | Trusted computing base |
| WHNF | Weak head normal form |
| NbE | Normalization by evaluation |
| THROW | Kernel invariant violation (crash) |
| REJECT | Term rejected (via effect or fuel) |
---
## 13. Known Limitations
The following are documented implementation choices or limitations,
not bugs. They are recorded here so auditors do not rediscover them.
### 13.1 Pair quotation uses dummy type annotation
`quote(d, VPair(a, b))` produces `Pair(quote(d,a), quote(d,b), Unit)`
— the type annotation is always `Unit` regardless of the actual pair
type. The `VPair` value does not carry its type (values are untyped
in NbE), so the annotation cannot be reconstructed without additional
context. Quoted pairs are structurally correct but carry a dummy
annotation.
### 13.2 Lambda domain annotations discarded in checking mode
When checking `Lam(n, A, t)` against `VPi(n, dom, cl)`, the lambda's
domain annotation `A` is discarded and replaced by `dom` from the
Pi type. This is standard bidirectional type checking (Dunfield &
Krishnaswami 2021, §4): in checking mode, the expected type provides
the domain, not the term. The elaborated output uses `quote(d, dom)`,
making the original annotation unrecoverable.
### 13.3 Term constructors do not validate argument types
Term constructors (`mkVar`, `mkSucc`, etc.) accept arbitrary Nix
values without type validation. `mkVar "hello"` produces
`{ tag = "var"; idx = "hello"; }`, which crashes at eval time.
The trust boundary is the HOAS layer (`hoas.nix`), which is the
public API — direct term construction is internal to the kernel.
### 13.4 `tryEval` only catches `throw` and `assert false`
`builtins.tryEval` in the elaborator's `isConstantFamily` sentinel
detection only catches explicit `throw` and `assert false`. Nix
coercion errors (e.g., "cannot convert a function to JSON"),
missing attribute access, and type comparison errors are uncatchable.
The elaborator uses `builtins.typeOf` in error paths to avoid
triggering coercion errors.
### 13.5 HOAS sentinel comparison
The `isConstantFamily` sentinel test in the elaborator applies two
distinct sentinel values and compares the results to detect whether
a binding body is dependent. Both Pi and Sigma paths compare
**elaborated kernel terms** (`H.elab r1.value == H.elab r2.value`)
rather than raw HOAS trees. This avoids false negatives from Nix's
function identity comparison (`==` on lambdas). However, if `H.elab`
itself produces structurally different terms for semantically
equivalent types (e.g., through different elaboration paths), false
negatives remain possible. This is a safe failure mode — the kernel
still type-checks correctly, but elaboration may require explicit
`_kernel` annotations unnecessarily.
### 13.6 StrEq neutral canonicalization
When one argument to `vStrEq` is neutral and the other is a literal,
the neutral's spine is extended with `EStrEq(literal)`. When both
arguments are neutral, the **left** neutral's spine is extended with
`EStrEq(right)`. This means `StrEq(x, y)` and `StrEq(y, x)` (where
both are neutral) produce different normal forms: `VNe(x, [EStrEq(y)])`
vs `VNe(y, [EStrEq(x)])`. Therefore `conv` will report them as
**not** definitionally equal, even though `StrEq` is semantically
symmetric. This is a safe conservatism: the kernel may reject some
provable equalities but never accepts a false one.
### 13.7 Extract uses type value threading (not sentinels)
The `extract` function threads kernel type values (`tyVal`) through
recursive extraction, rather than using sentinel-based non-dependence
tests. For Pi extraction, the codomain type is computed per-invocation
via `instantiate(tyVal.closure, kernelArg)`, supporting both dependent
and non-dependent function extraction. For Sigma extraction (records),
the second component's type is computed via
`instantiate(tyVal.closure, val.fst)`. A `reifyType : Val → HoasTree`
fallback converts kernel type values back to HOAS when the HOAS body
cannot be applied (e.g., when the body accesses record fields from a
neutral). `reifyType` loses sugar (VSigma → `H.sigma`, not
`H.record`) so the HOAS body is preferred when available.
### 13.8 Spine comparison complexity
`convSp` uses `builtins.elemAt` in a fold to compare neutral spines.
In Nix, `builtins.elemAt` on lists is O(1) (Nix lists are internally
vectors/arrays), so the actual complexity is O(n), not O(n²). This
was incorrectly flagged in an earlier audit.
---
## References
1. Coquand, T. et al. (2009). *A simple type-theoretic language: Mini-TT.*
2. Dunfield, J. & Krishnaswami, N. (2021). *Bidirectional Typing.* ACM Computing Surveys.
3. Kovács, A. (2022). *Generalized Universe Hierarchies.* CSL 2022.
4. Abel, A. & Chapman, J. (2014). *Normalization by Evaluation in the Delay Monad.*
5. Girard, J.-Y. (1972). *Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur.* Thèse d'État, Université Paris 7.
6. Hurkens, A. J. C. (1995). *A Simplification of Girard's Paradox.* TLCA 1995.
7. de Bruijn, N. (1972). *Lambda Calculus Notation with Nameless Dummies.*
8. Martin-Löf, P. (1984). *Intuitionistic Type Theory.* Bibliopolis.
9. Felicissimo, T. (2023). *Generic Bidirectional Typing for Dependent Type Theories.*
## Core API
### Adapt
Handler context transformation. Contravariant on context, covariant on continuation.
## `adapt`
Transform a handler's state context.
```
adapt : { get : P -> S, set : P -> S -> P } -> Handler -> Handler
```
Wraps a handler that works with child state S so it works with
parent state P, using a get/set lens. Propagates both resume and abort.
```nix
counterHandler = { param, state }: { resume = null; state = state + param; };
adapted = adapt { get = s: s.counter; set = s: c: s // { counter = c; }; } counterHandler;
# adapted now works with { counter = 0; logs = []; } state
```
## `adaptHandlers`
Adapt an entire handler set (attrset of handlers) to a different state context.
Applies the same get/set lens to every handler in the set.
```nix
stateHandlers = {
get = { param, state }: { value = state; inherit state; };
put = { param, state }: { value = null; state = param; };
};
adapted = adaptHandlers { get = s: s.data; set = s: d: s // { data = d; }; } stateHandlers;
```
### Binds
Idiomatic Nix bind helpers
## `bindAttrs`
Like a bind-chain but operates over named attrset of required-effects.
```nix
bind.attrs { foo = 99; bar = pure 22; baz = asks (env: env.baz); }
```
Values that are non-effects become send params: `send "foo" 99`.
Pass the `optionalArg` sentinel to mark a key as optional: bindAttrs
probes via `has-handler` first and omits the key when no handler is
installed (so a Nix function's default value can take over).
Result has same attr-keys with corresponding effect result.
See also: `bind.comp`, `bind.fn` for which this is the foundation.
# NOTE: Ordering of chained effects.
Since an attrSet has no order, this function chains effects in
same order as `builtins.attrNames` (alphabetical). If you need
an special order for computations that might be order senstive,
specify a `__sort = names => names` function.
## `bindComp`
Turns a Nix effectful function into an effect chain via bindAttrs.
```nix
bindComp { bar = pure 22; } ({ foo, bar }: pure (foo * bar))
```
The function sees bar as the result of `pure 22` and `foo` as the
result of `send "foo" false` -- false comes directly from using
`lib.functionArgs f`, the handler can know if "foo" is optional in f.
Optional args (those with defaults in the Nix function) are probed
via has-handler before sending. If no handler exists, the arg is
skipped and the Nix default kicks in.
This works by using `bindAttrs` on the intersection of function args
and attrs.
## `bindFn`
Like bindComp but works on normal Nix functions and turns
its result into a pure-effect.
```nix
bindFn { bar = pure 22; } ({ foo, bar }: foo * bar)
```
### Build
## `materialize`
Materialize a validated BuildPlan into a derivation.
Converts the eval-time plan (validated by fx.build.plan) into a
pkgs.runCommand derivation. Sources are copied into a working
directory, per-step environment variables are scoped, and steps
execute sequentially under set -euo pipefail.
```
materialize : { pkgs, plan, native? } -> derivation
```
The plan argument is the `.plan` field from fx.build.plan output.
Shell generation helpers (mkStepScript, mkSourceSetup, mkBuildScript)
are pure functions tested inline.
## `plan`
Validate and process build steps into a BuildPlan.
Runs an eval-time pipeline that validates each step against
BuildStep, filters steps by `when` predicates using reader context,
and collects all errors without throwing.
```
plan : { name, steps, sources?, context? } -> { plan, errors, warnings, typeErrors }
```
## `types`
Build types for effects-powered builders.
BuildStep and BuildPlan describe build pipelines at the type level,
enabling validation before materialization into derivations.
### Comp
Computation ADT: introduction and elimination forms for Pure | Impure.
## `impure`
Create a suspended computation (OpCall constructor). Takes an effect and a continuation queue.
## `isComp`
Test whether a value is a computation.
## `isPure`
Test whether a computation is Pure. For hot-path conditionals where match would allocate.
## `match`
Eliminate a computation by cases.
```
match comp { pure = a: ...; impure = effect: queue: ...; }
```
Every function that consumes a Computation should go through
match or isPure — never inspect _tag directly.
## `pure`
Lift a value into a pure computation (Return constructor).
### Diag
The `diag` namespace provides typed diagnostic Errors and
structured Hints for the type-checker and runtime contracts.
## error
Diagnostic Error ADT.
An Error has a Layer (Kernel | Generic), a Detail record whose fields
are all optional, a short msg, an optional hint, and a list of
children. A leaf has `children = []`; a branch has a non-empty
children list whose entries are `{ position, error }` pairs. Sibling
failures produce many children; a chained descent produces one
child; a leaf has none.
Constructors:
mkKernelError { position?, rule, msg, expected?, got?, ctx_depth?, hint? }
mkGenericError { type?, context?, value, desc?, index?, guard?, msg, hint? }
Combinators:
nestUnder : Position -> Error -> Error
addChild : Position -> Error -> Error -> Error
Layer constants: Kernel, Generic. Predicates: isError, isLayer.
Equality: eq (structural).
Pure data. No dependencies on kernel, trampoline, effects, tc, or
types modules.
## positions
Shared diagnostic alphabet. Pure data.
A Position names the blame location in a structural descent through
a Desc or through raw MLTT structure (Π / Σ / Ann / μ / App). The
alphabet is description-centric: names such as `DArgSort`, `DPlusL`,
and `PiDom` identify sub-positions by their meaning in the structure,
not by the code path that happens to visit them.
Two kinds of consumer:
- A kernel enrichment layer that wraps rule delegations, emitting
a child error tagged with the `Position` of the sub-call that
failed.
- A value-level validator (record / list / variant field walkers)
that emits `Field` / `Elem` / `Tag` positions from its per-
component blame traversal.
Both consumers produce `Error` trees whose children are keyed by
`Position`, allowing errors from either source to compose into one
tree.
## pretty
Pretty-printing for diagnostic Errors.
Exports:
pathSegments : Error -> [String]
pathString : Error -> String
oneLine : Error -> String
multiLine : Error -> String
Chain walkers recurse directly up to 500
frames, then fall through to a `builtins.genericClosure` slow
path that WHNF-forces the next node at each step.
Pure data -> string; no effects.
## hints
Hint resolver for diagnostic Errors.
Exports:
resolve : Error -> Hint | null
classify : Error -> String
hints : { = Hint; }
A Hint is `{ _tag = "Hint"; text; category; severity; docLink; }`.
The `_tag` marker keeps it terminal for `api.extractValue`, and
the remaining fields are plain data consumable by renderers,
LSPs, docs, and linters. Severity is `"error"` at this layer;
`docLink` points at the per-key heading anchor on the
auto-generated diag module page (`/nix-effects/core-api/diag`).
The anchor slug matches the docs-site markdown renderer's
heading-id slugification rule, so each hint's docLink lands
precisely on the rendered section for its key.
Keys encode a leaf-anchored suffix of the blame path plus the
classifier pattern: `"....::"`. A key
matches when its positions equal the last N tags of the blame
path; `resolve` returns the hint under the longest matching
suffix. Single-position keys are the 1-hop special case. Hint
text is position-semantic: no kernel-rule strings, no source-file
references.
Chain walking recurses directly up to 500
frames, then falls through to a `builtins.genericClosure` slow
path that WHNF-forces the next node.
## Hint registry
The Hint table maps each *blame-path-suffix · classifier-pattern*
key to a structured Hint record. Each subsection below
corresponds to one such key; the heading anchor is the canonical
`docLink` target referenced from `hints.nix`.
### AnnTerm::type-mismatch
Category: **type-mismatch** · Severity: **error**
the annotated term does not match its declared type
### AnnType::not-a-type
Category: **sort** · Severity: **error**
the annotation position must be a type (live in some U(k)), not a term. Write a type expression such as `nat`, `bool`, `u 0`, or a user-defined datatype.
### AppArg::type-mismatch
Category: **type-mismatch** · Severity: **error**
the argument does not match the function's domain
### AppHead::not-a-function
Category: **arity** · Severity: **error**
the head of an application must have a function type (Pi)
### Case::type-mismatch
Category: **elimination** · Severity: **error**
this case-body's inferred type does not match the type the eliminator's motive requires
### DArgBody::not-a-desc
Category: **description** · Severity: **error**
the body of `arg` must produce a description (Desc I), not an ordinary value. Build one with `descRet`, `descArg`, `descRec`, `descPi`, or `descPlus`.
### DArgSort::universe-mismatch
Category: **universe** · Severity: **error**
the sort position of `arg` must live in U(0); descriptions only carry small types. Pass `u 0`, or factor the dependency through `descRec` / `descPi` if a larger type is genuinely needed.
### DPiBody::not-a-desc
Category: **description** · Severity: **error**
the body of `pi` must produce a description for each input, not a plain term. Return a Desc I via `descRet`, `descArg`, `descRec`, `descPi`, or `descPlus`.
### DPiFn::not-a-function
Category: **arity** · Severity: **error**
the index selector `f` of `pi` must be a function `S -> I`
### DPiFn::type-mismatch
Category: **indexing** · Severity: **error**
the index selector's domain must match the declared sort `S`
### DPiSort::universe-mismatch
Category: **universe** · Severity: **error**
the sort position of `pi` must live in U(0); `descPi` takes a small domain. Use `u 0`, or encode the dependency through an index instead of the Pi domain.
### DPlusL::not-a-desc
Category: **description** · Severity: **error**
the left summand of `plus` must be a description (Desc I)
### DPlusR::not-a-desc
Category: **description** · Severity: **error**
the right summand of `plus` must be a description at the same index type as the left summand
### DRecIndex::type-mismatch
Category: **indexing** · Severity: **error**
the index position of `rec` must match the Desc's declared index type. Pass a term of that index type, or adjust the enclosing `μ I ...` to match.
### DRecTail::not-a-desc
Category: **description** · Severity: **error**
the tail position of `rec` must itself be a description, not an ordinary term. Continue the spine with `descRet`, `descArg`, `descRec`, `descPi`, or `descPlus`.
### DRetIndex::type-mismatch
Category: **indexing** · Severity: **error**
the index position of `ret` must match the Desc's declared index type. Supply a term of that index type, or redefine the enclosing `μ I ...` over the index you actually have.
### Elem::inhabitation-failed
Category: **inhabitation** · Severity: **error**
the element does not inhabit the list's element type
### Elem::refinement-failed
Category: **refinement** · Severity: **error**
the element violates the element type's refinement predicate
### Field::inhabitation-failed
Category: **inhabitation** · Severity: **error**
the field's value does not inhabit the declared field type
### Field::refinement-failed
Category: **refinement** · Severity: **error**
the field's value violates the field type's refinement predicate
### JType::not-a-type
Category: **sort** · Severity: **error**
the type parameter of `J` must be a type (live in some U(k)), not a term. Pass a type expression like `nat`, `u 0`, or the type shared by J's two endpoints.
### JType::type-mismatch
Category: **type-mismatch** · Severity: **error**
the type parameter of `J` must match the type of its two endpoints
### LevelMaxLhs::type-mismatch
Category: **universe** · Severity: **error**
the left operand of `max` must be a Level
### LevelMaxRhs::type-mismatch
Category: **universe** · Severity: **error**
the right operand of `max` must be a Level
### LevelSucPred::type-mismatch
Category: **universe** · Severity: **error**
the predecessor of `suc` must be a Level
### Motive.PiDom::not-a-type
Category: **sort** · Severity: **error**
the motive's domain must be a type (live in some U(k)). The motive receives the scrutinee's type as its domain and returns a type; supply a concrete type such as `nat`, `u 0`, or the datatype being eliminated.
### Motive::not-a-function
Category: **arity** · Severity: **error**
the motive must be a function from the scrutinee's type into a type, not a bare type or value. Supply a one-argument function whose body lives in some `U k`.
### Motive::not-a-type
Category: **sort** · Severity: **error**
an eliminator's motive must return a type (live in some U(k))
### MuDesc::not-a-desc
Category: **description** · Severity: **error**
the description argument of μ must be a Desc I term, not an ordinary value. Construct it with `descRet`, `descArg`, `descRec`, `descPi`, or `descPlus`.
### MuIndex::type-mismatch
Category: **indexing** · Severity: **error**
the index passed to `con` must have the description's index type
### MuPayload::type-mismatch
Category: **indexing** · Severity: **error**
the payload of `con` must inhabit the description's interpretation at the given index
### OpaqueType::not-a-function
Category: **arity** · Severity: **error**
the annotation on an opaque lambda must be a Pi type
### OpaqueType::type-mismatch
Category: **type-mismatch** · Severity: **error**
the opaque lambda's declared domain does not match the expected domain
### PiCod::not-a-type
Category: **sort** · Severity: **error**
the codomain family of Π must return a type for each argument, not an ordinary value. Provide a function whose body inhabits some `U k`.
### PiDom::not-a-type
Category: **sort** · Severity: **error**
the domain of Π must be a type (live in some U(k)), not a term or value. Supply a type expression like `nat`, `bool`, `u 0`, or a user-defined datatype.
### Scrut::type-mismatch
Category: **elimination** · Severity: **error**
the scrutinee's type must match the eliminator's expected shape. Annotate the scrutinee via `ann`, or switch to the eliminator that matches its inferred type.
### SigmaFst::inhabitation-failed
Category: **inhabitation** · Severity: **error**
the first component does not inhabit the declared `fst` type
### SigmaFst::refinement-failed
Category: **refinement** · Severity: **error**
the first component violates the `fst` type's refinement predicate
### SigmaSnd::inhabitation-failed
Category: **inhabitation** · Severity: **error**
the second component does not inhabit the dependent `snd` type
### SigmaSnd::refinement-failed
Category: **refinement** · Severity: **error**
the second component violates the `snd` type's refinement predicate
### Tag::inhabitation-failed
Category: **inhabitation** · Severity: **error**
the variant's payload does not inhabit the branch type
### Tag::refinement-failed
Category: **refinement** · Severity: **error**
the variant's payload violates the branch type's refinement predicate
### ULevel::type-mismatch
Category: **universe** · Severity: **error**
the level argument of `U` must be a Level
### Kernel
Freer monad kernel: Return/OpCall ADT with FTCQueue bind, send, map, seq, pipe, kleisli.
## `bind`
Monadic bind: sequence two computations.
```
bind comp f = case comp of
Pure a -> f a
Impure e q -> Impure e (snoc q f)
```
O(1) per bind via FTCQueue snoc (Kiselyov & Ishii 2015, Section 3.1).
## `kleisli`
Kleisli composition: compose two Kleisli arrows (a -> M b) and (b -> M c) into (a -> M c).
## `map`
Map a function over the result of a computation (Functor instance).
## `pipe`
Chain a computation through a list of Kleisli arrows, threading results via bind.
## `send`
Send an effect request. Returns the handler's response via continuation.
## `seq`
Sequence a list of computations, threading state via bind. Returns the last result.
### Pipeline
Typed pipeline framework with composable stages.
Stages are composable transformations executed with reader (immutable
environment), error (collecting validation errors), and acc (non-fatal
warnings) effects. The run function wires up all handlers and returns
{ value, errors, warnings, typeErrors }.
```nix
let
stage1 = pipeline.mkStage {
name = "discover";
transform = data:
bind (pipeline.asks (env: env.config)) (cfg:
pure (data // { config = cfg; }));
};
result = pipeline.run { config = "prod"; } [ stage1 ];
in result # => { config = "prod"; }
```
## `compose`
Chain stages into a single computation.
```
compose : [Stage] -> Data -> Computation Data
```
Each stage's transform receives the output of the previous stage
and returns a computation producing the next stage's input.
Initial data seeds the pipeline.
## `mkStage`
Create a named pipeline stage.
```
mkStage : { name, description?, transform, inputType?, outputType? } -> Stage
```
transform : Data -> Computation Data
Takes current pipeline data, uses effects (ask, raise, warn),
returns computation producing updated pipeline data.
inputType/outputType : optional type schemas for validation
at stage boundaries (checked when provided).
Validation uses fx.types.validate which sends typeCheck effects.
## `run`
Execute a pipeline with effect handling.
```
run : args -> [Stage] -> { value, errors, warnings, typeErrors }
```
args : { ... }
Becomes the reader environment -- stages access via ask/asks.
stages : [Stage]
Ordered list of stages to execute.
Returns:
value -- final pipeline data from last stage
errors -- list of { message, context } from validation failures
warnings -- list of non-fatal warning items
typeErrors -- list of type validation errors
### Queue
FTCQueue (catenable queue, after Kiselyov & Ishii 2015). O(1) snoc/append, amortized O(1) viewl.
## `append`
Concatenate two queues. O(1).
## `leaf`
Create a singleton queue containing one continuation function.
## `node`
Join two queues. O(1) — just creates a tree node.
## `qApp`
Apply a queue of continuations to a value. Processes continuations
left-to-right: if a continuation returns Pure, feed the value to the
next continuation. If it returns Impure, append the remaining queue
to the effect's own queue and return.
## `singleton`
Create a queue with a single continuation. O(1).
## `snoc`
Append a continuation to the right of the queue. O(1).
## `viewl`
Extract the leftmost continuation from the queue. Amortized O(1).
```
Returns { head = fn; tail = queue | null; }
```
`tail` is null if the queue had only one element.
### Sugar
Opt-in syntax-livability layer for nix-effects.
- `fx.sugar.do` / `fx.sugar.letM` — combinator forms
- `fx.sugar.operators.__div` — `/` as reverse-apply (bind)
- re-exports of `pure bind run handle map seq pipe kleisli`
See `book/src/sugar.md` for the opt-in matrix and caveats.
### Trampoline
Trampolined interpreter using builtins.genericClosure for O(1) stack depth.
## `handle`
Trampolined handler combinator with return clause.
```
handle : { return?, handlers, state? } -> Computation a -> { value, state }
```
Follows Kiselyov & Ishii's `handle_relay` pattern but trampolined
via genericClosure for O(1) stack depth.
**Arguments** (attrset):
- `return` — `value -> state -> { value, state }`. How to transform the final Pure value. Default: identity.
- `handlers` — `{ effectName = { param, state }: { resume | abort, state }; }`. Each must return `{ resume; state; }` or `{ abort; state; }`.
- `state` — initial handler state. Default: null.
## `rotate`
Selectively handle known effects and rotate unknown effects outward.
```
rotate : { return?, handlers, state? } -> Computation a -> Computation b
```
If the current effect has a matching handler, the handler is applied.
If it does not match, the effect is re-suspended and its continuation
is wrapped so handling resumes after that effect is interpreted by an
outer handler.
This corresponds to the Kyo-style handler rotation law
from https://gist.github.com/vic/3a7f52974a28675dbaf40b34bec74787:
```
handle(tag1, suspend(tag2, i, k), f) = suspend(tag2, i, x => handle(tag1, k(x), f))` for `tag1 != tag2
```
## `run`
Run a computation through the genericClosure trampoline.
```
run : Computation a -> Handlers -> State -> { value : a, state : State }
```
**Arguments:**
- `comp` — the freer monad computation to interpret
- `handlers` — `{ effectName = { param, state }: { resume | abort, state }; ... }`
- `initialState` — starting state passed to handlers
Handlers must return one of:
```
{ resume = value; state = newState; } -- invoke continuation with value
{ abort = value; state = newState; } -- discard continuation, halt
```
This is the defunctionalized encoding of Plotkin & Pretnar (2009):
`resume` ≡ invoke continuation k(v), `abort` ≡ discard k.
Stack depth: O(1) — constant regardless of computation length.
Time: O(n) where n = number of effects in the computation.
## Effects
### Acc
Accumulator effect: emit/emitAll/collect for incremental list building.
## `collect`
Read the current accumulated items.
```
collect : Computation [a]
```
## `emit`
Append a single item to the accumulator.
```
emit : a -> Computation null
```
## `emitAll`
Append a list of items to the accumulator.
```
emitAll : [a] -> Computation null
```
## `handler`
Standard accumulator handler. State is a list of accumulated items.
Initial state: `[]`
```nix
handle { handlers = acc.handler; state = []; } comp
```
### Choice
Non-deterministic choice effect: choose/fail/guard with list handler.
## `choose`
Non-deterministic choice from a list of alternatives.
The handler determines how alternatives are explored.
```
choose : [a] -> Computation a
```
## `fail`
Fail the current branch of non-deterministic computation.
Equivalent to `choose []`.
```
fail : Computation a
```
## `guard`
Guard a condition: continue if true, fail if false.
```
guard : bool -> Computation null
```
## `initialState`
Initial state for the listAll handler.
## `listAll`
Handler that explores all non-deterministic branches and returns
a list of all results. Empty choices abort that branch.
State is `{ results : [a], pending : [Computation a] }`.
After handling, results are in `state.results`.
```nix
let r = handle { handlers = choice.listAll; state = choice.initialState; } comp;
in r.state.results
```
### Conditions
CL-style condition system: signal/warn with restart-based recovery.
## `collectConditions`
Collecting handler: accumulates conditions in state, resumes with continue.
State shape: list of { name, data }
Initial state: []
## `fail`
Fail handler: throws on any condition. Ignores available restarts.
Use as a last-resort handler.
## `ignore`
Ignore handler: resumes with null for any condition.
All conditions are silently discarded.
## `signal`
Signal a condition. The handler chooses a restart strategy.
```
signal : string -> any -> [string] -> Computation any
```
**Arguments:**
- `name` — condition name (e.g. `"division-by-zero"`, `"file-not-found"`)
- `data` — condition data (error details, context)
- `restarts` — list of available restart names
The handler receives `{ name, data, restarts }` and returns a
`{ restart, value }` attrset. The continuation receives this choice.
## `warn`
Signal a warning condition. Like signal but with a conventional
`"muffle-warning"` restart. If the handler doesn't muffle, the
computation continues normally.
```
warn : string -> any -> Computation null
```
## `withRestart`
Create a handler that invokes a specific restart for a named condition.
For all other conditions, falls through (throws).
```
withRestart : string -> string -> any -> handler
```
**Arguments:**
- `condName` — condition name to match
- `restartName` — restart to invoke
- `restartVal` — value to pass via the restart
### Error
Error effect with contextual messages and multiple handler strategies.
## `collecting`
Collecting error handler: accumulates errors in state as a list.
Resumes computation with null so subsequent effects still execute.
Use when you want all errors, not just the first.
State shape: list of { message, context }
## `raise`
Raise an error. Returns a Computation that sends an "error" effect.
The handler determines what happens: throw, collect, or recover.
```
raise : string -> Computation a
```
## `raiseWith`
Raise an error with context. The context string describes where
in the computation the error occurred, enabling stack-trace-like
error reports when used with the collecting handler.
```
raiseWith : string -> string -> Computation a
```
## `result`
Result error handler: aborts computation with tagged Error value.
Uses the non-resumption protocol to discard the continuation.
Returns `{ _tag = "Error"; message; context; }` on error.
## `strict`
Strict error handler: throws on first error via builtins.throw.
Use when errors should halt evaluation immediately.
Includes context in the thrown message when available.
### HasHandler
Check if a handler with given name exists in current scope.
```
hasHandler : String -> Computation Bool
```
### Linear
Graded linear resource tracking: acquire/consume/release with usage enforcement.
Each resource gets a capability token at acquire time. The graded handler
covers linear (exactly once), affine (at most once via release), exact(n),
and unlimited usage through a single maxUses parameter.
Quick start:
```nix
let comp = bind (linear.acquireLinear "secret") (token:
bind (linear.consume token) (val:
pure val));
in linear.run comp
```
For composition with other handlers, use handler/return/initialState with
`adaptHandlers`.
## `acquire`
Acquire a graded linear resource. Returns a capability token.
```
acquire : { resource : a, maxUses : Int | null } -> Computation Token
```
The token wraps the resource with an ID for tracking. The handler
maintains a resource map in its state, counting each consume call
against the maxUses bound.
- `maxUses = 1` — Linear: exactly one consume required
- `maxUses = n` — Exact: exactly n consumes required
- `maxUses = null` — Unlimited: any number of consumes allowed
Tokens should be consumed exactly maxUses times, or explicitly
released. At handler exit, the return clause (finalizer) checks:
released → always OK, `maxUses = null` → always OK,
otherwise → `currentUses` must equal `maxUses`.
## `acquireExact`
Acquire a resource that must be consumed exactly n times.
```
acquireExact : a -> Int -> Computation Token
```
## `acquireLinear`
Acquire a linear resource (exactly one consume required).
```
acquireLinear : a -> Computation Token
```
## `acquireUnlimited`
Acquire an unlimited resource (any number of consumes allowed).
```
acquireUnlimited : a -> Computation Token
```
## `consume`
Consume a capability token, returning the wrapped resource value.
```
consume : Token -> Computation a
```
Increments the token's usage counter. Aborts with `LinearityError` if:
- Token was already released (`"consume-after-release"`)
- Usage would exceed maxUses bound (`"exceeded-bound"`)
The returned value is the original resource passed to acquire.
## `handler`
Graded linear resource handler. Interprets linearAcquire, linearConsume,
and linearRelease effects. Tracks resource usage in handler state.
Use with `trampoline.handle`:
```nix
handle {
handlers = linear.handler;
return = linear.return;
state = linear.initialState;
} comp
```
Or use the convenience: `linear.run comp`
- `linearAcquire`: creates token, adds resource entry to state
- `linearConsume`: increments usage counter, returns resource value
- `linearRelease`: marks resource as released (finalizer skips it)
## `initialState`
Initial handler state for the linear resource handler.
```nix
{ nextId = 0; resources = {}; }
```
- `nextId`: monotonic counter for generating unique resource IDs.
- `resources`: map from ID (string) to resource tracking entry.
## `release`
Explicitly release a capability token without consuming it.
```
release : Token -> Computation null
```
Marks the resource as released. The finalizer skips released resources,
so this allows affine usage (acquire then drop). Aborts with
`LinearityError` on double-release.
## `return`
Finalizer return clause for the linear handler.
Checks each resource in handler state:
- `released` → OK (explicitly dropped)
- `maxUses = null` → OK (unlimited)
- otherwise → `currentUses` must equal `maxUses`
On violation, wraps the original value in a `LinearityError` with
details of each mismatched resource. On success, passes through
unchanged. Runs on both normal return and abort paths.
## `run`
Run a computation with the graded linear handler.
```
run : Computation a -> { value : a | LinearityError, state : State }
```
Bundles handler, return clause, and initial state into one call.
To compose with other handlers, use handler/return/initialState
separately with `adaptHandlers`.
```nix
let
comp = bind (acquireLinear "secret") (token:
bind (consume token) (val:
pure "got:${val}"));
in linear.run comp
# => { value = "got:secret"; state = { nextId = 1; resources = { ... }; }; }
```
### Reader
Read-only environment effect: ask/asks/local with standard handler.
## `ask`
Read the current environment.
```
ask : Computation env
```
## `asks`
Read a projection of the environment.
```
asks : (env -> a) -> Computation a
```
## `handler`
Standard reader handler. Interprets ask effects.
The state IS the environment (immutable through the computation).
```nix
handle { handlers = reader.handler; state = myEnv; } comp
```
## `local`
Run a computation with a modified environment.
Returns a new computation that transforms the environment
before executing the inner computation.
Since handlers are pure functions, local is implemented by
wrapping the inner computation's ask effects with the modifier.
In practice, use separate handler installation with the modified env.
```
local : (env -> env) -> Computation a -> Computation a
```
### Scope
Computation-scoped handlers via effect rotation.
## `handlersFromAttrs`
Helper to transform an attrset into named handlers.
If attrValue is a function `{ param, state }` it is used directly as handler;
If attrValue is a function, resume is `f param` and preserves state;
Otherwise a constant handler always resumes with attrValue, preserving state.
## `provide`
Install handlers for a computation's dynamic extent without
touching state. Unhandled effects rotate outward; outer handler
state mutations survive unaffected.
This is the reader/val handler pattern (Koka's `val`, Haskell's
`runReader`, Scheme's `parameterize`) — use it when handlers are
stateless (resume with a constant, pass state through).
For handlers that need their own state, use scope.run or
scope.stateful instead.
```
scope.provide : handlers -> Computation a -> Computation a
```
## `run`
Run a computation with scoped handlers. Effects matching `handlers`
are handled inside the scope. Unknown effects rotate outward.
The scope's internal state is hidden — caller sees only the body's value.
```
scope.run : { handlers, state? } -> Computation a -> Computation a
```
## `runWith`
Like scope.run but exposes the scope's final state alongside the value.
```
scope.runWith : { handlers, state? } -> Computation a -> Computation { value, state }
```
## `stateful`
Run a computation with scoped handlers while preserving
state around effect rotation.
```
scope : handlers -> Computation a -> Computation a
```
## `val`
Provide constant values as named effect handlers for a
computation's dynamic extent. Each key in the bindings attrset
becomes an effect that resumes with the corresponding value.
Built on scope.provide via handlersFromAttrs.
Named after Koka's `val` effect handler. For the traditional
single-environment reader (ask/asks/local), see fx.effects.reader.
```
scope.val : AttrSet -> Computation a -> Computation a
```
### State
Mutable state effect: get/put/modify with standard handler.
## `get`
Read the current state. Returns a Computation that, when handled,
yields the current state value.
```
get : Computation s
```
## `gets`
Read a projection of the current state.
```
gets : (s -> a) -> Computation a
```
## `handler`
Standard state handler. Interprets get/put/modify effects.
Use with `trampoline.handle`:
```nix
handle { handlers = state.handler; state = initialState; } comp
```
- `get`: returns current state as value
- `put`: replaces state with param, returns null
- `modify`: applies param (a function) to state, returns null
## `modify`
Apply a function to the current state. Returns a Computation that,
when handled, transforms the state via f and returns null.
```
modify : (s -> s) -> Computation null
```
## `put`
Replace the current state. Returns a Computation that, when handled,
sets the state to the given value and returns null.
```
put : s -> Computation null
```
## `update`
Apply a computation to the current state. Returns a Computation that,
when handled, updates the state and returns value.
```
update : (s -> Computation { state, value }) -> Computation value
```
### Typecheck
Reusable typeCheck handlers: strict (throw), collecting (accumulate), logging (record all).
## `collecting`
Collecting typeCheck handler: accumulates errors in state.
Resumes with `true` on success, `false` on failure (computation continues).
State shape: list of `{ context, typeName, actual, message, path }`
Initial state: `[]`
## `logging`
Logging typeCheck handler: records every check (pass or fail) in state.
Always resumes with the actual check result (boolean).
State shape: list of `{ context, typeName, passed, path }`
Initial state: `[]`
## `strict`
Strict typeCheck handler: throws on first type error.
Resumes with true on success (check passed).
Use when type errors should halt evaluation immediately.
State: unused (pass null).
### Writer
Append-only output effect: tell/tellAll with list-collecting handler.
## `handler`
Standard writer handler. Collects tell output in state as a list.
Initial state: `[]`
```nix
handle { handlers = writer.handler; state = []; } comp
```
## `tell`
Append a value to the output log.
```
tell : w -> Computation null
```
## `tellAll`
Append a list of values to the output log.
```
tellAll : [w] -> Computation null
```
## Types
### Constructors
Type constructors: Record, ListOf, Maybe, Either, Variant.
## `Either`
Tagged union of two types. Accepts `{ _tag = "Left"; value = a; }`
or `{ _tag = "Right"; value = b; }`.
## `ListOf`
Homogeneous list type. `ListOf Type` checks that all elements have the given type.
Custom verifier sends per-element `typeCheck` effects with indexed context
strings (e.g. `List[Int][2]`) for blame tracking. Unlike Sigma, elements
are independent — no short-circuit. All elements are checked; the handler
decides error policy (strict aborts on first, collecting gathers all).
## `Maybe`
Option type. Maybe Type accepts null or a value of Type.
## `Record`
Record type constructor. Takes a schema { field = Type; ... } and checks
that a value has all required fields with correct types.
Extra fields are permitted (open record semantics).
## `Variant`
Discriminated union. Takes `{ tag = Type; ... }` schema.
Accepts `{ _tag = "tag"; value = ...; }` where value has the corresponding type.
### Dependent
Dependent contracts: Pi (Π), Sigma (Σ), Certified, Vector, DepRecord.
Grounded in Martin-Löf (1984) "Intuitionistic Type Theory".
## `Certified`
Certified value: `Σ(v:A).Proof(P(v))`.
A dependent pair where:
```
fst : A — the value
snd : true — proof witness (must be true AND predicate must hold)
```
The second component's type depends on the first: it checks both
that the proof is `true` and that `predicate(fst)` holds.
Certified is a first-order contract — both components are concrete
data, so the contract is checked immediately and completely (like
Sigma). The guard IS full membership.
Construction:
- `.certify v` — pure smart constructor (throws on invalid)
- `.certifyE v` — effectful smart constructor (sends `typeCheck` effects)
- `.check` — inherited from Sigma (full dependent pair check)
- `.validate` — inherited from Sigma (effectful introduction check)
The `.certifyE` constructor is NOT an introduction check — it's a
convenience that takes a raw value, evaluates the predicate, and
produces the Sigma pair `{ fst = v; snd = true; }`. The actual
introduction check (`.validate`) is inherited from Sigma and verifies
an already-formed pair.
## `DepRecord`
Dependent record type built on nested Sigma.
Schema is an ordered list of `{ name; type; }` where `type` can be:
- A Type (static field)
- A function (`partial-record → Type`) for dependent fields
Isomorphic to nested Sigma types:
```
{ a : A, b : B(a) } ≅ Σ(a:A).B(a)
{ a : A, b : B(a), c : C(a,b) } ≅ Σ(a:A).Σ(b:B(a)).C(a,b)
```
Values are nested Sigma pairs:
```nix
{ fst = a; snd = { fst = b; snd = c; }; }
```
Inherits from Sigma: `.validate` (effectful), `.proj1`, `.proj2`,
`.pair`, `.pairE`, `.curry`, `.uncurry`.
Use `.pack` to convert flat attrset → nested Sigma value.
Use `.unpack` to convert nested Sigma value → flat attrset.
## `Pi`
Dependent function type `Π(x:A).B(x)`.
Arguments:
- `domain` — Type A
- `codomain` — A-value → Type (type family B indexed by domain values)
- `universe` — Universe level (explicit parameter — see below)
- `name` — optional display name
== Higher-order contract with algebraic effects ==
Pi is a HIGHER-ORDER CONTRACT (Findler & Felleisen 2002). Higher-order
contracts check function values differently from data values: a data
contract is verified immediately and completely, but a function contract
is verified incrementally at each application site. This is the
standard, correct strategy for function contracts — not a deficit.
The (Specification, Guard, Verifier) triple for Pi:
```
Guard (check): builtins.isFunction — the immediate first-order
part of the contract. Soundly rejects non-functions.
Verifier (validate): effectful guard (auto-derived, 1 arg) — wraps
the guard in a typeCheck effect for blame tracking.
Elimination (checkAt): deferred contract check (2 args) — verifies a
specific application f(arg) by sending typeCheck
effects for both domain (arg : A) and codomain
(f(arg) : B(arg)).
```
This is precisely the Findler-Felleisen decomposition: the immediate
part (`isFunction`) is checked at introduction; the deferred part
(domain + codomain) is checked at each elimination site via `checkAt`.
== Adequacy ==
```
check f ⟺ all typeCheck effects in (validate f) pass
```
Both `check` and `validate` verify the introduction form (is it a function?).
`checkAt` verifies individual applications — the deferred contract.
== Universe level ==
Universe level is an explicit parameter. In MLTT, the level is computed
as `max(i, sup_{a:A} level(B(a)))` by inspecting the syntax of B.
For types with explicit kernelType, the kernel computes and verifies
levels via checkTypeLevel. The explicit universe parameter provides
the level for the surface API's `.universe` field.
== MLTT rule mapping ==
```
Formation: Pi { domain, codomain, universe }
Introduction check: .check (guard: isFunction)
Introduction verify: .validate (effectful guard, auto-derived)
Elimination: .apply (pure), .checkAt (effectful, deferred contract)
Computation: β-reduction (Nix evaluation)
```
Operations:
- `.checkAt f arg` — deferred contract check at elimination site
- `.apply arg` — pure elimination: compute codomain type B(arg)
- `.compose f other` — compose Pi types (requires witness function)
- `.domain` — the domain type A
- `.codomain` — the type family B
## `Sigma`
Dependent pair type `Σ(x:A).B(x)`.
Arguments:
- `fst` — Type A (type of the first component)
- `snd` — A-value → Type (type family for the second component)
- `universe` — Universe level (explicit parameter)
- `name` — optional display name
Values are `{ fst; snd; }` where `fst : A` and `snd : B(fst)`.
== First-order contract — guard is exact ==
Sigma is a FIRST-ORDER CONTRACT: both components are concrete data,
so the contract is checked immediately and completely. The guard
(`check`) IS full membership — there is no over-approximation.
```
Guard (check): fst:A ∧ snd:B(fst) — exact. G = ⟦Σ(x:A).B(x)⟧.
Verifier (verify): decomposed effectful check — sends separate
typeCheck effects for fst and snd for blame tracking.
```
This contrasts with Pi where the guard over-approximates (`isFunction`)
because functions are higher-order. Sigma pairs are data — the
dependent relationship (snd's type depends on fst's value) can be
fully verified because both values are available.
Adequacy:
```
T.check v ⟺ all typeCheck effects in T.validate v pass
```
Under the all-pass handler. The guard is exact and the decomposed
verifier sends individual `typeCheck` effects per component — the all-pass
handler's boolean state tracks whether all passed. Totality: if the input
is structurally malformed (not an attrset, missing `fst`/`snd`), verify falls
back to a single `typeCheck` for the whole type — failure goes through the
effect system, never crashes Nix.
Universe level is an explicit parameter (computing
`sup_{a:A} snd(a).universe` requires evaluating the type family on
all domain values, same as Pi).
== MLTT rule mapping ==
```
Formation: Sigma { fst, snd, universe }
Introduction: .check (exact guard), .validate (effectful, decomposed)
Elimination: .proj1 (π₁), .proj2 (π₂)
Computation: π₁(a,b) ≡ a, π₂(a,b) ≡ b
```
Operations:
- `.proj1 pair` — first projection π₁
- `.proj2 pair` — second projection π₂
- `.pair a b` — smart constructor (throws on invalid)
- `.validate v` — effectful: decomposed typeCheck effects for blame
- `.pairE a b` — effectful smart constructor
- `.pullback f g` — contravariant predicate pullback (see below)
- `.curry` / `.uncurry` — standard Sigma adjunction
- `.fstType` — the type A
- `.sndFamily` — the type family B
## `Vector`
Length-indexed list type family, built on Pi.
```
Vector(A) = Π(n:Nat).{xs : List(A) | |xs| = n}
```
This is the correct Martin-Löf encoding: Vector IS a Pi type.
It inherits `.validate` (effectful), `.compose`, `.apply`, `.domain`, `.codomain`
from Pi.
Usage:
```nix
Vector elemType # the Pi type family (Nat → SizedList)
(Vector elemType).apply 3 # specific type for length 3
```
### Foundation
Type system foundation: Type constructor, check, validate, make, refine.
## `check`
Check whether a value inhabits a type. Returns bool.
## `make`
Validate a value and return it, or throw on failure.
## `mkType`
Create a type from its kernel representation.
A nix-effects type is defined by its `kernelType` — an HOAS type tree
representing the type in the MLTT kernel. All fields are derived:
- `.check` = `decide(kernelType, v)` — the decision procedure
- `.universe` = `checkTypeLevel(kernelType)` — computed universe level
- `.kernelCheck` = same as `.check`
- `.prove` = kernel proof checking for HOAS terms
Arguments:
- `name` — Human-readable type name
- `kernelType` — HOAS type tree (required — this IS the type)
- `guard` — Optional runtime predicate for refinement types.
When present, `.check = kernelDecide(v) && guard(v)` (conjunction —
kernel catches structural errors, guard handles residual constraints).
The guard handles constraints the kernel can't express (e.g., x >= 0).
- `verify` — Optional custom verifier (`self → path → value → Computation`).
`path` is a list of string segments describing the structural
descent from the validation root (e.g. `["a" "b" "c"]` for a
nested field, `["[0]" "mtu"]` for a list element's field).
When null (default), `validate` is auto-derived by wrapping
`check` in a `typeCheck` effect. Supply a custom `verify` for
types that decompose checking (e.g. Record sends separate
effects per field for blame tracking).
- `description` — Documentation string (default = `name`)
- `universe` — Optional universe level override. When null (default),
computed from `checkTypeLevel(kernelType)`. Use when the kernelType
is a fallback (e.g., `H.function_` for Pi) that doesn't capture the
real universe level.
- `approximate` — When true, the kernelType is a sound but lossy
approximation (e.g., `H.function_` for Pi, `H.any` for Sigma).
Suppresses `_kernel`, `kernelCheck`, and `prove` on the result,
since the kernel representation doesn't precisely capture this type.
The kernelType is still used internally for universe computation.
## `refine`
Narrow a type with an additional predicate. Creates a refinement type
whose check = kernelDecide(v) ∧ guard(v) (conjunction).
The base type's kernel provides structural checking; the guard handles
the refinement predicate the kernel cannot express.
Grounded in Freeman & Pfenning (1991) "Refinement Types for ML" and Rondon et al. (2008) "Liquid Types".
## `validate`
Standalone effectful validation with explicit context string.
Sends a `typeCheck` effect with the given type, value, and context.
The handler receives `{ type, context, value }` and determines the
response: throw, collect error, log, or offer restarts.
For typical use, prefer `type.validate` (auto-derived by `mkType`,
uses the type's name as context). This 3-arg form is for cases
where a custom context string is needed.
```
validate : Type → Value → String → Computation Bool
```
### Linear
Linear type constructors: structural guards for capability tokens.
Pure type predicates that check token structure without consuming.
Usage enforcement is in effects/linear.nix (separate concerns).
Linear(T) — exactly one consume required
Affine(T) — at most one consume (release allowed)
Graded(n, T) — exactly n consumes (generalizes Linear/Affine)
See Orchard et al. (2019) for graded modal types.
## `Affine`
Affine type: capability token that may be consumed at most once.
```
Affine : Type -> Type
```
Structurally identical to `Linear(T)`. The name communicates that the
resource may be explicitly released (dropped) via `effects/linear.release`
without consuming it — "at most once" vs Linear's "exactly once."
The structural guard is the same: both check for a valid capability
token with inner type T. The usage distinction (exactly-once vs
at-most-once) is enforced by the effect handler, not the type system.
Operations:
- `.check v` — pure guard: is v a valid affine token wrapping T?
- `.validate v` — effectful: sends `typeCheck` for blame tracking
- `.innerType` — the wrapped type T
## `Graded`
Graded type: capability token with usage multiplicity annotation.
```
Graded : { maxUses : Int | null, innerType : Type } -> Type
```
Generalizes Linear and Affine via a `maxUses` parameter:
```nix
Graded { maxUses = 1; innerType = T; } # ≡ Linear(T)
Graded { maxUses = null; innerType = T; } # ≡ Unlimited(T)
Graded { maxUses = n; innerType = T; } # ≡ Exact(n, T)
```
The structural guard is the same as Linear and Affine — token
structure with inner type check. The `maxUses` appears in the type
name for documentation but is NOT checked by the guard (the grade
lives in handler state, not the token).
The name uses ω for null (unlimited):
`Graded(1, Int)`, `Graded(5, String)`, `Graded(ω, Bool)`
From Orchard et al. (2019) "Quantitative Program Reasoning with
Graded Modal Types" — semiring-indexed usage annotations where
+ models branching, × models sequencing, 1 = linear, ω = unlimited.
Operations:
- `.check v` — pure guard: is v a valid graded token wrapping T?
- `.validate v` — effectful: sends `typeCheck` for blame tracking
- `.innerType` — the wrapped type T
- `.maxUses` — the declared usage multiplicity
## `Linear`
Linear type: capability token that must be consumed exactly once.
```
Linear : Type -> Type
```
Creates a type whose `check` verifies the capability token structure:
```nix
{ _linear = true, id = Int, resource = innerType }
```
Pure structural guard — checking does not consume the token.
`effects/linear.nix` tracks consumption separately.
Adequacy invariant:
```
Linear(T).check v ⟺ all typeCheck effects in Linear(T).validate v pass
```
Holds by construction via `mkType`'s auto-derived `validate`.
Operations:
- `.check v` — pure guard: is v a valid linear token wrapping T?
- `.validate v` — effectful: sends `typeCheck` for blame tracking
- `.innerType` — the wrapped type T
### Primitives
Primitive types: String, Int, Bool, Float, Attrs, Path, Function, Null, Unit, Any.
## `Any`
Top type. Every value inhabits Any.
## `Attrs`
Attribute set type (any attrset).
## `Bool`
Boolean type.
## `Float`
Float type.
## `Function`
Function type.
## `Int`
Integer type.
## `Null`
Null type. Only null inhabits it.
## `Path`
Path type.
## `String`
String type.
## `Unit`
Unit type. Isomorphic to Null — the trivial type with one inhabitant.
### Refinement
Refinement types and predicate combinators.
Grounded in Freeman & Pfenning (1991) and Rondon et al. (2008).
## `allOf`
Combine predicates with conjunction: (allOf [p1 p2]) v = p1 v && p2 v.
## `anyOf`
Combine predicates with disjunction: (anyOf [p1 p2]) v = p1 v || p2 v.
## `inRange`
Predicate factory: (inRange lo hi) v = lo <= v <= hi.
## `matching`
Predicate factory: (matching pattern) s = s matches regex pattern.
## `negate`
Negate a predicate: (negate p) v = !(p v).
## `nonEmpty`
Predicate: string or list is non-empty.
## `nonNegative`
Predicate: value >= 0.
## `positive`
Predicate: value > 0.
## `refined`
Create a named refinement type.
```
refined : string -> Type -> (value -> bool) -> Type
```
### Universe
Universe hierarchy: Type_0 : Type_1 : Type_2 : ... Lazy infinite tower.
## `level`
Get the universe level of a type.
## `typeAt`
Create universe type at level n (cumulative). `Type_n` contains all types
with universe ≤ n. `Type_n` itself has universe n + 1.
```
Type_n : Type_(n+1) for all n
```
## Streams
### Combine
Stream combination: concat, interleave, zip, zipWith.
## `concat`
Concatenate two streams: all elements of the first, then all of the second.
```
concat : Computation (Step r a) -> Computation (Step s a) -> Computation (Step s a)
```
## `interleave`
Interleave two streams: alternate elements from each.
```
interleave : Computation (Step r a) -> Computation (Step s a) -> Computation (Step null a)
```
## `zip`
Zip two streams into a stream of pairs.
Stops when either stream ends.
```
zip : Computation (Step r a) -> Computation (Step s b) -> Computation (Step null { fst : a, snd : b })
```
## `zipWith`
Zip two streams with a combining function.
```
zipWith : (a -> b -> c) -> Computation (Step r a) -> Computation (Step s b) -> Computation (Step null c)
```
### Core
Stream primitives: done/more/fromList/iterate/range/replicate.
## `done`
Terminate a stream with a final value.
```
done : a -> Computation (Step a b)
```
## `fromList`
Create a stream from a list.
```
fromList : [a] -> Computation (Step null a)
```
## `iterate`
Create an infinite stream by repeated application.
```
iterate f x = [x, f(x), f(f(x)), ...]
```
Must be consumed with a limiting combinator (take, takeWhile).
```
iterate : (a -> a) -> a -> Computation (Step r a)
```
## `more`
Yield an element and a continuation stream.
```
more : a -> Computation (Step r a) -> Computation (Step r a)
```
## `range`
Create a stream of integers from start (inclusive) to end (exclusive).
```
range : int -> int -> Computation (Step null int)
```
## `replicate`
Create a stream of n copies of a value.
```
replicate : int -> a -> Computation (Step null a)
```
### Limit
Stream limiting: take, takeWhile, drop.
## `drop`
Skip the first n elements of a stream.
```
drop : int -> Computation (Step r a) -> Computation (Step r a)
```
## `take`
Take the first n elements of a stream.
```
take : int -> Computation (Step r a) -> Computation (Step null a)
```
## `takeWhile`
Take elements while a predicate holds.
```
takeWhile : (a -> bool) -> Computation (Step r a) -> Computation (Step null a)
```
### Reduce
Stream reduction: fold, toList, length, sum, any, all.
## `all`
Check if all elements satisfy a predicate.
```
all : (a -> bool) -> Computation (Step r a) -> Computation bool
```
## `any`
Check if any element satisfies a predicate.
Short-circuits on first match (via lazy evaluation).
```
any : (a -> bool) -> Computation (Step r a) -> Computation bool
```
## `fold`
Left fold over a stream.
```
fold : (b -> a -> b) -> b -> Computation (Step r a) -> Computation b
```
## `length`
Count the number of elements in a stream.
```
length : Computation (Step r a) -> Computation int
```
## `sum`
Sum all numeric elements in a stream.
```
sum : Computation (Step r number) -> Computation number
```
## `toList`
Collect all stream elements into a list.
```
toList : Computation (Step r a) -> Computation [a]
```
### Transform
Stream transformations: map, filter, scanl.
## `filter`
Keep only elements satisfying a predicate.
```
sfilter : (a -> bool) -> Computation (Step r a) -> Computation (Step r a)
```
## `map`
Map a function over each element of a stream.
```
smap : (a -> b) -> Computation (Step r a) -> Computation (Step r b)
```
## `scanl`
Accumulate a running fold over the stream, yielding each intermediate value.
```
scanl : (b -> a -> b) -> b -> Computation (Step r a) -> Computation (Step r b)
```
## Type Checker
### Check
Semi-trusted (Layer 1): uses the TCB (eval/quote/conv) and reports
type errors via `send "typeError"`. Bugs here may produce wrong
error messages but cannot cause unsoundness.
Spec reference: kernel-spec.md §7–§9.
## Core Functions
- `check : Ctx → Tm → Val → Computation Tm` — checking mode (§7.4).
Verifies that `tm` has type `ty` and returns an elaborated term.
- `infer : Ctx → Tm → Computation { term; type; }` — synthesis mode (§7.3).
Infers the type of `tm` and returns the elaborated term with its type.
- `checkType : Ctx → Tm → Computation Tm` — verify a term is a type (§7.5).
- `checkTypeLevel : Ctx → Tm → Computation { term; level; }` — like
`checkType` but also returns the universe level (§8.2).
## Context Operations (§7.1)
- `emptyCtx` — empty typing context `{ env = []; types = []; depth = 0; }`
- `extend : Ctx → String → Val → Ctx` — add a binding (index 0 = most recent)
- `lookupType : Ctx → Int → Val` — look up a variable's type by index
## Test Helpers
- `runCheck : Computation → Value` — run a computation through the
trampoline handler, aborting on `typeError` effects.
- `checkTm : Ctx → Tm → Val → Tm|Error` — check and unwrap.
- `inferTm : Ctx → Tm → { term; type; }|Error` — infer and unwrap.
## Key Behaviors
- **Sub rule**: when checking mode doesn't match (e.g., checking a
variable), falls through to `infer` and uses `conv` to compare.
- **Cumulativity**: `U(i) ≤ U(j)` when `i ≤ j` (§8.3).
- **Large elimination**: motives may return any universe, enabling
type-computing eliminators (`checkMotive`).
- **Trampolining**: Succ and Cons chains checked iteratively (§11.3).
## `diag`
# fx.tc.check.diag — Kernel Diagnostic Shell
Outside the trust boundary. Routes kernel check/infer results
through the trusted core and decorates failures with a resolved
hint + a SourceMap-sourced surface origin. No new effects.
## API
- `sourceMap` — SourceMap data type and combinators. See the
module's own doc for the full surface.
- `checkD : Ctx -> Tm -> Val -> SourceMap -> Any`
- `inferD : Ctx -> Tm -> SourceMap -> Any`
- `runCheckD : SourceMap -> Computation -> Any`
- `runCheckDLazy : (Unit -> SourceMap) -> Computation -> Any`
On success, these return what the trusted core returned (the
elaborated Tm for checkD, `{term; type;}` for inferD). On failure,
they return `{ error; msg; expected; got; hint; surface; }`.
`runCheckDLazy` defers `mkSm null` into the failure branch, so the
success path pays one closure allocation instead of the full SM
walker. Kernel HOAS entry points (`checkHoas`/`inferHoas`) use this
variant.
`hint` is a `Hint` record (`{ _tag="Hint"; text; category;
severity; docLink; }`) from `fx.diag.hints.resolve`, or null.
`surface` is the SourceMap's hoas payload at the blame chain's
leaf, or null when the chain exits the mapped region.
Soundness audit: this module contains no kernel rule logic. A bug
here can produce wrong hint text or an incorrect surface back-map;
it cannot cause an ill-typed term to be accepted.
### Conv
Checks whether two values are definitionally equal at a given
binding depth. Purely structural — no type information used, no
eta expansion. Pure function — part of the TCB.
Spec reference: kernel-spec.md §6.
## Core Functions
- `conv : Depth → Val → Val → Bool` — check definitional equality.
- `convSp : Depth → Spine → Spine → Bool` — check spine equality
(same length, pairwise `convElim`).
- `convElim : Depth → Elim → Elim → Bool` — check elimination frame
equality (same tag, recursively conv on carried values).
## Conversion Rules
- §6.1 **Structural**: same-constructor values with matching fields.
Universe levels compared by `==`. Primitive literals by value.
- §6.2 **Binding forms**: Pi, Lam, Sigma compared under a fresh
variable at depth d (instantiate both closures, compare at d+1).
- §6.3 **Compound values**: recursive on all components.
- §6.4 **Neutrals**: same head level and convertible spines.
- §6.5 **Catch-all**: different constructors → false.
## Trampolining
VSucc and VCons chains use `genericClosure` to avoid stack overflow
on S^5000 or cons^5000 comparisons.
## No Eta
`conv` does not perform eta expansion: a neutral `f` and
`λx. f(x)` are **not** definitionally equal. Cumulativity
(`U(i) ≤ U(j)`) is handled in check.nix, not here.
### Elaborate
Bridges the fx.types layer to the kernel's term representation
via the HOAS combinator layer. Provides the Nix ↔ kernel boundary.
## Type Elaboration
- `elaborateType : FxType → Hoas` — convert an fx.types type descriptor
to an HOAS tree. Dispatches on: (1) `_kernel` annotation, (2) structural
fields (Pi: domain/codomain, Sigma: fstType/sndFamily), (3) name
convention (Bool, Nat, String, Int, Float, ...).
Dependent Pi/Sigma require explicit `_kernel` annotation.
## Value Elaboration
- `elaborateValue : Hoas → NixVal → Hoas` — convert a Nix value to
an HOAS term tree given its HOAS type. Bool→true_/false_, Int→natLit,
List→cons chain, Sum→inl/inr, Sigma→pair. Trampolined for large lists.
## Structural Validation
- `validateValue : String → Hoas → NixVal → [{ path; msg; }]` —
applicative structural validator. Mirrors `elaborateValue`'s recursion
but accumulates all errors instead of throwing on the first.
Path accumulator threads structural context (Reader effect).
Error list is the free monoid (Writer effect).
Empty list ↔ `elaborateValue` would succeed (soundness invariant).
## Value Extraction
- `extract : Hoas → Val → NixValue` — reverse of `elaborateValue`.
Converts kernel values back to Nix values. VZero→0, VSucc^n→n,
VCons chain→list, VInl/VInr→tagged union.
Pi extraction wraps the VLam as a Nix function with boundary conversion.
Opaque types (Attrs, Path, Function, Any) throw — kernel discards payloads.
- `extractInner : Hoas → Val → Val → NixValue` — three-argument extraction
with kernel type value threading. Supports dependent Pi/Sigma via closure
instantiation instead of sentinel tests.
- `reifyType : Val → Hoas` — converts a kernel type value back to HOAS.
Fallback for when HOAS body application fails (dependent types).
Loses sugar (VSigma→sigma, not record).
## Decision Procedure
- `decide : Hoas → NixVal → Bool` — returns true iff elaboration
and kernel type-checking both succeed. Uses `tryEval` for safety.
- `decideType : FxType → NixVal → Bool` — elaborate type then decide.
## Full Pipeline
- `verifyAndExtract : Hoas → Hoas → NixValue` — type-check an HOAS
implementation against an HOAS type, evaluate, extract to Nix value.
Throws on type error.
### Eval
Pure evaluator: interprets kernel terms in an environment of
values. Zero effect system imports — part of the trusted computing
base (TCB).
Spec reference: kernel-spec.md §4, §9.
## Core Functions
- `eval : Env → Tm → Val` — evaluate with default fuel (10M steps)
- `evalF : Int → Env → Tm → Val` — evaluate with explicit fuel budget
- `instantiate : Closure → Val → Val` — apply a closure to an argument
## Elimination Helpers
- `vApp : Val → Val → Val` — apply a function value (beta-reduces VLam, extends spine for VNe)
- `vFst`, `vSnd` — pair projections
- `vNatElim`, `vListElim` — inductive eliminators
- `vSumElim` — sum elimination
- `vJ` — identity elimination (computes to base on VRefl)
## Trampolining (§11.3)
`vNatElim`, `vListElim`, `succ` chains, and `cons` chains use
`builtins.genericClosure` to flatten recursive structures iteratively,
guaranteeing O(1) stack depth on inputs like S^10000(0) or cons^5000.
## Fuel Mechanism (§9)
Each `evalF` call decrements a fuel counter. When fuel reaches 0,
evaluation throws `"normalization budget exceeded"`. This bounds
total work and prevents unbounded computation in the Nix evaluator.
Default budget: 10,000,000 steps.
### Hoas
Higher-Order Abstract Syntax layer that lets you write kernel terms
using Nix lambdas for variable binding. The `elaborate` function
compiles HOAS trees to de Bruijn indexed Tm terms.
Spec reference: kernel-spec.md §2.
## Example
```nix
# Π(A:U₀). A → A
H.forall "A" (H.u 0) (A: H.forall "x" A (_: A))
```
## Type Combinators
- `nat`, `bool`, `unit`, `void` — base types
- `string`, `int_`, `float_`, `attrs`, `path`, `function_`, `any` — primitive types
- `listOf : Hoas → Hoas` — List(elem)
- `sum : Hoas → Hoas → Hoas` — Sum(left, right)
- `eq : Hoas → Hoas → Hoas → Hoas` — Eq(type, lhs, rhs)
- `u : Int → Hoas` — Universe at level
- `forall : String → Hoas → (Hoas → Hoas) → Hoas` — Π-type (Nix lambda for body)
- `sigma : String → Hoas → (Hoas → Hoas) → Hoas` — Σ-type
## Compound Types (Sugar)
- `record : [{ name; type; }] → Hoas` — nested Sigma (sorted fields)
- `maybe : Hoas → Hoas` — Sum(inner, Unit)
- `variant : [{ tag; type; }] → Hoas` — nested Sum (sorted tags)
## Term Combinators
- `lam : String → Hoas → (Hoas → Hoas) → Hoas` — λ-abstraction
- `let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas` — let binding
- `zero`, `succ`, `true_`, `false_`, `tt`, `refl` — intro forms
- `nil`, `cons`, `pair`, `inl`, `inr` — data constructors
- `stringLit`, `intLit`, `floatLit`, `attrsLit`, `pathLit`, `fnLit`, `anyLit` — primitive literals
- `absurd`, `ann`, `app`, `fst_`, `snd_` — elimination/annotation
## Eliminators
- `ind` — NatElim(motive, base, step, scrut)
- `boolElim` — (k : Level) → (Q : bool → U(k)) → Q true_ → Q false_ → (b : bool) → Q b
- `listElim` — ListElim(elem, motive, onNil, onCons, scrut)
- `sumElim` — SumElim(left, right, motive, onLeft, onRight, scrut)
- `j` — J(type, lhs, motive, base, rhs, eq)
## Elaboration
- `elaborate : Int → Hoas → Tm` — compile at given depth
- `elab : Hoas → Tm` — compile from depth 0
## Convenience
- `checkHoas : Hoas → Hoas → Tm|Error` — elaborate type+term, type-check
- `inferHoas : Hoas → { term; type; }|Error` — elaborate and infer
- `natLit : Int → Hoas` — build S^n(zero)
## Stack Safety
Binding chains (pi/lam/sigma/let), succ chains, and cons chains
are elaborated iteratively via `genericClosure` — safe to 8000+ depth.
### Quote
Converts values back to terms, translating de Bruijn levels to
indices. Pure function — part of the TCB.
Spec reference: kernel-spec.md §5.
## Core Functions
- `quote : Depth → Val → Tm` — read back a value at binding depth d.
Level-to-index conversion: `index = depth - level - 1`.
- `quoteSp : Depth → Tm → Spine → Tm` — quote a spine of eliminators
applied to a head term (folds left over the spine).
- `quoteElim : Depth → Tm → Elim → Tm` — quote a single elimination
frame applied to a head term.
- `nf : Env → Tm → Tm` — normalize: `eval` then `quote`. Useful for
testing roundtrip idempotency (`nf env (nf env tm) == nf env tm`).
- `lvl2Ix : Depth → Level → Index` — level-to-index helper.
## Trampolining
VSucc and VCons chains are quoted iteratively via `genericClosure`
for O(1) stack depth on deep values (5000+ elements).
## Binder Quotation
For VPi, VLam, VSigma: instantiates the closure with a fresh
variable at the current depth, then quotes the body at `depth + 1`.
### Term
Syntax of the kernel's term language. All 48 constructors produce
attrsets with a `tag` field (not `_tag`, to distinguish kernel terms
from effect system nodes). Binding is de Bruijn indexed: `mkVar i`
refers to the i-th enclosing binder (0 = innermost).
Name annotations (`name` parameter on `mkPi`, `mkLam`, `mkSigma`,
`mkLet`) are cosmetic — used only in error messages, never in
equality checking.
Spec reference: kernel-spec.md §2.
## Constructors
### Variables and Binding
- `mkVar : Int → Tm` — variable by de Bruijn index
- `mkLet : String → Tm → Tm → Tm → Tm` — `let name : type = val in body`
- `mkAnn : Tm → Tm → Tm` — type annotation `(term : type)`
### Functions (§2.2)
- `mkPi : String → Tm → Tm → Tm` — dependent function type `Π(name : domain). codomain`
- `mkLam : String → Tm → Tm → Tm` — lambda `λ(name : domain). body`
- `mkApp : Tm → Tm → Tm` — application `fn arg`
### Pairs (§2.3)
- `mkSigma : String → Tm → Tm → Tm` — dependent pair type `Σ(name : fst). snd`
- `mkPair : Tm → Tm → Tm` — pair constructor `(fst, snd)`
- `mkFst : Tm → Tm` — first projection
- `mkSnd : Tm → Tm` — second projection
### Inductive Types
- `mkNat`, `mkZero`, `mkSucc`, `mkNatElim` — natural numbers with eliminator
- `mkList`, `mkNil`, `mkCons`, `mkListElim` — lists with eliminator
- `mkUnit`, `mkTt` — unit type and value
- `mkSum`, `mkInl`, `mkInr`, `mkSumElim` — disjoint sum with eliminator
- `mkEq`, `mkRefl`, `mkJ` — identity type with J eliminator
### Universes
- `mkU : (Int | Tm) → Tm` — universe `U(level)`. Accepts either a
concrete Int (wrapped via `mkLevelLit`) or a Level-typed Tm
directly.
- `mkLevelLit : Int → Tm` — builds `suc^n zero` as a Level term.
### Axiomatized Primitives (§2.1)
- `mkString`, `mkInt`, `mkFloat`, `mkAttrs`, `mkPath`, `mkFunction`, `mkAny` — type formers
- `mkStringLit`, `mkIntLit`, `mkFloatLit`, `mkAttrsLit`, `mkPathLit`, `mkFnLit`, `mkAnyLit` — literal values
### Value
Values are the semantic domain produced by evaluation. They use
de Bruijn *levels* (counting outward from the top of the context),
not indices, which makes weakening trivial.
Spec reference: kernel-spec.md §3.
## Closures
`mkClosure : Env → Tm → Closure` — defunctionalized closure.
No Nix lambdas in the TCB; a closure is `{ env, body }` where
`body` is a kernel Tm evaluated by `eval.instantiate`.
## Value Constructors
Each `v*` constructor mirrors a term constructor:
- `vLam`, `vPi` — function values/types (carry name, domain, closure)
- `vSigma`, `vPair` — pair types/values
- `vNat`, `vZero`, `vSucc` — natural number values
- `vList`, `vNil`, `vCons` — list values
- `vUnit`, `vTt` — unit
- `vSum`, `vInl`, `vInr` — sum values
- `vEq`, `vRefl` — identity values
- `vU` — universe values
- `vString`, `vInt`, `vFloat`, `vAttrs`, `vPath`, `vFunction`, `vAny` — primitive types
- `vStringLit`, `vIntLit`, `vFloatLit`, `vAttrsLit`, `vPathLit`, `vFnLit`, `vAnyLit` — primitive literals
## Neutrals
`vNe : Level → Spine → Val` — a stuck computation: a variable
(identified by de Bruijn level) applied to a spine of eliminators.
`freshVar : Depth → Val` — neutral with empty spine at the given depth.
Used during type-checking to introduce fresh variables under binders.
## Elimination Frames (Spine Entries)
- `eApp`, `eFst`, `eSnd` — function/pair eliminators
- `eNatElim`, `eListElim`, `eSumElim`, `eJ` — inductive eliminators
### Verified
High-level combinators for writing kernel-checked implementations.
Write programs with these combinators, then call `v.verify` to
type-check and extract a Nix function that is correct by construction.
## Example
```nix
# Verified successor: Nat → Nat
v.verify (H.forall "x" H.nat (_: H.nat))
(v.fn "x" H.nat (x: H.succ x))
# → Nix function: n → n + 1
```
## Literals
- `nat : Int → Hoas` — natural number literal (S^n(zero))
- `str : String → Hoas` — string literal
- `int_ : Int → Hoas` — integer literal
- `float_ : Float → Hoas` — float literal
- `true_`, `false_` — boolean literals
- `null_` — unit value (tt)
## Binding
- `fn : String → Hoas → (Hoas → Hoas) → Hoas` — lambda abstraction
- `let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas` — let binding
## Data Operations
- `pair`, `fst`, `snd` — Σ-type construction and projection
- `field : Hoas → String → Hoas → Hoas` — record field projection by name
- `inl`, `inr` — Sum injection
- `app` — function application
## Eliminators (Constant Motive)
These auto-generate the motive `λ_.resultTy`, so you only supply
the result type and the branches:
- `if_ : Hoas → Hoas → { then_; else_; } → Hoas` — Bool elimination
- `match : Hoas → Hoas → { zero; succ : k → ih → Hoas; } → Hoas` — Nat elimination
- `matchList : Hoas → Hoas → Hoas → { nil; cons : h → t → ih → Hoas; } → Hoas` — List elimination
- `matchSum : Hoas → Hoas → Hoas → Hoas → { left; right; } → Hoas` — Sum elimination
## Derived Combinators
- `map : Hoas → Hoas → Hoas → Hoas → Hoas` — map f over a list
- `fold : Hoas → Hoas → Hoas → Hoas → Hoas → Hoas` — fold over a list
- `filter : Hoas → Hoas → Hoas → Hoas` — filter a list by predicate
## Pipeline
- `verify : Hoas → Hoas → NixValue` — type-check + eval + extract
- `verifiedFn : Hoas → Hoas → VerifiedValue` — callable value with
`_hoasImpl` for full kernel body verification in parent types