Compose

fx.experimental.desc-interp.compose: universal handler-result type UniRet and its smart constructors. Every kernel-resident handler can be re-shaped into a UniRet-returning form; composeHandlers operates uniformly on that shape.

UniRet

UniRet : Π (S:U) (Op:U) (Resp:Op→U) (op:Op) (A:U). U — universal handler-result type. Left summand Σ _r:(Resp op). S = resume (response + new state). Right summand Σ _a:A. S = abort (final value + new state). State's handle_StateTy is conv-equal to Π S A. Π op:EffState S. Π _s:S. UniRet S (EffState S) (Resp_State S) op A — see the inline conv test below.

UniRetTy

Π-type of UniRet: Π (S:U) (Op:U) (Resp:Op→U) (op:Op) (A:U). U.

composeHandlers

composeHandlers S_A S_B Op_A Op_B Resp_A Resp_B A H_A H_B — kernel-resident combinator taking two UniRet-shaped handlers and producing a UniRet-shaped handler over the sum effect. Body dispatches outer sumElim on op, projects the matching state slot, runs the per-effect handler, then inner-sumElims on the UniRet result to re-package into the composed shape with the threaded product state. The composed-law witness lifts per-effect laws through this shape.

composeHandlersTy

Π-type of composeHandlers: Π (S_A S_B Op_A Op_B : U). Π (Resp_A : Op_A → U). Π (Resp_B : Op_B → U). Π (A : U). (Π op:Op_A. Π _s:S_A. UniRet S_A Op_A Resp_A op A) → (Π op:Op_B. Π _s:S_B. UniRet S_B Op_B Resp_B op A) → Π op:(Sum Op_A Op_B). Π _s:(Σ S_A S_B). UniRet (Σ S_A S_B) (Sum Op_A Op_B) (composedResp Op_A Op_B Resp_A Resp_B) op A.

composedResp

composedResp Op_A Op_B Resp_A Resp_B op — paired response family for the sum effect. sumElim-driven so composedResp … (inl opA) ≡ Resp_A opA and composedResp … (inr opB) ≡ Resp_B opB by iota; composeHandlers relies on this conv-equality to retype the mkResume r-argument.

composedRespAt

composedRespAt Op_A Op_B Resp_A Resp_B — Nix-level helper for the 4-arg composedResp spine; result has type Π op:(Sum Op_A Op_B). U.

composedRespTy

Π-type of composedResp: Π (Op_A Op_B : U). Π (Resp_A : Op_A → U). Π (Resp_B : Op_B → U). Π op:(Sum Op_A Op_B). U.

mkAbort

mkAbort : Π S Op Resp op A. A → S → UniRet S Op Resp op A — right-injection smart constructor.

mkAbortAt

mkAbortAt S Op Resp op A a s — Nix-level helper for the fully-applied mkAbort spine.

mkAbortTy

Π-type of mkAbort.

mkResume

mkResume : Π S Op Resp op A. (Resp op) → S → UniRet S Op Resp op A — left-injection smart constructor.

mkResumeAt

mkResumeAt S Op Resp op A r s — Nix-level helper for the fully-applied mkResume spine.

mkResumeTy

Π-type of mkResume.

uniRetAt

uniRetAt S Op Resp op A — Nix-level helper for the fully-applied UniRet spine; consumers avoid hand-rolling the 5-arg app each time.