Navigation
/
Manual
GuideIntroductionGetting StartedEffects and HandlersTyped ValidationGenerated DatatypesGeneric ProgrammingOrnaments and Description-Backed DataProof GuideSugar
ConceptsTheory
InternalsTrampolineKernel ArchitectureKernel Formal Specification
Examples
Overview
ProofsProof BasicsEquality ProofsVerified Functions
Effects and ValidationHandler-Swap Validation
Surface LanguagesSurface STLCSTLC Core SurfaceSTLC Sums and ProductsSTLC Recursive ListsSTLC Refinements and Diagnostics
ApplicationsCategory TheoryExpression InterpreterBuild Simulator
API Reference
Core APIKernelCompBindsTrampolineQueueAdaptPipelineStateThunkSugarBuildTypesExperimentalDesc-interpComposeCompose-lawsComposed-shortcutComposed-shortcut-lawsDescDescind-lawsEffectsErrorError-shortcut-lawsError-uniform-shortcut-lawsStateState-shortcut-lawsTypecheckTypecheck-shortcut-lawsExtractKernelTrampoline
DiagnosticsPositionsErrorHintsPretty
EffectsStateReaderWriterAccErrorConditionsChoiceScopeLinearTypecheckHasHandler
TypesFoundationPrimitivesConstructorsRefinementDependentLinearUniverse
StreamsCoreTransformLimitCombineReduce
Type CheckerTermValueQuoteConvEval_internalDispatchCheckDiag_internalElaborateMeta_internalHoas_internal_encoders_forced_indexedSurfaceRegistryGenericDescDatatypeValueDeriveCheckCheckDOrnamentsVerifiedKernel
Diagnostic HintsDArgSort::universe-mismatchDPiSort::universe-mismatchLevelMaxLhs::type-mismatchLevelMaxRhs::type-mismatchLevelSucPred::type-mismatchULevel::type-mismatchAnnType::not-a-typeJType::not-a-typeMotive.PiDom::not-a-typeMotive::not-a-typePiCod::not-a-typePiDom::not-a-typeDArgBody::not-a-descDPiBody::not-a-descDPlusL::not-a-descDPlusR::not-a-descDRecTail::not-a-descMuDesc::not-a-descAppHead::not-a-functionDPiFn::not-a-functionMotive::not-a-functionOpaqueType::not-a-functionDPiFn::type-mismatchDRecIndex::type-mismatchDRetIndex::type-mismatchMuIndex::type-mismatchMuPayload::type-mismatchElem::inhabitation-failedField::inhabitation-failedSigmaFst::inhabitation-failedSigmaSnd::inhabitation-failedTag::inhabitation-failedElem::refinement-failedField::refinement-failedSigmaFst::refinement-failedSigmaSnd::refinement-failedTag::refinement-failedCase::type-mismatchScrut::type-mismatchAnnTerm::type-mismatchAppArg::type-mismatchJType::type-mismatchOpaqueType::type-mismatch::unhandled-boot-inl::unhandled-boot-inr::unhandled-boot-refl::unhandled-lam::unhandled-other::unhandled-pair::unhandled-tt

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`, raw built-in predicates `positive`/`nonNegative`/`inRange`/`nonEmpty`/`matching`, and the kernel-i...
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 non-cumulative Tarski tower; `lift`/`liftTo` coerce across levels; `Type_0`–`Type_4` are predefined; ...