Types
7 pages
Foundation
Type system foundation: `mkType`/`check`/`validate`/`make`/`refine` build types from kernel HOAS representations and the guard/effect machinery underneath.
Primitives
Primitive types: String/Int/Bool/Float/Attrs/Path/Derivation/Function/Null/Unit/Any — universe-0 atomic types corresponding to Nix's value categories.
Constructors
Type constructors: Record/RecordOpen/ListOf/Maybe/Either/Variant — higher-kinded builders composing simpler types with per-component blame.
Refinement
Refinement types: `refined` plus `allOf`/`anyOf`/`negate` and built-in predicates `positive`/`nonNegative`/`inRange`/`nonEmpty`/`matching`.
Dependent
fx.types.dependent: dependent contracts Pi (Π), Sigma (Σ), Certified, Vector, DepRecord — higher-order contracts checked incrementally at each applicatio...
Linear
Linear type constructors: `Linear`/`Affine`/`Graded` — pure structural guards for capability tokens; usage enforcement lives in the linear effect handler.
Universe
Universe hierarchy: `typeAt n` produces `Type_n` in a cumulative MLTT tower; `Type_0`–`Type_4` are predefined; `level` reads a type's universe.