# Derive


Generic, codegen-friendly summaries of a datatype's shape.
Each helper consumes a `DataSpec` (or pre-normalised meta) and
produces a pure-data record that downstream tooling — schema
validators, doc renderers, codegen, dependency analysers —
can consume without re-walking the kernel HOAS.

`typeDescriptor` projects an arbitrary HOAS or `Val` type to
`{ kind; … }` with a finite tag set covering primitives
(`nat`/`bool`/`int`/`string`/`float`/`attrs`/`path`/`function`/`any`/`unit`/`universe`),
algebraic forms (`list { elem }`, `sum { left; right }`,
`datatype { name; args? }`), recursive sites (`recursive`),
and unknown fallthrough (`hoas { tag }`).

`deriveDescriptor` is the base artefact: name, constructors,
per-field records with kind / index / level / role / source /
proof / recursive-index / branch-index / dependent-type /
type-descriptor. `deriveSchema` projects to
JSON-Schema-flavoured `{ title; oneOf }`. `deriveDocs`
re-shapes for Markdown / HTML rendering. `deriveFold` produces
the fold-skeleton record for code generators.

`deriveDeps` walks a constructor record, emitting a
`{ nodes; edges }` graph that records constructor descents
(`recAt` recursion sites), role-tagged dependency fields
(matched against a fixed role policy), and proof-bearing
fields. The output is consumable by the generic graph
renderer and by build-time dependency analysers.

## `deriveDeps`

_deriveDeps: build a node-and-edge dependency graph from a value — walks each constructor record, emitting nodes for constructors and edges for `recAt` recursion sites, role-tagged dependency fields, and proof-bearing fields._

```
deriveDeps : DataSpec -> NixVal -> { datatype, root, rootPath, indexed, index, nodes, edges }
```

Traversal seeds at path `\"$\"` and recurses into each `recAt`
field, accumulating constructor nodes and per-field edges.
Emitted edge kinds:

- `recAt` field on a constructor: edge from parent to child
  constructor, carrying `field`, `role`, `source`, and the
  resolved child type.
- Dependency-role field (matching the role-policy predicate):
  edge to a referenced datatype.
- Proof-bearing field (`proof = true`): edge tagging the
  unresolved obligation.

The returned `nodes` / `edges` shape is consumable by the
generic graph renderer and by build-time dependency analysers.

## `deriveDescriptor`

_deriveDescriptor: produce a full structured descriptor of a datatype — name, constructors, fields with kinds/types/roles, and source provenance. The base artefact other `derive*` helpers consume._

```
deriveDescriptor : DataSpec -> { name : String; constructors : [ConstructorDescriptor]; ... }
```

## `deriveDocs`

_deriveDocs: produce a documentation-friendly descriptor — same `name` and `constructors` as `deriveDescriptor` plus a `heading` field for use in Markdown/HTML rendering._

```
deriveDocs : DataSpec -> { heading : String; name : String; constructors : [...] }
```

## `deriveFold`

_deriveFold: produce a fold-skeleton descriptor — `{ datatype; cases = [{ name; fields = [{ name; kind; type; }] }] }`; consumed by code generators emitting per-datatype fold scaffolds._

```
deriveFold : DataSpec -> { datatype : String; cases : [Object] }
```

## `deriveSchema`

_deriveSchema: produce a JSON-Schema-flavoured `{ title, oneOf : [ConstructorSchema] }` from a datatype — each constructor schema records its name, field name+kind+type, and metadata flags (target index, proof, etc.)._

```
deriveSchema : DataSpec -> { title : String; oneOf : [Object] }
```

## `typeDescriptor`

_typeDescriptor: convert a kernel type (HOAS or `Val`) into a structured descriptor record — `{ kind; name?; constructors?; ... }` summarising the shape; used downstream by schema, docs, and dependency derivations._

```
typeDescriptor : Hoas | Val | null -> { kind : String; ... }
```