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

Kernel

fx.experimental.desc-interp.kernel: pure/send/bind constructors producing FreeFx Desc values directly as μ freeFxApp data, not Nix-host computations.

bind

bind Eff Resp A B m f — sequence two computations. Pure case applies f to the payload; Impure case snocs f into the queue. Linear continuation chains stay flat in the queue, sidestepping Nix's call-depth ceiling.

bind : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas U -> Hoas (μ freeFxApp Eff Resp A) -> (Hoas A -> Hoas (μ freeFxApp Eff Resp B)) -> Hoas (μ freeFxApp Eff Resp B)

pure

pure Eff Resp A v — lift v into the Pure summand of FreeFx; alias for D.pureCon.

pure : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas A -> Hoas (μ freeFxApp Eff Resp A)

qSnoc

qSnoc Eff Resp B q f — append the Nix-meta continuation f (Hoas q._index.A → Hoas (μ freeFxApp Eff Resp B)) to the right of queue q. The chain's input type is q._index.X and its current output is q._index.A. Identity short-circuits to a fresh qLeaf at (q._index.A, B); otherwise builds qNode q (qLeaf q._index.A B fn) with the seam M = q._index.A asserted via the sidecar invariant on qNode.

qSnoc : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas (μI U² kontQueueApp …) -> (Hoas A -> Hoas (μ freeFxApp Eff Resp B)) -> Hoas (μI U² kontQueueApp …)

send

send Eff Resp op — issue an effect request with the identity continuation; emits an impureCon whose queue slot is qIdentity Eff Resp (Resp op) at index (Resp op, Resp op).

send : Hoas U -> Hoas (U -> U) -> Hoas Eff -> Hoas (μ freeFxApp Eff Resp (Resp op))
prevExtractTrampolinenext