Phase 0, Section 1: Type System Foundation

Phase 0: Foundation — establishing the formal core calculus. Section 1 of 5: Type System Foundation.

1. What this section commits to

The grammar of types, the refinement language, the type formation rules, and the compile-time/runtime phase distinction. Everything subsequent — operation typing, subtyping, semantics, implementation — references decisions made here.

This section does not address operations (Section 2), subtyping (Section 3), semantics (Section 4), or implementation (Section 5). Anything from those concerns that appears here is a forward reference, not a commitment.

The convention through Phase 0: precise, prescriptive, with rationale. When a design alternative is rejected, the rejection is explicit. When something is deferred, it is named.

2. Grammar

The core type grammar:

Type    ::= Tensor[Dtype, Shape, Refinements]
          | Type → Type
          | Scalar[Dtype]
          | Unit

Dtype   ::= F32 | F16 | BF16 | F8E4M3 | F8E5M2
          | I64 | I32 | I16 | I8 | I4
          | Bool

Shape   ::= [Dim, ...]                              -- ordered list

Dim     ::= n                                        -- constant ∈ ℕ
          | α                                        -- variable
          | e                                        -- symbolic expression

e       ::= n | α | e + e | e − e | c · e            -- Presburger
          | e / e   (where divisor is constant)
          | e mod c

Ref     ::= [Predicate, ...]

Pred    ::= e = e | e ≠ e | e ≤ e | e < e
          | e ≥ 0 | Pred ∧ Pred | Pred ∨ Pred | ¬ Pred

A few notes:

• Shape is ordered. [B, S, D] and [S, B, D] are distinct types. There is no implicit dimension naming.
• Dim is integer-valued. Shapes don't have fractional dimensions. Division in e is restricted to constant divisors so that the result is in Presburger arithmetic.
• Predicates are SMT-decidable. This is the central commitment of the section; the rationale is in §3.
• I64 is a core dtype. Phase 0 argmax and argmin produce it, and Phase 1 gather consumes it; operation admissibility otherwise treats it as an ordinary signed integer dtype.
• Unit exists for operations that have no meaningful return value (effects, debug prints in later phases). It costs nothing to have it.

3. The refinement language: Presburger arithmetic

Decision: refinements are predicates in quantifier-free Presburger arithmetic with congruences (mod), discharged by Z3.

Presburger arithmetic is the first-order theory of the integers with +, −, =, <, ≤, multiplication by constants, and (in our extension) mod by constants. It is decidable. Z3 handles it efficiently.

What we get

• Decidable type checking. No human in the proof loop. The compiler discharges every refinement obligation automatically (subject to SMT timeouts, which §6 addresses).
• Sufficient for shape arithmetic. Most relationships between tensor dimensions are linear: D = H · D_head (multi-head attention), S' = S − k + 1 (convolution output shape), seq_len mod mesh_size = 0 (sharding divisibility). Presburger handles these.
• Reasonable error messages. When a refinement fails, Z3 can produce a counterexample assignment, which gets surfaced as "shape constraint not satisfied: example failure when B = 3, S = 5".

What we lose

• No multiplication of variables. X · Y where both are variables is outside Presburger. This rules out quadratic shape relationships, which do occur (block-sparsity at variable block sizes, FFT shapes). Workaround: introduce a fresh variable Z representing the product and let the user assert Z = X · Y as an axiom; the compiler accepts the assertion without proving it. Sound if the user is right; unsound if they're wrong. Documented as such.
• No quantifiers. All predicates are quantifier-free. Universal claims about all shapes get expressed structurally (parametric polymorphism) rather than as predicates.
• No real arithmetic. Numerical bounds on FP values (for quantization error) need a separate refinement layer; deferred to Phase 6.

Alternatives rejected

• Full first-order arithmetic. Undecidable. Requires user-written proofs for non-trivial obligations. Reject for a first version; the cost-benefit fails for the kinds of obligations Phase 0 needs to discharge.
• Linear arithmetic over rationals (LRA). Decidable, more expressive on the numeric side, but mismatches integer-valued shape semantics. Spurious solutions like B = 1.5 would need to be filtered. Reject.
• Liquid-types-style abstract interpretation. Could work but adds an inference layer between user predicates and the SMT solver. The leverage is recovered through SMT directly with care; defer Liquid-style automation to a later phase if it becomes necessary.
• Dependent types in the host calculus (Idris/Agda style). More expressive but undecidable type checking. Wrong shape for a practitioner-facing language. Reject.

The decision is Presburger plus a controlled escape hatch (axiomatic assertions). This is the same pragmatic tradeoff Liquid Haskell makes and that PyTorch 2's symbolic shape engine implicitly makes.

4. Type formation

When is a type well-formed? The judgment Γ ⊢ T type says "in context Γ, T is a well-formed type."

The context Γ tracks:

• Bound type variables (introduced by polymorphic function signatures).
• Bound shape variables (introduced by tensor types in scope).
• Active predicates (introduced by requires clauses on functions or by refinements on types in scope).

Formation rules:

─────────────────  (unit)
  Γ ⊢ Unit type


  Γ ⊢ dt dtype
─────────────────────  (scalar)
  Γ ⊢ Scalar[dt] type


  Γ ⊢ T₁ type      Γ ⊢ T₂ type
─────────────────────────────────  (function)
       Γ ⊢ T₁ → T₂ type


  Γ ⊢ dt dtype
  Γ ⊢ s shape
  Γ; s ⊢ R refset
  Γ ⊢ Sat(R)              -- refinements jointly satisfiable
─────────────────────────────────────────────  (tensor)
       Γ ⊢ Tensor[dt, s, R] type

The auxiliary judgments:

α ∈ Γ
─────────────  (var-shape)
 Γ ⊢ α dim


  Γ ⊢ d₁ dim    ...    Γ ⊢ dₖ dim
─────────────────────────────────────  (shape-list)
       Γ ⊢ [d₁, ..., dₖ] shape


  Γ; s ⊢ p₁ pred    ...    Γ; s ⊢ pₘ pred
──────────────────────────────────────────────  (refinements)
       Γ; s ⊢ [p₁, ..., pₘ] refset

The satisfiability check

Γ ⊢ Sat(R) says the refinements in R are jointly satisfiable in some integer model — that is, there exist concrete shape assignments under which all predicates hold. A refinement set like [B ≥ 1, B = 0] is well-formed grammatically but produces an empty type, which is almost certainly a programmer error. The compiler discharges Sat(R) via Z3 and rejects the type if Z3 returns unsat.

This catches obvious mistakes early. It does not catch useful refinement sets that happen to be vacuous in a particular call site — the check is on the type being well-formed, not on the call site producing a non-empty set of acceptable inputs.

5. Compile-time vs runtime phase distinction

Sharp commitment. What is known at compile time:

• All dtypes.
• The rank of every tensor (the length of its Shape).
• The structure of every shape (constant or symbolic; if symbolic, which variables and what expression).
• All active refinements and their satisfiability.

What is known only at runtime:

• The concrete integer values of symbolic shape variables.
• The contents of tensors (the floating-point or integer data).

The compiler reasons about types parameterized over symbolic shapes. The runtime substitutes concrete values for the symbolic variables when a function is called.

Implications

• Rank polymorphism is rejected for Phase 0. A function that operates on tensors of unknown rank (Tensor[f32, ?]) is not expressible. Rank must be known statically. This rules out some APL-family idioms but matches every production ML compiler.
• Symbolic dimension polymorphism is supported. A function can be polymorphic over any number of symbolic shape variables. def f[B, S, D](x: Tensor[f32, [B, S, D]]) -> ... is the standard form.
• Existential dimensions are deferred. Operations like nonzero(x), where the output dimension depends on data, are not expressible in Phase 0. Their handling is part of the data-dependent-shape work that connects to Phase 4 (sparsity) and Memo 1's discussion of data-dependent shapes. For now: not in scope.

This is intentionally restrictive. The phase distinction can loosen later (allowing existentials, allowing rank polymorphism in restricted forms); tightening it later would be a breaking change. Start tight, loosen carefully.

6. Symbolic shape variables: mechanics

A symbolic shape variable is bound by the program structure that introduces it. Three binding sites:

1. Function parameters. def matmul[B, S, D, V](a: Tensor[f32, [B, S, D]], b: Tensor[f32, [B, D, V]]) -> ... introduces B, S, D, V as bound in the function's scope.
2. Local declarations. let n = shape(x)[0] in ... introduces n as the runtime value of the dimension; n is in scope for the rest of the block.
3. Module-level constants. const HIDDEN = 768 introduces HIDDEN as a compile-time constant.

Variables bound at one binding site may not be referenced outside it. The compiler tracks scope through Γ.

Equality and aliasing

Two shape variables are equal only if they are the same variable, or if a refinement asserts their equality. Tensor[f32, [B, S, D]] and Tensor[f32, [B', S', D']] are different types even if the values turn out to coincide at runtime. To express equality, either:

• Use the same variable: Tensor[f32, [B, S, D]] twice in a signature.
• Add a refinement: requires B = B' ∧ S = S' ∧ D = D'.

This is the same convention as in dependently-typed languages with refinement types. It makes type identity decidable.

Substitution

Substitution T[α := e] replaces all free occurrences of α in T with the expression e. Standard capture-avoiding substitution; no special cases. When a function is called, the caller's argument types are unified against the function signature, producing a substitution that instantiates the function's bound variables.

Default α ≥ 1 and empty dimensions. Section 2 §15–§16: every introduced shape variable carries an implicit α ≥ 1 so zero-sized axes are excluded unless the programmer strengthens refinements with an explicit α ≥ 0 (or equivalent) on that variable — needed for empty-batch–style programs. If you omit such an override, types with a genuinely zero-sized dimension are ill-typed in the default discipline.

7. Examples

A few concrete typed signatures to ground the grammar.

Matmul

matmul : ∀ B, M, K, N.
  Tensor[F32, [B, M, K]] →
  Tensor[F32, [B, K, N]] →
  Tensor[F32, [B, M, N]]

The contraction dimension K appears in both inputs and is eliminated in the output. The batch B and the outer dimensions M, N are preserved.

Layer norm with hidden divisible by group size

groupNorm : ∀ B, S, H, G.
  requires H mod G = 0.
  Tensor[F32, [B, S, H]] → Tensor[F32, [B, S, H]]

The refinement H mod G = 0 is discharged at every call site; if the caller cannot prove it, the call does not type-check.

Reshape with conservation

reshape : ∀ d₁ ... dₘ, e₁ ... eₙ. ∀ T : Dtype.
  requires d₁ · d₂ · ... · dₘ = e₁ · e₂ · ... · eₙ.
  Tensor[T, [d₁, ..., dₘ]] → Tensor[T, [e₁, ..., eₙ]]

Note the products in the requires clause use multiplication of variables, which is outside Presburger. This is the case where the controlled escape hatch (§3) earns its keep: the user (or the elaborator) introduces fresh variables P_in and P_out representing the products, and the refinement becomes P_in = P_out. The product equalities themselves (P_in = d₁ · d₂ · ... · dₘ) are accepted axiomatically. The compiler trusts the user that P_in is the product; if they're wrong, the runtime catches it via shape mismatch.

This is ugly. Section 2 will refine the treatment of multi-dimensional reshape. Phase 0 just notes the issue and the workaround.

Attention head split

splitHeads : ∀ B, S, D, H.
  requires D mod H = 0.
  Tensor[F32, [B, S, D]] → Tensor[F32, [B, H, S, D / H]]

Division by a constant (or by a bound variable that the refinement establishes as a divisor of D) is supported because the result is in Presburger.

8. Design decisions, summarized

Decisions committed by this section:

Decisions not made (deferred to later sections or phases):

• How operations are typed (Section 2).
• How subtyping works (Section 3).
• Effect tracking, sparsity, sharding, hardware capabilities (later phases).
• Surface syntax (Phase 7).
• The mechanics of SMT timeout handling (Section 5 + implementation).

9. Open issues to revisit

1. Reshape's variable-product problem. The escape hatch in §7 is workable but ugly. Consider whether reshape gets a special form in the operation typing (Section 2) that handles dimension products via a built-in axiom rather than a user-facing assertion.

2. Default refinements (α ≥ 1). Resolved in Section 2 §15–§16: implicit at introduction, with explicit α ≥ 0 (or similar) override for empty-tensor cases.

3. Refinement set canonicalization. Two refinement sets [B ≥ 1, S ≥ 1] and [S ≥ 1, B ≥ 1] are equivalent. The type-checker needs to canonicalize before comparison. Trivial in principle; the implementation will need to choose a canonical form (sorted by some total order on predicates).

4. What goes in requires vs. in the refinement set. A function with requires D mod H = 0 could equivalently have the refinement on the input tensor type itself: Tensor[F32, [B, S, D] where D mod H = 0]. The grammar in §2 supports both. Pick one as canonical (probably: refinements bound to a tensor go on the tensor; refinements relating multiple tensors go in requires).

These are issues to revisit in later sections, not blockers.

10. Section 2 preview

Section 2 commits to (see that section for the authoritative rules):

• The ten core operations: elementwise unary, cast, elementwise binary, matmul, reduce (with keepdims typing variant), transpose, reshape, broadcast, slice, concat.
• The typing rules for each, including how shape arithmetic works.
• Broadcasting: explicit broadcast in the core IR only; no implicit broadcasting (Section 2 §11). Surface syntax may recover NumPy-like ergonomics later (Phase 7).
• How operation typing interacts with the satisfiability check (when does an operation's output type need a fresh Sat discharge?).

The grammar from this section is designed to support those operations without modification. If Section 2 forces a change to the grammar, that's a sign that this section's design is wrong and should be revisited rather than papered over.

End of Phase 0, Section 1.