Datatype

Operates on the _dtypeMeta attrset attached to every datatype produced by H.datatype / H.datatypeI / H.datatypeP, and on H.app-spines whose head carries _dtypeMeta (instantiated polymorphic datatypes). datatypeInfo is the canonical entry: it normalises a raw meta or applies meta.instantiate to the spine args before returning a fully-defaulted record (indexed, params, paramArgs, indexTy, plus both constructors and the legacy cons alias).

Lookup helpers stay close to caller intent: constructors, fields, constructorByName, and constructorByIx accept either pre-normalised meta or a raw DataSpec. Mismatched names and out-of-range indices throw with descriptive messages; nothing fails silently.

Field-level resolution threads prev — the record of previously-materialised dependent-field values — so fieldType field prev returns the kernel HOAS type for both concrete fields (field.type) and dependent fields (field.typeFn prev). targetIndex con prev resolves a constructor's target index in the datatype's index type the same way. fieldRole exposes the optional role annotation used by generic derivations to distinguish payload from proof-bearing fields.

constructorByIx

constructorByIx: lookup a constructor by zero-based declaration-order index; throws on out-of-range or non-integer index.

constructorByIx : Meta | DataSpec -> Int -> Constructor

constructorByName

constructorByName: lookup a constructor by name in a datatype's meta/DataSpec; throws on unknown name with a descriptive message.

constructorByName : Meta | DataSpec -> String -> Constructor

constructors

constructors: extract the constructor list from a meta or DataSpec — accepts either a pre-normalised meta with constructors or a raw DataSpec, calling datatypeInfo for the latter.

constructors : Meta | DataSpec -> [Constructor]

datatypeInfo

datatypeInfo: produce normalised metadata from either a DataSpec (record with _dtypeMeta) or an H.app spine whose head is a polymorphic datatype; for polymorphic heads, applies meta.instantiate to the spine args.

datatypeInfo : DataSpec | Hoas -> Meta

fieldRole

fieldRole: extract the role annotation from a field, or null if unset. Used by generic derivations to distinguish e.g. proof-bearing fields from ordinary payload.

fieldRole : Field -> String | null

fieldType

fieldType: resolve a field's HOAS type — prefers field.typeFn prev (dependent fields) over field.type (concrete); throws if neither slot is filled.

fieldType : Field -> AttrSet -> Hoas

fields

fields: extract the field list from a constructor record; defaults to [] for constructors with no fields slot.

fields : Constructor -> [Field]

instantiate

instantiate: apply parameter arguments to a polymorphic datatype DataSpec, returning the normalised meta for that instantiation; throws for non-polymorphic datatypes given non-empty paramArgs.

instantiate : DataSpec -> [Hoas] -> Meta

isDatatype

isDatatype: predicate identifying values that carry _dtypeMeta directly, or app-spines whose head carries _dtypeMeta (instantiated polymorphic datatypes).

isDatatype : Any -> Bool

normalizeMetadata

normalizeMetadata: canonicalise a raw _dtypeMeta attrset — requires constructors, defaults indexed/params/paramArgs/indexTy, and pre-fills every field with level/eq/proof/type/typeFn/S/SFn/idxFn/branchIdxFn/role/source slots.

normalizeMetadata : Meta -> Meta

targetIndex

targetIndex: compute a constructor's target index in the datatype's index type — applies con.targetIdx prev where prev is the materialised previous-field record; throws if no targetIdx function is present.

targetIndex : Constructor -> AttrSet -> Hoas