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

