# 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-`sumElim`s 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._