Feature contract: project — named record projection#

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

(project Family field value) has exactly a family identifier, field identifier, and scrutinee term. Prefix syntax has no precedence ambiguity.

2. Scope and binding rules, including generated names#

The form binds no user name. Elaboration creates a motive binder and branch binders represented by de Bruijn indices. Expanded rendering alpha-renames them to fresh _alpha_expanded_N identifiers disjoint from every referenced global.

3. Type and quantity requirements#

Family must be a checked single-constructor family, value must have that family type, and field must be declared. The current draft requires an expected projection result type. Consuming a linear record once is accepted; using it twice or capturing it in an unrestricted closure is rejected by the kernel quantity checker.

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

Projection evaluates its scrutinee once through the ordinary eliminator. It adds no effect or partiality and retains the scrutinee's resource use.

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

Projection becomes one REliminate with a constant result motive and the selected constructor branch binder as its body. Recursive fields and induction hypothesis binders participate in the kernel-provided branch layout.

6. Representation and target support, where relevant#

The existing eliminator erasure and x86-64 path own representation and native execution. No record-specific runtime object exists.

7. Error codes and primary/secondary origins#

ALPHA-RECORD-PROJECTION-NEEDS-TYPE points at the field; ALPHA-RECORD-UNKNOWN-FIELD points at the field identifier; ALPHA-RECORD-NOT-SINGLE-CONSTRUCTOR points at the form; and ALPHA-RECORD-PROJECTION-FAMILY points at the scrutinee. Resource violations use ALPHA-QUANTITY-VIOLATION with the kernel-owned source origin.

8. Formatting and migration rules#

Normal formatting retains project and comments. Expanded inspection prints its explicit eliminate with fresh branch binders, reparses and rechecks the candidate, and requires identical closure interface digests.

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

tests/language/records/Projection.alpha proves exact ordinary-core lowering and negative field/type cases. ConsumingProjection.alpha, the quantity cases under source-negative/, and bootstrap surface tests cover linear consumption, duplicate use, affine branch use, and unrestricted capture.

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

project is draft alpha-2027 syntax over old REliminate. The expanded form uses existing source and core syntax; ALRI v4 and interface v5 do not change.