Navigation
Manual
GuideIntroductionGetting StartedEffects and HandlersTyped ValidationGenerated DatatypesGeneric ProgrammingOrnaments and Description-Backed DataProof GuideSugar
ConceptsTheory
InternalsTrampolineSystems ArchitectureKernel 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
API Reference
Core APIKernelCompBindsTrampolineQueueAdaptPipelineStateThunkSugarBuildTypesExperimentalDesc-interpComposeCompose-lawsComposed-shortcutComposed-shortcut-lawsDescDescind-lawsEffectsErrorError-shortcut-lawsError-uniform-shortcut-lawsStateState-shortcut-lawsExtractKernelTrampoline
DiagnosticsPositionsErrorHintsPretty
EffectsStateReaderWriterAccErrorConditionsChoiceScopeLinearTypecheckHasHandler
TypesFoundationPrimitivesConstructorsRefinementDependentLinearUniverse
StreamsCoreTransformLimitCombineReduce
Type CheckerTermValueQuoteConvEval_internalDispatchCheckDiag_internalElaborateMeta_internalHoas_internal_encoders_forced_indexedSurfaceRegistryGenericDescDatatypeValueDeriveCheckCheckDOrnamentsVerified
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

Desc-interp

desc.nix encodes FreeFx as plus pureSummand impureSummand; continuations live in an FTCQueue value (Kiselyov & Ishii) rather than meta-level Nix functions. kernel.nix mirrors fx.kernel's pure/send/bind; bind snocs into the Impure summand's queue without recursing on the μ-tree. trampoline.nix drives programs via builtins.genericClosure at O(1) host stack depth.

Handler shortcut layering

Each canonical handler op admits a partial-evaluation residual that bypasses kernel vApp per Impure step. Soundness splits:

  • kernel-side (effects/*-shortcut-laws.nix): H.refl lemma handle_X op s ≡_kernel mkResumeAt … r s (resp. mkAbortAt) certifying the per-op rewrite under ι+β.
  • emitter-side (extract.nix): per-primitive Val-conv test eval (HOAS witness) ≡_Val extract (Primitive …). Sugars (Resume/Abort/PairRaw) fold into primitives.
  • composed-side (compose.nix + composed-shortcut.nix + composed-shortcut-laws.nix): composeHandlers over UniRet closes the algebra under +. Six lemmas chain composeHandlersInl/InrLemma with per-effect uniform-shortcut lemmas; composedHandlerShortcut mirrors the kernel-composed path by direct Val construction.

Adding a new effect with a handler shortcut

Recipe — apply in order:

  1. Identify canonical RHS shapes. Reduce handle_X op s per constructor via ι+β. Each canonical op should normalise to mkResumeAt … r s or mkAbortAt … v s (or a bare H.pair _ _ outside the UniRet shape).

  2. Extend extract.nix only if needed. Existing sugars cover the UniRet and bare-pair shapes; primitives (DescCon, BootInl, BootInr, Pair, Tt, BootRefl) suffice for anything else. Add a sugar only when a non-trivial shape repeats across multiple effects.

  3. Write effects/x-shortcut-laws.nix. One H.refl lemma per canonical op asserting handle_X op s ≡_kernel mkXAt …. Mirror effects/state-shortcut-laws.nix's withPrefix/ lamPrefix helper layout. If uniformOf_X differs from handle_X (error's three strategies), add effects/x-uniform-shortcut-laws.nix too.

  4. Wire handlerShortcut in atType. Pre-compute metadata Vals (leftSig, rightSig, sumDescVal) once per instantiation; in handlerShortcut op stateVal, dispatch on op._opTag and return extract (Resume …) / extract (Abort …) / extract (PairRaw …). Smart constructors tag canonical ops via _opTag = "<effect>-<op>". If uniformOf_X is needed for composition, expose uniformOfShort (or uniformOfShortAt A if A varies post-atType).

  5. Add parity tests in trampoline.nix. For each canonical op, compare runX { handler; dispatch; } vs runX { handler; dispatch; handlerShortcut; } via fx.tc.conv.conv 0 on both .value and .state. For ops that abort with a Nix throw (strict-style), force .state.tag under builtins.tryEval and assert both paths trip the throw.

Composition with another effect via composeHandlers reuses the per-effect uniformOfShort plus composedHandlerShortcut H_short_A H_short_B metaFor; soundness is anchored kernel-side by composed-shortcut-laws.nix without any per-effect-pair work.

Sub-namespaces

Source

prevExperimentalComposenext