# 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 …)
```