# 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.extract`s 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.