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.

Pure (K.pure …) sub-walks short-circuit through bindP's isPure fast path — no handler install, no overhead.

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; ... }