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; ... }