Row-typed records

ral records are open-row-polymorphic maps with scoped-label typing (Leijen 2005). [host: String, port: Int] has type [host: String, port: Int | ρ], where the tail variable ρ stands for unknown further fields:

• Field selection unifies the target with [label: α | ρ] and returns α.
• Label mismatch permutes labels past each other into a shared fresh tail (the Rémy 1989 rewrite).
• Open rows compose. A block { |opts| ... } accepts [host: String, port: Int | ρ] and adds or overrides fields without knowing the tail, so record-passing composes.

Duplicate labels are permitted; selection takes the first. Several consequences follow:

• A spread prepends and thus shadows. [...$base, port: 9090] over $base : [host: String | ρ] infers [port: Int, host: String | ρ].
• No restriction operator (Pre / Abs) is needed. The rewrite already preserves the relative order of same-label entries, so shadowing is coherent.
• Records and tags draw on two label alphabets — backtick-prefixed for variants and tag-keyed records, bare for ordinary records — and the two never unify.
• Structural equality of closed records is order-insensitive: [a: 1, b: 2] == [b: 2, a: 1].

A case closes a variant row, and the syntax is what lets it. The arms are written out at the case, so the label set is known when the rule fires: the scrutinee’s row unifies with exactly that set, and coverage is decided there, always (case-is-syntax-try-is-not). An open scrutinee row absorbs an arm label it has not been seen to construct — let v = `ok 5 then a case with an `err arm typechecks — which is principal row inference and not a gap in the proof: the row records what the program has shown, and the case is one more such showing.

Scoped labels and spread shadowing are how ral expresses optionality and defaults at the level of data rather than argument lists — see optionality-via-variants and fixed-arity. Rows type data only, never effects — that refusal is argued against the literature in rows-and-handlers.

Realised in type-inference (row unification by the Rémy rewrite).

Cite: RATIONALE §“Structured values cross once”; docs/SPEC.md §4, §4.5.