Type Checker
9 pages
Check
Semi-trusted (Layer 1): uses the TCB (eval/quote/conv) and reports
type errors via send "typeError". Bugs...
Conv
Checks whether two values are definitionally equal at a given
binding depth. Purely structural — no type information...
Elaborate
Bridges the fx.types layer to the kernel's term representation
via the HOAS combinator layer. Provides the Nix ↔ kernel...
Eval
Pure evaluator: interprets kernel terms in an environment of
values. Zero effect system imports — part of the trusted...
Hoas
Higher-Order Abstract Syntax layer that lets you write kernel terms
using Nix lambdas for variable binding. The...
Quote
Converts values back to terms, translating de Bruijn levels to
indices. Pure function — part of the TCB.
Spec...
Term
Syntax of the kernel's term language. All 48 constructors produce
attrsets with a tag field (not _tag, to distinguish...
Value
Values are the semantic domain produced by evaluation. They use
de Bruijn levels (counting outward from the top of the...
Verified
High-level combinators for writing kernel-checked implementations.
Write programs with these combinators, then call...