Value

Two-way conversion between HOAS values and Nix constructor-records, plus generic structural traversal. The type argument accepts either an HOAS type directly or a datatype-output record carrying .T; everything else is normalised by typeOf internally.

view is the HOAS-or-Nix → tagged-record direction: record/variant datatypes return { _con = "name"; …fields }, primitives flatten to their native Nix form. The function is idempotent on values already in HOAS form. review is the inverse, kernel-elaborating a Nix value back to HOAS via Elab.elaborateValue. toConstructorRecord and fromConstructorRecord are intent-named aliases preferred in datatype-generic code.

fold consumes a { <ctor> = Fields -> R; default? } map and dispatches on _con; recAt fields are recursively folded before being passed in, all other fields appear raw. Missing constructors fall through to cases.default constructor or throw. mapChildren rewrites a single layer: each recAt field is replaced by childMapper field child; non-recursive fields pass through unchanged. The result is normalised by view so it round-trips with review.

fold

fold: structural fold over a generated datatype value — dispatches on the constructor's name in cases, recursing into recAt fields before invoking the case function with the record of materialised fields.

fold : Hoas -> { <ctor> = Fields -> R; default? : Constructor -> Fields -> R; } -> NixVal -> R

Each case in cases receives a record of materialised fields keyed by field name; recAt fields have already been folded recursively, all other fields appear as raw Nix values. Missing constructors fall through to cases.default constructor if present, else throw "missing case '<name>'".

Implementation note: walks via view + constructorByName, so the input must be either a constructor-record or a value elaborable via review. Non-attrset value views (e.g., raw Nat) bypass this function — caller folds over the primitive directly.

fromConstructorRecord

fromConstructorRecord: alias of review — the datatype-generic name for the record-to-value direction; preferred when expressing intent over generated datatypes.

fromConstructorRecord : Hoas | { T : Hoas; ... } -> NixVal -> Hoas

mapChildren

mapChildren: rewrite a single layer of a generated datatype — for each recAt field, apply childMapper field child; non-recursive fields pass through unchanged. The result is view-normalised so it round-trips with review.

mapChildren : Hoas -> (Field -> NixVal -> NixVal) -> NixVal -> NixVal

review

review: Nix-value → HOAS-value — friendly alias of Elab.elaborateValue taking the type either as Hoas directly or via a .T field (datatype outputs); inverse of view.

review : Hoas | { T : Hoas; ... } -> NixVal -> Hoas

toConstructorRecord

toConstructorRecord: alias of view — the datatype-generic name for the value-to-record direction; preferred when expressing intent over generated datatypes.

toConstructorRecord : Hoas | { T : Hoas; ... } -> Hoas | NixVal -> NixVal

view

view: HOAS-value or Nix-value → Nix constructor-record — kernel-elaborates if given a Nix value, then Elab.extracts back to a tagged record (_con for record/variant datatypes, primitive for leaf types).

view : Hoas | { T : Hoas; ... } -> Hoas | NixVal -> NixVal

Idempotent on the HOAS form: when value is already an HOAS tree (_htag present), it skips re-elaboration. Otherwise round-trips through review to produce an HOAS value, then evaluates and extracts.

Returns a constructor-record { _con = "name"; ...fields } for record/variant datatypes. Primitive values (Nat, String, ...) flatten to their native Nix form. Cross-ref: fromConstructorRecord is the alias name used in the datatype-generic API surface.