# Desc


A uniform interface to levitated descriptions
(`Desc I k`) that hides the encoder details behind a small
algebra of views, folds, and predicates. Every entry accepts
either HOAS or evaluated `Val` descriptions — `evalDesc`
normalises to `Val` idempotently.

`descView` returns a one-step semantic view exposing the outer
constructor as both an integer `idx` (0=ret, 1=arg, 2=rec, 3=pi,
4=plus) and a human-readable `kind` string, alongside the
constructor-specific fields (`I`, `k`, `j`, `sTy`, `tFn`, `sub`,
`A`, `B`, plus optional `label`/`conLabel` sidecar metadata).

`foldDesc` is the catamorphism: pass per-constructor handler
functions, each receiving a record with the recursed sub-values
already materialised. `foldDescM` is the monadic dual — each
handler returns a `Computation R` and the combinator binds
sub-results before invoking the matching case; `paraDM` is the
paramorphic variant that additionally exposes the original
sub-description `Val` at each recursive site (for callers that
consult kernel-level shape without paying for a monadic
descent). `foldDescWithPath` mirrors `foldDescM` and threads a
`[fx.diag.positions]` chain extended at each descent so handlers
can construct positionally-blamed errors directly from inside
the fold. `mapDesc` is the structural map — handlers return
either replacement HOAS, an explicit `{ _replaceChildren = …; }`
payload, or a `Val` for direct substitution; identity mappers
reconstruct definitionally-equal outputs via the canonical
encoder chain.

`deepEqualDesc` decides definitional equality by delegating to
`fx.tc.conv.conv`; presentation labels (`_label`, `_conLabel`)
are conv-irrelevant. `children`, `shape`, and the `isRet` /
`isArg` / `isRec` / `isPi` / `isPlus` predicates round out the
introspection surface for callers that want lightweight
structural queries without writing a full fold.

## `children`

_children: direct sub-descriptions list — empty for `ret`, `[body]` for `arg`/`rec`/`pi` (arg applies the body to a `vTt` placeholder), `[A, B]` for `plus`._

```
children : Hoas | Val -> [Val]
```

## `deepEqualDesc`

_deepEqualDesc: definitional equality on description values — evaluates both arguments via `evalDesc`, then runs `fx.tc.conv.conv 0` for full conv-equality._

```
deepEqualDesc : Hoas | Val -> Hoas | Val -> Bool
```

## `descView`

_descView: one-step semantic view of a description value — returns `{ idx, kind, I, k, ... }` selecting the outer constructor (`0` = ret, `1` = arg, `2` = rec, `3` = pi, `4` = plus); throws on malformed inputs._

```
descView : Hoas | Val -> { idx : 0..4; kind : String; I : Val; k : Val; ... }
```

Friendly wrapper around `fx.tc.eval.descView` that adds a
human-readable `kind` field alongside the integer `idx`.
Returns the raw view fields (`I`, `k`, `j`, `sTy`, `tFn`,
`sub`, `A`, `B`, optional `label`/`conLabel`) so callers can
peel apart any description shape uniformly.

Use this entry as the canonical view for generic programming
over levitated descriptions; the lower-level
`fx.tc.eval.descView` is identical in semantics but skips the
kind-naming step.

## `evalDesc`

_evalDesc: idempotent description normaliser — returns evaluated `Val` descriptions unchanged, evaluates HOAS descriptions via `H.elab` + `E.eval []`; throws on inputs that are neither._

```
evalDesc : Hoas | Val -> Val
```

## `foldDesc`

_foldDesc: catamorphism over description structure — recursively decomposes a description into its ret/arg/rec/pi/plus shape and invokes the matching case in `cases` with the materialised sub-values._

```
foldDesc : { ret? ; arg? ; rec? ; pi? ; plus? ; default? } -> Hoas | Val -> R
```

## `foldDescM`

_foldDescM: monadic catamorphism over description structure — recurses through ret/arg/rec/pi/plus and binds each sub-`Computation R` before invoking the matching handler, so handlers receive already-bound `R` carriers and the combinator owns the threading._

```
foldDescM : { ret? ; arg? ; rec? ; pi? ; plus? ; default? } -> Hoas | Val -> Computation R
```

Monadic dual of `foldDesc`. Each handler returns a
`Computation R`; recursed sub-computations are sequenced via
`fx.kernel.bind` before the handler runs, so a handler
observes bound `R` values (not raw computations).

Per-summand handler shapes:

- `ret`   : `{ view; j }` — no sub-recursion.
- `arg`   : `{ view; sTy; body; sample }` where
             `body : arg -> Computation R` defers recursion at
             the body's parameter and `sample : R` is the bound
             result of recursing on the placeholder-instantiated
             body (mirrors the pure `foldDesc` arg convention).
- `rec`   : `{ view; j; sub }` with `sub : R`.
- `pi`    : `{ view; sTy; fn; sub }` with `sub : R` (the
             selector `fn` stays raw — it's a `Val`, not a
             description).
- `plus`  : `{ view; left; right }` with both bound.

The `default` handler is used when a per-summand handler is
absent; default-of-defaults is `_: K.pure null`.

Use this fold to drive `checkD`/`inferD`-shaped walkers where
each kernel-CHECK sub-delegation lives inside a
`Computation Tm` (typeError handler, `bindP`-style position
wrapping). The combinator preserves the pure-bind discipline:
recursing at a summand whose sub-walk resolves to `K.pure …`
does not install a handler.

## `foldDescWithPath`

_foldDescWithPath: monadic catamorphism that threads a `path` of `fx.diag.positions` segments AND uses `bindP` at each descent so emitted typeErrors auto-wrap under the structural position before re-raising._

```
foldDescWithPath : [Position] -> { ret? ; arg? ; rec? ; pi? ; plus? ; default? } -> Hoas | Val -> Computation R
```

Variant of `foldDescM` with two-pronged structural blame:
every descent installs a `fx.tc.check.bindP` handler under
the descent's position, and the current `path` is exposed to
handlers as data. The blame alphabet at each descent:

  arg.T   → `P.DArgBody`
  rec.D   → `P.DRecTail`
  pi.T    → `P.DPiBody`
  plus.L  → `P.DPlusL`
  plus.R  → `P.DPlusR`

Because the descent uses `bindP`, a sub-handler that emits
`typeError` produces an error tree whose outermost edge is
the descent position, with the original error nested under
it. Nested descents stack — a typeError emitted at the leaf
of a plus(rec(ret)) descent surfaces with the edge chain
`[DPlusL, DRecTail]` outermost-first, matching the kernel's
existing positional-blame convention. Handlers that prefer
explicit position wrapping can use the `path` argument and
`D.nestUnder` directly; both routes compose because the
alphabet is identical.

Each handler receives the *current* `path` (the chain leading
to its node, not yet extended by its own descent) and, for
non-leaf summands, helper extenders matching what the
descent will install:

- `ret`   : `{ view; path; j }`.
- `arg`   : `{ view; path; sTy; body; sample; bodyPath }` —
             `bodyPath = path ++ [DArgBody]`.
- `rec`   : `{ view; path; j; sub; subPath }` —
             `subPath = path ++ [DRecTail]`.
- `pi`    : `{ view; path; sTy; fn; sub; subPath }` —
             `subPath = path ++ [DPiBody]`.
- `plus`  : `{ view; path; left; right; leftPath; rightPath }`.

Pass `[]` as the root path for a top-level walk. Nested
callers pass the outer chain so positions compose
end-to-end.

## `isArg`

_isArg: predicate — `true` iff the description's outer constructor is `descArg`._

```
isArg : Hoas | Val -> Bool
```

## `isPi`

_isPi: predicate — `true` iff the description's outer constructor is `descPi`._

```
isPi : Hoas | Val -> Bool
```

## `isPlus`

_isPlus: predicate — `true` iff the description's outer constructor is `plusI` (binary sum)._

```
isPlus : Hoas | Val -> Bool
```

## `isRec`

_isRec: predicate — `true` iff the description's outer constructor is `descRec`._

```
isRec : Hoas | Val -> Bool
```

## `isRet`

_isRet: predicate — `true` iff the description's outer constructor is `descRet`._

```
isRet : Hoas | Val -> Bool
```

## `mapDesc`

_mapDesc: structurally rewrite each layer of a description via per-shape mapper functions, then reconstruct using the canonical encoder chain — the result is conv-equivalent to the original when mappers are identities._

```
mapDesc : { ret? ; arg? ; rec? ; pi? ; plus? } -> Hoas | Val -> Val
```

## `paraDM`

_paraDM: monadic paramorphism over description structure — each handler additionally receives the original sub-description `Val` alongside the bound recursed result, enabling certificate-aware fast paths and reflective elaborators._

```
paraDM : { ret? ; arg? ; rec? ; pi? ; plus? ; default? } -> Hoas | Val -> Computation R
```

Paramorphic variant of `foldDescM`. Where `foldDescM` exposes
only the recursed `R` carrier at each sub-position, `paraDM`
also exposes the raw sub-description `Val` — required by
callers that inspect the kernel-level description shape
without paying for a monadic descent (certificate consultation,
ornament-section selection, reflection).

Per-summand handler shapes:

- `ret`   : `{ view; j }`.
- `arg`   : `{ view; sTy; body; bodyDesc; sample; sampleDesc }`
             — `body : arg -> Computation R` and the
             parallel `bodyDesc : arg -> Val` return
             the sub-description without recursing. `sample`
             and `sampleDesc` are the bound result and raw
             `Val` at the placeholder respectively.
- `rec`   : `{ view; j; sub; subDesc }` — `subDesc : Val` is
             the original sub-description `view.sub`.
- `pi`    : `{ view; sTy; fn; sub; subDesc }`.
- `plus`  : `{ view; left; right; leftDesc; rightDesc }`.

`default` and identity-on-failure semantics match `foldDescM`.

## `shape`

_shape: tagged-record skeleton of a description — returns `{ kind = "ret" | "arg" | "rec" | "pi" | "plus"; ...payload }` with only the shape-relevant fields; payload depends on `kind`._

```
shape : Hoas | Val -> { kind : String; ... }
```