Elaborate

Bridges the fx.types layer to the kernel's term representation via the HOAS combinator layer. Provides the Nix ↔ kernel boundary.

Spec reference: kernel-mvp-research.md §3.

Type Elaboration

• elaborateType : FxType → Hoas — convert an fx.types type descriptor to an HOAS tree. Dispatches on: (1) _kernel annotation, (2) structural fields (Pi: domain/codomain, Sigma: fstType/sndFamily), (3) name convention (Bool, Nat, String, Int, Float, ...). Dependent Pi/Sigma require explicit _kernel annotation.

Value Elaboration

• elaborateValue : Hoas → NixVal → Hoas — convert a Nix value to an HOAS term tree given its HOAS type. Bool→true/false, Int→natLit, List→cons chain, Sum→inl/inr, Sigma→pair. Trampolined for large lists.

Value Extraction

• extract : Hoas → Val → NixValue — reverse of elaborateValue. Converts kernel values back to Nix values. VZero→0, VSucc^n→n, VCons chain→list, VInl/VInr→tagged union. Pi extraction wraps the VLam as a Nix function with boundary conversion. Opaque types (Attrs, Path, Function, Any) throw — kernel discards payloads.
• extractInner : Hoas → Val → Val → NixValue — three-argument extraction with kernel type value threading. Supports dependent Pi/Sigma via closure instantiation instead of sentinel tests.
• reifyType : Val → Hoas — converts a kernel type value back to HOAS. Fallback for when HOAS body application fails (dependent types). Loses sugar (VSigma→sigma, not record).

Decision Procedure

• decide : Hoas → NixVal → Bool — returns true iff elaboration and kernel type-checking both succeed. Uses tryEval for safety.
• decideType : FxType → NixVal → Bool — elaborate type then decide.

Full Pipeline

• verifyAndExtract : Hoas → Hoas → NixValue — type-check an HOAS implementation against an HOAS type, evaluate, extract to Nix value. Throws on type error.