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

Composed-shortcut

Pipeline per Impure step on a composed op: read op._side / op._inner, project the composed state with extract.Project, recurse via the matching per-side shortcut, then extract.OfElim on the sub-UniRet — Resume → composed Resume; Abort → composed Abort — repacking the sibling state slot via extract.PairRaw.

Soundness: kernel-side composedHandlerShortcutLemma (composed-shortcut-laws.nix) chains composeHandlersInl/InrLemma with per-effect uniform-shortcut lemmas; emitter-side, the _self.tests below conv-check kernel-composed vs shortcut-emitted Vals at concrete canonical ops.

composedHandlerShortcut

composedHandlerShortcut H_short_A H_short_B metaFor op stateVal — composed UniRet Val mirroring eval (composeHandlers … H_A H_B opVal stateVal). op carries _side/_inner sidecars from composedInl/composedInr; metaFor is the composed-UniRet metadata lookup keyed by inner-op tag; per-side shortcuts must return UniRet Vals. null propagates from any of the inputs (kernel fallback).

composedInl

composedInl Op_A Op_B subOp — H.inl Op_A Op_B subOp with _side = "composed-inl", _inner = subOp. Sidecars are ignored by elab and survive K.send's impureCon wrap.

composedInr

composedInr Op_A Op_B subOp — H.inr counterpart of composedInl.

mkComposedMeta

mkComposedMeta { SigmaSHoas; A; respHoas; } — precompute { sumDescVal; leftSigVal; rightSigVal; } for the composed UniRet at one canonical inner op (response type already ι-reduced).

prevCompose-lawsComposed-shortcut-lawsnext