# 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
```