Feature contract: record — named record construction#

1. Lexical and grammar rules, including precedence and termination#

(record Family (field = value)+) is a parenthesized prefix form with at least one assignment. Family and every field are identifiers. Each assignment is grouped and contains one = and one value term. The outer close terminates the form; malformed or unterminated assignments produce ALPHA-PARSE-RECORD.

2. Scope and binding rules, including generated names#

Construction binds and generates no source names. Values resolve in the enclosing scope. Field order in source is irrelevant; declaration order owns the constructor argument order.

3. Type and quantity requirements#

The family must have exactly one checked constructor. Every declared value or recursive field appears exactly once. Values are checked progressively against the constructor telescope, so dependent later fields see earlier values. Parameterized records infer parameters from the expected family type.

4. Effects, totality, and evaluation-order rules#

Fields are checked in declaration order and construction adds no effect or partiality. Field quantities are the constructor's declared quantities and are enforced by the kernel.

5. Elaboration into existing core or a specifically versioned new core extension#

The elaborator emits RConstructorApplication Family Constructor with inferred parameters followed by fields in declaration order. It adds no core form.

6. Representation and target support, where relevant#

Representation and x86-64 lowering are exactly those of the existing family constructor. ALRI v4 and checked-interface v5 are unchanged.

7. Error codes and primary/secondary origins#

ALPHA-RECORD-NOT-SINGLE-CONSTRUCTOR, ALPHA-RECORD-NEEDS-TYPE, ALPHA-RECORD-EXPECTED-FAMILY, ALPHA-RECORD-MISSING-FIELD, ALPHA-RECORD-DUPLICATE-FIELD, and ALPHA-RECORD-UNKNOWN-FIELD are stable. Duplicate and unknown errors point at the offending assignment; missing-field errors point at the record form.

8. Formatting and migration rules#

Canonical formatting keeps named assignments and preserves their comments and tokens. Expanded inspection prints the checked constructor application and proves semantic-interface equality by an overlay re-check. alpha-2026 rejects the form; no automatic migration rewrites it into that edition.

9. Positive, negative, execution, and edge-case tests#

tests/language/records/{SourceForms,Construction,Parameters}.alpha cover parsing, order, dependencies, parameter inference, failures, and exact core correspondence. tests/language/records/source-negative/ and the bootstrap surface tests cover the stable diagnostics and spans.

10. Compatibility with the old edition, serialized forms, and cache keys#

The form is new only in alpha-2027. Its elaborated core is accepted by the old core and serializers, so no ALRI or interface successor is required. Edition is already part of the cache key.