// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2024-2026 hyperpolymath (Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>)
= Row Polymorphism: Complete Formalization

*Document Version*: 1.0 *Last Updated*: 2024 *Status*: Theoretical
framework complete; implementation verification pending
`++[++IMPL-DEP: type-checker++]++`

== Abstract

This document provides a complete formalization of row polymorphism in
AffineScript, including the syntax, typing rules, unification algorithm,
and soundness proofs. Row polymorphism enables extensible records and
variants with full type inference, following the tradition of Rémy
(1989) and Wand (1991), extended with AffineScript’s effects,
quantities, and ownership.

== 1. Introduction

Row polymorphism allows polymorphism over record and variant "`shapes`"
without requiring explicit subtyping. A function can operate on any
record containing at least certain fields, regardless of what other
fields exist:

[source,affinescript]
----
fn get_name[ρ](r: {name: String, ..ρ}) -> String {
    r.name
}
----

This document formalizes: 1. Row types and their kinding 2. Row
unification algorithm 3. Type soundness with rows 4. Coherence of row
operations 5. Principal types with row polymorphism

== 2. Syntax of Rows

=== 2.1 Row Types

....
ρ ::=
    | ∅                           -- Empty row
    | (l : τ | ρ)                 -- Row extension
    | α                           -- Row variable

Record types:
{ρ}                               -- Record with row ρ
{l₁: τ₁, ..., lₙ: τₙ}             -- Sugar for {(l₁:τ₁|...(lₙ:τₙ|∅)...)}
{l₁: τ₁, ..., lₙ: τₙ | α}         -- Open record (extensible)

Variant types:
⟨ρ⟩                               -- Variant with row ρ
⟨l₁: τ₁ | ... | lₙ: τₙ⟩           -- Closed variant
⟨l₁: τ₁ | ... | lₙ: τₙ | α⟩       -- Open variant (extensible)
....

=== 2.2 Labels

Labels l are drawn from a countably infinite set L. We assume a total
ordering on labels for canonical row representations.

=== 2.3 Row Equivalence

Rows are equivalent up to permutation (but not duplication):

*Definition 2.1 (Row Equivalence)*: ρ₁ ≡ ρ₂ iff they contain the same
labels with the same types, differing only in order.

Formally, define the flattening function:

....
flatten(∅) = {}
flatten((l : τ | ρ)) = {l ↦ τ} ∪ flatten(ρ)    (if l ∉ dom(flatten(ρ)))
flatten(α) = {α}                               (row variable)
....

Then ρ₁ ≡ ρ₂ iff flatten(ρ₁) = flatten(ρ₂).

*Axioms*:

....
(l₁ : τ₁ | (l₂ : τ₂ | ρ)) ≡ (l₂ : τ₂ | (l₁ : τ₁ | ρ))    (l₁ ≠ l₂)
....

=== 2.4 Row Restriction

*Definition 2.2 (Row Restriction)*: ρ  l removes label l from row ρ:

....
∅ \ l = ∅
(l : τ | ρ) \ l = ρ
(l' : τ | ρ) \ l = (l' : τ | ρ \ l)    (l ≠ l')
α \ l = α                              (defer to unification)
....

=== 2.5 Row Concatenation

*Definition 2.3 (Row Concatenation)*: ρ₁ ⊕ ρ₂ combines rows (disjoint
labels required):

....
∅ ⊕ ρ = ρ
(l : τ | ρ₁) ⊕ ρ₂ = (l : τ | ρ₁ ⊕ ρ₂)    (l ∉ labels(ρ₂))
....

=== 2.6 Presence/Absence Types (Rémy’s Approach)

For complete type inference, we extend rows with presence/absence
annotations:

....
π ::= Pre(τ) | Abs

ρ̂ ::= ∅ | (l : π | ρ̂) | α

Pre(τ)     -- Label l is present with type τ
Abs        -- Label l is absent
....

This allows unifying records with different field sets by marking absent
fields.

== 3. Kinding

=== 3.1 Kind Structure

....
κ ::= Type | Row | ...
....

=== 3.2 Kinding Rules

*K-Empty*

....
    ────────────
    Γ ⊢ ∅ : Row
....

*K-Extend*

....
    Γ ⊢ τ : Type    Γ ⊢ ρ : Row    l ∉ labels(ρ)
    ───────────────────────────────────────────────
    Γ ⊢ (l : τ | ρ) : Row
....

*K-RowVar*

....
    α : Row ∈ Γ
    ───────────────
    Γ ⊢ α : Row
....

*K-Record*

....
    Γ ⊢ ρ : Row
    ─────────────────
    Γ ⊢ {ρ} : Type
....

*K-Variant*

....
    Γ ⊢ ρ : Row
    ─────────────────
    Γ ⊢ ⟨ρ⟩ : Type
....

=== 3.3 Lack Constraints

To express "`row ρ does not contain label l`", we use lack constraints:

....
Γ ⊢ ρ lacks l
....

*Lacks-Empty*

....
    ─────────────────
    Γ ⊢ ∅ lacks l
....

*Lacks-Extend*

....
    Γ ⊢ ρ lacks l    l ≠ l'
    ────────────────────────
    Γ ⊢ (l' : τ | ρ) lacks l
....

*Lacks-Var* (constraint on variable)

....
    α lacks l ∈ Γ
    ─────────────────
    Γ ⊢ α lacks l
....

== 4. Typing Rules

=== 4.1 Record Introduction

*Rec-Empty*

....
    ────────────────────
    Γ ⊢ {} ⇒ {∅}
....

*Rec-Extend*

....
    Γ ⊢ e : τ ! ε    Γ ⊢ r : {ρ} ! ε'    Γ ⊢ ρ lacks l
    ──────────────────────────────────────────────────────
    Γ ⊢ {l = e, ..r} ⇒ {(l : τ | ρ)} ! (ε | ε')
....

*Rec-Literal*

....
    ∀i. Γ ⊢ eᵢ ⇒ τᵢ ! εᵢ    labels distinct
    ──────────────────────────────────────────────────────────
    Γ ⊢ {l₁ = e₁, ..., lₙ = eₙ} ⇒ {l₁: τ₁, ..., lₙ: τₙ} ! (ε₁ | ... | εₙ)
....

=== 4.2 Record Elimination

*Rec-Select*

....
    Γ ⊢ e ⇒ {(l : τ | ρ)} ! ε
    ──────────────────────────
    Γ ⊢ e.l ⇒ τ ! ε
....

*Rec-Restrict*

....
    Γ ⊢ e ⇒ {(l : τ | ρ)} ! ε
    ────────────────────────────
    Γ ⊢ e \ l ⇒ {ρ} ! ε
....

*Rec-Update*

....
    Γ ⊢ e₁ ⇒ {(l : τ | ρ)} ! ε₁    Γ ⊢ e₂ ⇒ σ ! ε₂
    ─────────────────────────────────────────────────
    Γ ⊢ e₁ with {l = e₂} ⇒ {(l : σ | ρ)} ! (ε₁ | ε₂)
....

=== 4.3 Variant Introduction

*Var-Inject*

....
    Γ ⊢ e ⇒ τ ! ε    α fresh
    ──────────────────────────────────
    Γ ⊢ l(e) ⇒ ⟨l : τ | α⟩ ! ε
....

=== 4.4 Variant Elimination

*Var-Case*

....
    Γ ⊢ e ⇒ ⟨l₁: τ₁ | ... | lₙ: τₙ⟩ ! ε
    ∀i. Γ, xᵢ: τᵢ ⊢ eᵢ ⇐ σ ! ε'
    ──────────────────────────────────────────────────────────────
    Γ ⊢ case e { l₁(x₁) → e₁ | ... | lₙ(xₙ) → eₙ } ⇒ σ ! (ε | ε')
....

*Var-Case-Open* (with default)

....
    Γ ⊢ e ⇒ ⟨l₁: τ₁ | ... | lₙ: τₙ | α⟩ ! ε
    ∀i. Γ, xᵢ: τᵢ ⊢ eᵢ ⇐ σ ! ε'
    Γ, y: ⟨α⟩ ⊢ e_default ⇐ σ ! ε'
    ──────────────────────────────────────────────────────────────────────
    Γ ⊢ case e { l₁(x₁) → e₁ | ... | lₙ(xₙ) → eₙ | y → e_default } ⇒ σ ! (ε | ε')
....

=== 4.5 Row Polymorphism

*Row-Gen*

....
    Γ, α:Row ⊢ e ⇒ τ ! ε    α ∉ FV(Γ)
    ─────────────────────────────────────
    Γ ⊢ e ⇒ ∀α:Row. τ ! ε
....

*Row-Inst*

....
    Γ ⊢ e ⇒ ∀α:Row. τ ! ε    Γ ⊢ ρ : Row
    ───────────────────────────────────────
    Γ ⊢ e ⇒ τ[ρ/α] ! ε
....

== 5. Unification

=== 5.1 Unification Problem

Given two types τ₁ and τ₂, find a substitution θ such that θ(τ₁) =
θ(τ₂).

=== 5.2 Row Unification Algorithm

Row unification extends standard unification with special handling for
rows:

[source,ocaml]
----
type unify_result =
  | Success of substitution
  | Failure of string

let rec unify_row (ρ₁ : row) (ρ₂ : row) : unify_result =
  match (ρ₁, ρ₂) with
  (* Both empty *)
  | (Empty, Empty) ->
      Success []

  (* Variable cases *)
  | (RowVar α, ρ) | (ρ, RowVar α) ->
      if occurs α ρ then
        Failure "occurs check"
      else
        Success [α ↦ ρ]

  (* Both extensions with same head label *)
  | (Extend (l, τ₁, ρ₁'), Extend (l', τ₂, ρ₂')) when l = l' ->
      let* θ₁ = unify τ₁ τ₂ in
      let* θ₂ = unify_row (apply θ₁ ρ₁') (apply θ₁ ρ₂') in
      Success (compose θ₂ θ₁)

  (* Extensions with different head labels - row rewriting *)
  | (Extend (l₁, τ₁, ρ₁'), Extend (l₂, τ₂, ρ₂')) when l₁ ≠ l₂ ->
      (* Rewrite: (l₁:τ₁|ρ₁') = (l₂:τ₂|ρ₂')
         becomes: ρ₁' = (l₂:τ₂|ρ₃) and ρ₂' = (l₁:τ₁|ρ₃) for fresh ρ₃ *)
      let ρ₃ = fresh_row_var () in
      let* θ₁ = unify_row ρ₁' (Extend (l₂, τ₂, ρ₃)) in
      let* θ₂ = unify_row (apply θ₁ ρ₂') (apply θ₁ (Extend (l₁, τ₁, ρ₃))) in
      Success (compose θ₂ θ₁)

  (* Empty vs extension - failure *)
  | (Empty, Extend _) | (Extend _, Empty) ->
      Failure "row mismatch"
----

=== 5.3 Occurs Check for Rows

[source,ocaml]
----
let rec row_occurs (α : row_var) (ρ : row) : bool =
  match ρ with
  | Empty -> false
  | RowVar β -> α = β
  | Extend (_, τ, ρ') -> type_occurs α τ || row_occurs α ρ'
----

=== 5.4 Correctness of Row Unification

*Theorem 5.1 (Soundness of Row Unification)*: If
`unify++_++row(ρ₁, ρ₂) = Success θ`, then `θ(ρ₁) ≡ θ(ρ₂)`.

*Proof*: By induction on the structure of the unification algorithm.

_Case RowVar_: θ = ++[++α ↦ ρ++]++, so θ(α) = ρ = θ(ρ). ✓

_Case Same-Head_: By IH, θ₁(τ₁) = θ₁(τ₂) and θ₂(θ₁(ρ₁’)) = θ₂(θ₁(ρ₂’)).
Combined substitution preserves equality. ✓

_Case Different-Head_: By IH and the rewriting equations, both sides
become equivalent. ✓

∎

*Theorem 5.2 (Completeness of Row Unification)*: If there exists θ such
that θ(ρ₁) ≡ θ(ρ₂), then `unify++_++row(ρ₁, ρ₂) = Success θ'` for some
θ’ more general than θ.

*Proof*: By induction, showing the algorithm finds the most general
unifier. ∎

*Theorem 5.3 (Termination of Row Unification)*: Row unification
terminates on all inputs.

*Proof*: Define a measure M(ρ) = (size(ρ), vars(ρ)). Each recursive call
strictly decreases this measure (lexicographically). ∎

== 6. Type Inference with Rows

=== 6.1 Constraint Generation

During type inference, generate constraints including row constraints:

....
C ::= τ = σ | ρ = ρ' | ρ lacks l | ...
....

=== 6.2 Principal Types

*Theorem 6.1 (Principal Types)*: For any expression e and context Γ, if
e is typeable then there exists a principal type scheme σ such that all
other types are instances of σ.

*Proof*: The unification algorithm computes most general unifiers, and
generalization produces principal type schemes. ∎

=== 6.3 Let-Polymorphism with Rows

....
    Γ ⊢ e₁ ⇒ τ₁ ! ε    σ = gen(Γ, τ₁)    Γ, x:σ ⊢ e₂ ⇒ τ₂ ! ε'
    ─────────────────────────────────────────────────────────────
    Γ ⊢ let x = e₁ in e₂ ⇒ τ₂ ! (ε | ε')
....

Where `gen(Γ, τ) = ∀ᾱ:κ̄. τ` for ᾱ = FTV(τ)  FTV(Γ).

== 7. Soundness

=== 7.1 Progress with Rows

*Theorem 7.1 (Progress)*: If `· ⊢ e : τ` where τ involves row types,
then either e is a value or e can step.

*Proof*: Extended from base progress theorem. The key cases:

_Case Record-Select_: If `· ⊢ e.l : τ` then
`· ⊢ e : ++{++(l : τ ++|++ ρ)}`. By IH, e is a value or steps. If e is a
value, by canonical forms it is a record `++{++l₁=v₁,...,lₙ=vₙ}`
containing field l. Therefore `e.l ⟶ v` where v is the value at label l.
✓

_Case Variant-Case_: Similar, using exhaustiveness from the type. ✓

∎

=== 7.2 Preservation with Rows

*Theorem 7.2 (Preservation)*: If `Γ ⊢ e : τ` and `e ⟶ e'`, then
`Γ ⊢ e' : τ`.

*Proof*: By induction on the reduction. Key cases:

_Case Record-Select_: `++{++l₁=v₁,...,l=v,...,lₙ=vₙ}.l ⟶ v`

From typing: `Γ ⊢ ++{++l₁=v₁,...,l=v,...,lₙ=vₙ} : ++{++(l : τ ++|++ ρ)}`
By inversion: `Γ ⊢ v : τ` ✓

_Case Record-Update_:
`++{++l=v₁++|++r} with ++{++l=v₂} ⟶ ++{++l=v₂++|++r}`

From typing: original type is `++{++(l : τ₁ ++|++ ρ)}`, new value has
type τ₂ Result type is `++{++(l : τ₂ ++|++ ρ)}` as required. ✓

∎

=== 7.3 Type Safety

*Corollary 7.3 (Type Safety with Rows)*: Well-typed programs with row
polymorphism do not get stuck.

== 8. Coherence

=== 8.1 Record Coherence

*Theorem 8.1 (Record Representation Independence)*: If
`Γ ⊢ e : ++{++ρ₁}` and `ρ₁ ≡ ρ₂`, then `Γ ⊢ e : ++{++ρ₂}`.

Operations on records are independent of field order.

=== 8.2 Polymorphic Coherence

*Theorem 8.2 (Coherence of Instantiation)*: For
`f : ∀α:Row. ++{++α} → τ`, all instantiations of α produce semantically
equivalent behavior.

*Proof*: Row polymorphism is parametric; the function cannot inspect the
specific row. ∎

== 9. Row Polymorphism and Effects

=== 9.1 Effect Rows

Effects use the same row machinery:

....
ε ::= ∅ | (E | ε) | ρ_eff
....

Effect rows and record/variant rows are disjoint kinds:

....
α : Row_Record
β : Row_Variant
ρ : Row_Effect
....

=== 9.2 Unified Row Kinding

....
κ_row ::= Row(sort)
sort ::= Record | Variant | Effect
....

== 10. Row Polymorphism and Ownership

=== 10.1 Owned Records

....
own {l₁: τ₁, ..., lₙ: τₙ | ρ}
....

Ownership applies to the whole record; individual fields inherit
ownership.

=== 10.2 Field Borrowing

[source,affinescript]
----
fn get_field['a, ρ](r: ref['a] {name: String, ..ρ}) -> ref['a] String {
    &r.name
}
----

The borrow of a field extends the borrow of the record.

== 11. Implementation

=== 11.1 AST Representation

From `lib/ast.ml`:

[source,ocaml]
----
type row_field = {
  rf_name : ident;
  rf_ty : type_expr;
}

type type_expr =
  | ...
  | TyRecord of row_field list * ident option  (* fields, row var *)
----

=== 11.2 Row Unification Module

`++[++IMPL-DEP: type-checker++]++`

[source,ocaml]
----
module RowUnify : sig
  type row =
    | Empty
    | Extend of string * typ * row
    | Var of int

  val unify : row -> row -> substitution result
  val rewrite : string -> row -> row * typ  (* extract field *)
  val lacks : row -> string -> bool
end
----

== 12. Examples

=== 12.1 Extensible Records

[source,affinescript]
----
fn full_name[ρ](person: {first: String, last: String, ..ρ}) -> String {
    person.first ++ " " ++ person.last
}

let employee = {first: "Alice", last: "Smith", id: 123}
let name = full_name(employee)  -- works with extra 'id' field
----

=== 12.2 Record Update

[source,affinescript]
----
fn with_id[ρ](r: {..ρ}, id: Int) -> {id: Int, ..ρ} {
    {id = id, ..r}
}
----

=== 12.3 Variant Extension

[source,affinescript]
----
type BaseError = ⟨NotFound: String | InvalidInput: String⟩
type ExtError[ρ] = ⟨NotFound: String | InvalidInput: String | ..ρ⟩

fn handle_base[ρ, A](
    e: ExtError[ρ],
    on_other: ⟨..ρ⟩ → A
) -> A {
    case e {
        NotFound(msg) → handle_not_found(msg),
        InvalidInput(msg) → handle_invalid(msg),
        other → on_other(other)
    }
}
----

== 13. Related Work

[arabic]
. *Rémy (1989)*: Original formulation of row polymorphism with
presence/absence
. *Wand (1991)*: Row polymorphism for type inference in ML
. *Leijen (2005)*: Extensible records with scoped labels
. *Pu*: Practical row polymorphism in production
. *Links*: Row polymorphism with effect types
. *Koka*: Row-polymorphic effects

== 14. References

[arabic]
. Rémy, D. (1989). Type Checking Records and Variants in a Natural
Extension of ML. _POPL_.
. Wand, M. (1991). Type Inference for Record Concatenation and Multiple
Inheritance. _Information and Computation_.
. Leijen, D. (2005). Extensible Records with Scoped Labels. _Trends in
Functional Programming_.
. Pottier, F. (2003). A Constraint-Based Presentation and Generalization
of Rows. _LICS_.
. Morris, J. G., & McKinna, J. (2019). Abstracting Extensible Data
Types. _POPL_.

'''''

*Document Metadata*: - Depends on: `lib/ast.ml` (row types), type
checker implementation - Implementation verification: Pending -
Mechanized proof: See `mechanized/coq/Rows.v` (stub)
