Desc

fx.experimental.desc-interp.desc: freer monad encoded as a levitated Desc (freeFx = pure + impure plus continuation queue); the substrate descInterp runs.

freeFx

freeFx Eff Resp A : Desc¹ ⊤ — freer monad as a plus-of-two-summands description; the Impure summand's continuation slot is a queue value μI U² (kontQueueApp Eff Resp) (Resp op, A) rather than a meta-level fn.

freeFx : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas (Desc¹ ⊤)

freeFxApp

freeFxApp Eff Resp A — identity-tagged HOAS form of freeFx Eff Resp A; canonApp wrapper that stamps the resulting VDescCon with _canonRef = { id = "freeFx"; params = [Eff, Resp, A]; } so conv/quote short-circuit on the canonical identity.

freeFxApp : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas (Desc¹ ⊤)

impureCon

impureCon Eff Resp A op q — smart constructor for the Impure summand; q : μI U² (kontQueueApp Eff Resp) (Resp op, A) is a queue value carrying the continuation. Emits a desc-con HOAS form with a Desc¹ inr payload storing op and the ret witness through LiftAt 0 1.

impureCon : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas Eff -> Hoas (μI U² kontQueueApp …) -> Hoas (FreeFx Eff Resp A)

kontQueue

kontQueue Eff Resp : IDesc(U × U) — description-side FTCQueue (Kiselyov & Ishii 2015, section 3.1) at the indexed slice; three-summand plus encoding Identity / Leaf / Node where ∃M existentials are reified as descArgAt-bound index witnesses (CDMM 2010, section 6). Levitation transposition of nix/nix-effects/src/queue.nix.

kontQueue : Hoas U -> Hoas (U -> U) -> Hoas (IDesc (U × U))

kontQueueApp

kontQueueApp Eff Resp — identity-tagged HOAS form of kontQueue Eff Resp; canonApp wrapper that stamps the resulting VDescCon with _canonRef = { id = "kontQueue"; params = [Eff, Resp]; } so conv on μI(kontQueueApp …) self-equality short-circuits without forcing .D. X and A are dropped from the wrapper's params — the indexing is intrinsic to IDesc(U × U).

kontQueueApp : Hoas U -> Hoas (U -> U) -> Hoas (IDesc (U × U))

pureCon

pureCon Eff Resp A v — smart constructor for the Pure summand; emits a desc-con HOAS form with a Desc¹ inl payload storing v and the ret witness through LiftAt 0 1.

pureCon : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas A -> Hoas (FreeFx Eff Resp A)

qIdentity

qIdentity Eff Resp X — smart constructor for the Identity summand of kontQueue; emits a desc-con HOAS form at index (X, X) with payload bootInl (X, refl) of the outer plus. Carries _index = { X; A = X; } sidecar.

qIdentity : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas (μI U² kontQueueApp …)

qLeaf

qLeaf Eff Resp X A fn — smart constructor for the Leaf summand; fn : X → μ(freeFxApp Eff Resp A) is a HOAS lam with fn.domain == X (host-level == is the principled Nix-meta surrogate for the descArgAt(X)-instantiation equality the kernel checker would enforce, mirroring qNode's seam check on _index). Emits a desc-con HOAS form at index (X, A) with payload bootInr (bootInl (X, (A, (fn, refl)))) of the nested plus. Carries _index = { X; A; } sidecar.

qLeaf : Hoas U -> Hoas (U -> U) -> Hoas U -> Hoas U -> Hoas (X -> μ freeFx) -> Hoas (μI U² kontQueueApp …)

qNode

qNode Eff Resp l r — smart constructor for the Node summand; l and r are queue values whose _index sidecars supply the index witnesses. Seam M = l._index.A is asserted equal to r._index.X via Nix-level == (kernel has no surface metavariables; the host-level check is the principled enforcement). Emits a desc-con HOAS form at index (l._index.X, r._index.A) with payload bootInr (bootInr (X, (M, (A, (l, (r, refl)))))) of the nested plus. Carries _index = { X; A; } sidecar.

qNode : Hoas U -> Hoas (U -> U) -> Hoas (μI U² kontQueueApp …) -> Hoas (μI U² kontQueueApp …) -> Hoas (μI U² kontQueueApp …)