Phase 0, Section 3: Subtyping and Coercion

Phase 0: Foundation — establishing the formal core calculus. Section 3 of 5: Subtyping and Coercion.

1. What this section commits to

When two types are the same under the type-checker even though they are not literally equal: the subtyping relation. When the user (or elaborator) must insert an explicit operation to bridge two types: the coercion relation. The line between these is the central question for this section.

The Sections 1 and 2 grammar and operation typing are not expected to change here. If subtyping forces a change to either, that's evidence the foundation is wrong rather than that subtyping needs special-casing.

2. Subtyping vs. coercion: the conceptual distinction

Two types T₁ and T₂ may be related in three ways:

Phase 0 commits to a sharp line:

Subtyping affects only the refinement axis. Dtype, shape structure, and rank are all invariant. Differences along those axes require coercions (cast, broadcast, reshape, transpose) — explicit operations in the IR with explicit lowering.

The rationale is operational. A subtype relationship has no runtime effect; the value just gets viewed at a different type. A coercion is a real operation: cast performs FP rounding, broadcast replicates data (or sets up a view), reshape may or may not produce a new tensor. The IR should make the distinction visible because the lowering and the cost are different.

3. Subtyping rules

The judgment is Γ ⊢ T₁ <: T₂ — "in context Γ, every value of T₁ is a value of T₂."

3.1 Reflexivity

   Γ ⊢ T type
─────────────────  (refl)
  Γ ⊢ T <: T

Every well-formed type is a subtype of itself. Standard.

3.2 Transitivity

  Γ ⊢ T₁ <: T₂      Γ ⊢ T₂ <: T₃
─────────────────────────────────────  (trans)
        Γ ⊢ T₁ <: T₃

Subtyping composes. The implementation derives transitivity rather than checking it explicitly; it falls out of the structural rules below.

3.3 Tensor subtyping (the load-bearing rule)

  Γ ⊢ s₁ ≡ s₂
  Γ; R₁ ⊨ R₂
─────────────────────────────────────────────────  (sub-tensor)
  Γ ⊢ Tensor[dt, s₁, R₁] <: Tensor[dt, s₂, R₂]

Three premises:

• Dtype is invariant. Same on both sides. Tensor[F32, ...] <: Tensor[BF16, ...] does not hold even though every BF16 value is approximately representable as F32. The value sets are different (different rounding behavior, different bit patterns); coercion is required.
• Shape is structurally equal. s₁ ≡ s₂ is the SMT-discharged shape equality from Section 2 §2: same length, dimension-wise equality under SMT. There is no shape "polymorphism" or "narrowing"; differences require explicit reshape or broadcast.
• Refinements: R₁ implies R₂. This is the only place real subtyping happens. The notation Γ; R₁ ⊨ R₂ means "in context Γ extended with the assumption that all predicates in R₁ hold, every predicate in R₂ is implied." Discharged via Z3: assert Γ ∧ R₁ ∧ ¬R₂; if unsat, the implication holds.

The intuition: stronger refinements produce smaller value sets. A tensor known to satisfy B ≥ 100 can be used wherever a tensor satisfying B ≥ 1 is expected, because the first constraint implies the second. The subtype is the more constrained one.

3.4 Function subtyping

  Γ ⊢ T₂ <: T₁    Γ ⊢ U₁ <: U₂
─────────────────────────────────  (sub-fn)
   Γ ⊢ T₁ → U₁ <: T₂ → U₂

Contravariant in the input, covariant in the output. Standard. A function is a subtype if it accepts a wider set of inputs (less constrained refinements) and produces a narrower set of outputs (more constrained refinements).

3.5 No width subtyping

Refinement sets are not records. There is no [p₁, p₂, p₃] <: [p₁, p₂] rule based on length. Width-style subtyping falls out of implication: R₁ ⇒ R₂ if R₁ includes (or implies) every predicate of R₂, regardless of cardinality.

This means:

• A canonicalization pass at parse time is not required for subtyping correctness. SMT handles semantic equivalence: [B ≥ 100] ⇒ [B ≥ 1] whether or not the predicates are syntactically aligned.
• Canonicalization is still useful for implementation efficiency (caching subtyping results, deduplication in error messages). The implementation will canonicalize; the type system doesn't depend on it.

4. The subsumption rule

  Γ ⊢ e : T₁    Γ ⊢ T₁ <: T₂
─────────────────────────────────  (subsumption)
        Γ ⊢ e : T₂

Standard. Any expression at a subtype can be used where a supertype is expected. This is what makes subtyping implicit — no syntactic marker, the value just flows.

The subsumption rule is admissible, not declared as a separate operation. The type-checker applies it during synthesis-vs-checking (bidirectional type-checking, Section 5 implementation): when checking that an expression has an annotated type, the checker synthesizes the expression's type and verifies subtyping against the annotation.

5. Subtyping algorithm

Given Γ ⊢ T₁ <: T₂?, the implementation:

1. Structural decomposition. If T₁ and T₂ are different shapes (one tensor, one function), reject. If both are functions, recurse on inputs (contravariantly) and outputs (covariantly). If both are tensors, proceed to (2).

2. Dtype check. Compare dtypes for syntactic equality. If different, reject. (Cast is required.)

3. Shape check. For each dimension, build the SMT obligation s₁[i] = s₂[i] and discharge under Γ. If any dimension fails, reject.

4. Refinement implication. Build the SMT obligation R₁ ⇒ R₂ (i.e., assert Γ ∧ R₁ ∧ ¬R₂, check satisfiability). If unsat, the implication holds, accept. If sat, the counterexample is the failing refinement and is reported. If unknown (timeout), reject.

The total cost is dominated by SMT calls. The implementation should:

• Cache subtyping results by (T₁, T₂, Γ-hash).
• Short-circuit on syntactic equality before calling SMT.
• Batch related obligations when the type-checker has many subtyping queries against the same context.

Section 5 (implementation) elaborates these.

6. Coercions in the core IR

Coercions are operations, not subtyping. Each appears in the IR explicitly. From Section 2:

The user (or elaborator) inserts these explicitly. The core IR does not "automatically broadcast" or "automatically cast." This was committed in Section 2 §11 for broadcasting and §5 for casting; this section ratifies the broader principle.

The reason is consistency with the lowering story. Each coercion has a specific MLIR linalg lowering and a specific cost. Inserting them explicitly means the IR makes the cost visible and the lowering is unambiguous.

6.1 Coercion vs. subtyping in practice

Two cases that look similar but lie on opposite sides of the line:

(* Subtyping: the value flows; no operation. *)
let f (x : Tensor[F32, [B, S], [B ≥ 1]]) : Tensor[F32, [B, S], [B ≥ 0]] =
  x  (* B ≥ 1 implies B ≥ 0; subsumption applies. *)

(* Coercion: explicit operation in IR. *)
let g (x : Tensor[F32, [B, S, D]]) : Tensor[F32, [B, S, D, 1]] =
  reshape[[B, S, D, 1]] x
  (* The trailing 1 changes the shape structure. Not subtyping. *)

The first compiles to no IR operation — f is the identity at runtime. The second compiles to a reshape IR node, which lowers to (most likely) a stride manipulation but is still a visible operation.

7. The subtyping algorithm and bidirectional checking

The full type-checking strategy for Phase 0 is bidirectional:

• Synthesis (Γ ⊢ e ⇒ T): given an expression, produce its type. Used for variables, constants, and operations whose type is determined by their structure.
• Checking (Γ ⊢ e ⇐ T): given an expression and an expected type, verify the expression has that type. Used at function call sites, return statements, and let-bindings with annotations.

Subsumption appears at the synthesis-to-checking boundary:

  Γ ⊢ e ⇒ T₁    Γ ⊢ T₁ <: T₂
─────────────────────────────────  (check-via-sub)
        Γ ⊢ e ⇐ T₂

This is the only place the type-checker invokes the subtyping algorithm. Internal nodes use synthesis. Boundary checks use subtyping.

This commits us to bidirectional type-checking as the algorithmic strategy. It is well-understood, plays well with refinement systems, and produces good error messages (the failure point is always a synthesis-vs-checking mismatch at a known location).

8. Examples

Concrete cases to test understanding.

8.1 Refinement strengthening

T₁ = Tensor[F32, [B, S, D], [B ≥ 16, D mod 8 = 0]]
T₂ = Tensor[F32, [B, S, D], [B ≥ 1]]

T₁ <: T₂  ✓

T₁'s refinements imply T₂'s. A function expecting T₂ accepts T₁.

8.2 Refinement weakening (rejected)

T₁ = Tensor[F32, [B, S, D], [B ≥ 1]]
T₂ = Tensor[F32, [B, S, D], [B ≥ 16]]

T₁ <: T₂  ✗  (counterexample: B = 1)

B ≥ 1 does not imply B ≥ 16. The user gets a counterexample assignment.

8.3 Dtype mismatch (rejected, requires cast)

T₁ = Tensor[BF16, [B, S], []]
T₂ = Tensor[F32, [B, S], []]

T₁ <: T₂  ✗  (dtype invariant)

To convert: cast[F32] x : Tensor[F32, [B, S], []]

The dtype rejection is structural; the user inserts cast. Note that the cast operation's MLIR lowering may or may not be lossless; that's a numerical concern (Phase 6) not a type-system one.

8.4 Function subtyping

F₁ = Tensor[F32, [B, S], [B ≥ 1]]   → Tensor[F32, [B, S], [B ≥ 16]]
F₂ = Tensor[F32, [B, S], [B ≥ 16]]  → Tensor[F32, [B, S], [B ≥ 1]]

F₁ <: F₂  ✓

F₁ accepts a wider input set (B ≥ 1 is weaker than B ≥ 16) and produces a narrower output set (B ≥ 16 is stronger than B ≥ 1). It can be substituted for F₂ anywhere F₂ is expected.

8.5 Shape rank difference (rejected)

T₁ = Tensor[F32, [B, S], []]
T₂ = Tensor[F32, [B, S, 1], []]

T₁ <: T₂  ✗  (rank invariant)

To convert: reshape[[B, S, 1]] x  or  unsqueeze[axis=2] x

Different ranks are different types. The user inserts a reshape (or, if Phase 7's surface syntax adds unsqueeze, that desugars to reshape).

8.6 Refinement set canonicalization (handled implicitly)

T₁ = Tensor[F32, [B], [B ≥ 1, B ≥ 0]]
T₂ = Tensor[F32, [B], [B ≥ 1]]

T₁ <: T₂  ✓
T₂ <: T₁  ✓

B ≥ 0 is implied by B ≥ 1, so the two refinement sets are logically equivalent. SMT discharges both directions. The implementation will canonicalize for efficiency, but the rules are correct without it.

9. Implicit dtype promotion: rejected

A tempting feature that this section commits to not having: implicit dtype promotion. In NumPy, int_array + float_array automatically promotes the int to float. In Python, int + float returns float. In C, int + double promotes via integer promotions.

Phase 0 rejects this. Dtype mismatch in elementwise binary operations is a type error, full stop. The user calls cast explicitly.

Rationale:

• Implicit promotion has subtle semantic issues. INT8 + INT8 should not silently widen to INT32 (overflow vs widening is a real choice the user should make). BF16 + F32 should not silently downcast or upcast (precision matters in ML).
• The promotion lattice itself is contentious. NumPy's rules are documented but surprising; Python's are narrow; C's are notorious. There is no obviously-correct default.
• Surface syntax (Phase 7) is the right place for promotion sugar. Different surface dialects can have different promotion rules over the same core IR.

Same argument as broadcasting in Section 2 §11: the core IR is the contract; surface ergonomics is a separate concern.

10. Resolved open issues

• Section 1 issue 4 (requires vs. inline refinements): closed by Section 2 §15. Re-confirmed here because subtyping doesn't care about syntactic placement; only logical content matters.
• Section 1 issue 3 (refinement set canonicalization): closed for the type-system concern by §8.6. SMT handles semantic equivalence regardless of syntax. Canonicalization remains as an implementation efficiency item, not a correctness item.

11. New open issues

1. Algorithmic subtyping for refinements containing free shape variables. When Γ ⊢ T₁ <: T₂ and both types contain free shape variables (e.g., a polymorphic function's signature), the SMT discharge may ∀-quantify those variables. Z3 handles ∀-Presburger but may be slow. Engineering mitigation is recorded at the end of Section 5 §11 (structural unification before implication when needed).

2. Mutual recursion and subtyping coinduction. Functions calling each other through subtyping create a fixed-point obligation. Engineering approach: greatest fixed-point subtyping with cycle detection — end of Section 5 §11. Not user-visible in Phase 0.

3. Subtyping for effect rows. Effects (Phase 2) will introduce row types: Tensor[F32, s, R] !{Random, State}. Subtyping over effect rows is its own design question — typically row subtyping where extra effects in the smaller row are permitted. Deferred to Phase 2.

4. Negative refinements. A predicate like ¬(B = 0) is in the grammar but creates SMT performance issues (negation over disjunction explodes). Phase 0 semantics: correctness does not depend on a particular normal form. Implementation: canonicalize negation and align with the global SMT timeout policy — end of Section 5 §11.

12. Decisions, summarized

13. Section 4 preview

Section 4 commits to (see that section for the authoritative definitions):

• Operational semantics. Configurations (H, e) with a heap; small-step reduction; denotationally, tensors as functions from index tuples to values.
• Well-typed heap. A precise invariant H well-typed under Γ (Section 4 §3.3) used in subject reduction.
• Type soundness. Subject reduction and progress, modulo the idealized reshape assumption (Section 4 §7.0); proof deferred to Phase 6.
• The numerical-semantics gap. Structural (real-valued) semantics vs floating-point implementations; separation from numerical error verification (Phase 6+).

Sections 1, 2, and 3 are not expected to change in Section 4. The semantics is a model for the typing rules already committed; if the model can't accommodate them, the rules are wrong.

End of Phase 0, Section 3.