Check

The single polymorphic fold over the full HOAS type algebra, parameterised by an Algebra A. Two canonical algebras live alongside it: unitAlg returns null at every node and is used for validation (the walker emits typeCheck effects on failure); hoasAlg constructs the corresponding HOAS term at every node and is used for elaboration. Validation and elaboration are not two functors — they are one fold instantiated at two carriers.

deriveCheck and deriveElaborate thread unitAlg / hoasAlg respectively. Both accept (ty, path, value) and return a Computation A; the walker owns shape inspection, _htag dispatch, fx.kernel effect emissions, path threading, and the dependent-Σ snd-type derivation via an internal strict-handler trampoline on fst. Algebras own per-shape success-case construction and the field-walker (so unitAlg matches the legacy f.type-only traversal while hoasAlg threads prev through fieldType for dependent-field resolution).

checkWithGuard composes deriveCheck with a refinement predicate: shape-check via the unit walker first, predicate second (the two cannot run in parallel — the predicate's domain is exactly the values that pass shape). When the eventual Σ-with-Decide-snd encoding lands, this special case collapses into deriveCheck over Σ-types and the helper deletes.

Failure reasons carry one of shape-mismatch, missing-field, extra-field, predicate-failed, or deferred-pi, routed by handlers under fx.effects.typecheck.*.

checkWithGuard

checkWithGuard: refinement-predicate-aware variant of deriveCheck — runs shape check first via unitAlg, then composes the type's refinement predicate when present; required while refined types are encoded outside the canonical Σ-with-Decide-snd form.

checkWithGuard : Type -> Path -> Value -> Computation Null

deriveCheck

deriveCheck: canonical typed walker over the HOAS algebra threading unitAlg — emits fx.effects.typecheck failures with structured reason (shape-mismatch, missing-field, extra-field, predicate-failed, deferred-pi) and path (a fx.diag.positions chain).

deriveCheck : Type -> Path -> Value -> Computation Null

deriveElaborate

deriveElaborate: canonical typed walker over the HOAS algebra threading hoasAlg — reconstructs the corresponding HOAS term at every successfully-checked node; shares path threading and dispatch with deriveCheck.

deriveElaborate : Type -> Path -> Value -> Computation Hoas