Constructors

Type constructors: Record, RecordOpen, ListOf, Maybe, Either, Variant.

Either

Either: tagged sum type constructor; Either L R accepts { _tag = "Left"; value : L } or { _tag = "Right"; value : R }.

Either : Type -> Type -> Type

Tagged union of two types. Accepts { _tag = "Left"; value = a; } or { _tag = "Right"; value = b; }.

ListOf

ListOf: homogeneous list type constructor; ListOf T checks every element has type T, blames per-index, never short-circuits — handler picks error policy.

ListOf : Type -> Type

Homogeneous list type. ListOf Type checks that all elements have the given type.

Custom verifier sends per-element typeCheck effects with indexed context strings (e.g. List[Int][2]) for blame tracking. Unlike Sigma, elements are independent — no short-circuit. All elements are checked; the handler decides error policy (strict aborts on first, collecting gathers all).

Maybe

Maybe: option type constructor; Maybe T accepts null or any value of type T; kernel precision and sufficiency inherit from the inner type.

Maybe : Type -> Type

Option type. Maybe Type accepts null or a value of Type.

Record

Record: closed record type constructor; Record { f = T; ... } checks that values carry exactly the declared fields with matching types and rejects extras.

Record : { <field> = Type; ... } -> Type

Closed record type constructor. Takes a schema { field = Type; ... } and checks that a value has exactly the declared fields with correct types. Unknown fields are rejected — for open semantics use RecordOpen.

Verify is per-field and emits one typeCheck effect per blamed field, threading a Field name Position so handlers can recover the structural path.

RecordOpen

RecordOpen: open-record type constructor; like Record but undeclared fields are accepted untouched, useful for records carrying optional metadata slots.

RecordOpen : { <field> = Type; ... } -> Type

Open record type constructor. Like Record, but undeclared fields are permitted (and ignored by kernel and verify). Use for types whose values carry intentional metadata slots beyond the declared schema — e.g. build steps with optional tools / env / when annotations.

The kernel datatype tags openExtras = true in _dtypeMeta so downstream type-directed walks know to allow them.

Variant

Variant: discriminated-union type constructor; Variant { tag = T; ... } accepts { _tag = name; value } checked against the named branch.

Variant : { <tag> = Type; ... } -> Type

Discriminated union. Takes { tag = Type; ... } schema. Accepts { _tag = "tag"; value = ...; } where value has the corresponding type.