What Star is

A short, fair summary, in case you have not read it (you should). Star is a small functional array calculus — pointful, in the tradition of \tilde{F} and Single Assignment C — whose contribution is a type system for array shapes built from structural records and variants. Three ideas carry it.

First, algebraic shapes. A shape is not a tuple of integers but a tree of two constructors: a product shape {|ℓ : σ, …|}, indexed by a record of per-axis indices, models named multidimensional arrays; a concatenation shape ⟦T : σ, …⟧, indexed by a variant, models padding and concatenation. Records give a product on shapes; variants give a sum. The names are the point — a product shape is exactly a named-tensor axis set, and the paper is candid that this generalizes the named-tensor and xarray line of work.

Second, structural subtyping forming a distributive lattice. Star’s shapes and indices subtype — width and depth, records one way, variants the other — and the order is a distributive lattice with meets and joins. This is the algebraic-subtyping discipline of Dolan and Mycroft’s MLsub, with the polarity restriction lifted by Parreaux and Chau, and Star’s bet is that this discipline buys it principal ML-style type inference (conjectured, not yet proved). Crucially, broadcasting is the meet in this lattice: aligning two shapes finds their greatest lower bound, so a column vector and a row vector broadcast to the matrix that is their meet — the outer product.

Third, and most subtly, shapes and indices are distinct but isomorphic. Star insists you can no longer pretend an array’s shape and its index have the same type, the way you can when both are tuples of integers. A product shape is indexed by a record; a concatenation shape, built by a sequence of components, is indexed by one tagged variant. The relationship is carried by a metafunction \iota that maps each shape type \sigma to its index type \iota(\sigma), and \iota is an isomorphism in the type lattice. Arrays, in this reading, are containers in the sense of Abbott, Altenkirch and Ghani: a shape together with a position-type that depends on it, \Sigma(s : \mathrm{Shape}).\,\mathrm{Position}(s) \to \alpha. Star’s Position is exactly \iota.

The paper proves type safety in the simply-typed case — preservation and progress — and sketches the patterns it captures: tensors as products, padding as concatenations, broadcasting as the meet, axis indexing as record update and restriction. It leaves shape inference, stencils, recursive shapes, and the full polymorphic metatheory as future work. It is, in the best sense, a design paper: it stakes out a new region between untyped array programming and dependently typed array programming, and argues the region is habitable.

That third idea — a shape is not its index, but the two are isomorphic — is where Star and OCANNL are closest, and it is where the whole comparison should start.

Three convergences

A Rosetta stone

The convergence is easiest to feel on the shared examples. Star’s worked patterns are OCANNL’s worked patterns, and writing them side by side — the shape as Star would type it, the operation as OCANNL would spec it — shows the agreement on structure and the divergence on what each system then does with it.

Read across a row and the systems agree on the object. Read down the columns and the difference shows: Star’s column is a type, written by the programmer and checked; OCANNL’s column is a spec, from which sizes and a loop nest are inferred. Star types the padding; OCANNL types it and emits the offset arithmetic and the disjoint-cover check. The table is the whole comparison in miniature — same structure, two jobs.

Three divergences

The agreements are about structure. The disagreements are about goal, and they are sharper. Star optimizes for static safety guarantees expressible within ML-tradition type inference. OCANNL optimizes for shape inference and code generation. Where those goals pull apart, the systems pull apart — most visibly on numeric sizes and on boilerplate.

What OCANNL should borrow

Generosity with a purpose: Star has exactly the apparatus OCANNL’s blog-shaped account lacks, and the workshop paper should take it.

Star has a core calculus — a grammar of expressions, an operational semantics, a type system, and type-safety theorems with proofs — compressed into a handful of figures. OCANNL’s four posts describe algorithms (constraint solving, union-find, the closing policy) beautifully, but there is no formal object-language whose programs you can write down and whose semantics you can state. Star is the model for what that object should look like and how compactly it can be presented.

Star states principal inference as its goal and ties it to algebraic subtyping, where it remains a conjecture. OCANNL’s situation is the same in form and more interesting in detail. The core single-stage solver should be straightforwardly principal — the rules are monotonic, so the least-committed satisfying substitution is reached and is unique up to renaming — and the interest is in what survives once the stages wrap it: the affine index’s solve-then-evaluate strata, the padding fixpoint, concatenation’s coupling, and above all closing. Closing is deliberately not principal: it commits the variables the principal substitution leaves free, in a direction the constraints do not force. Here is a conjecture that sharpens what that costs. If every variable were closed upward, the result would be the most general shapes the constraints allow — the biggest types, which in this order are the tensors smallest in size — each unforced axis sent to the no-claim top 1_\emptyset. Uniform-upward closing is thus the closing nearest the principal, still-free substitution; the actual policy departs from it only on leaves, which it closes downward to a concrete allocatable shape, trading that generality for a size a buffer can be cut to. So the honest result is layered — principal core, generality-preserving on interiors, deliberately non-principal on leaves, with core projection inference not merely principal but canonical (an equivalence has no direction to choose) and the multi-stage question left open. That layered story, stated as the theorems below make it, is sharper than a single conjecture, and one Star has no need to tell, because Star does not close, stage, or compile.

OCANNL’s genuine debt to type-system research is narrower than Star’s and worth stating exactly, since it is not the container tradition. What OCANNL took was the emphasis on inference and the idea of combining row variables with subtyping — indeed the first post opens by retiring the name “row polymorphism plus nominal subtyping,” a name that records precisely that lineage even as it corrects it. The container and Naperian-functor vocabulary is a further borrow available to the paper, not one OCANNL already leans on. Star grounds its arrays in containers and Naperian functors — recognized PL vocabulary for indexable structures — and OCANNL’s arrays are containers, a shape together with a position map that projection inference computes; saying so in those words would cost nothing and signal fluency to exactly the audience the paper is for. It is an adoption to make deliberately, not a description of the present design.

And Star’s worked examples are OCANNL’s worked examples: padding, the outer product, the GNN broadcast, the graph construction. The Rosetta-stone table above is the seed of it; in the paper that table wants a worked pair or two spelled out in full — the same operation in Star’s variant-typed surface and OCANNL’s einsum spec, with OCANNL’s inferred sizes and loop nest shown alongside Star’s checked type — so the divergence speaks for itself, since Star types the padding and OCANNL types it and compiles it.

A template for the workshop paper

What follows is a skeleton — the spine, a core-calculus sketch in the compact style Star models, and the two theorem statements the paper would have to discharge. It is brainstorm material, not prose to lift; the paper is yours to write by hand. But it pins the obligations.

The spine. One elaboration, two readings, one bridge. A program elaborates to a single constraint set \Phi over dimension and row terms. The shape reading solves \Phi as an order, in the broadcast lattice (claim-free top 1_\emptyset, error bottom \bot), producing sizes. The index reading re-solves \Phi as an equivalence-and-coupling, producing a loop nest. The bridge is the elaboration \llbracket\cdot\rrbracket, which is OCANNL’s \iota: the canonical map from solved shape-structure to index-structure. Star types \iota; OCANNL computes along it. Everything in the four posts is an instance of this architecture, and the paper’s job is to make the architecture a theorem.

The terms (reusing the series’ notation, so the paper dovetails with the posts):

\begin{aligned} \text{dim term} \quad t &::= \alpha \;\mid\; n_b \;\mid\; \mathsf{Affine}\{\,\text{stride},\text{over},\text{conv},\text{offset}\,\} \;\mid\; \mathsf{Concat}[\,t,\ldots\,] \\ \text{row term} \quad R &::= \rho \;\mid\; l\cdot\diamond\cdot r \;\mid\; l\cdot\langle\rho\rangle\cdot r \\ \text{constraint} \quad \phi &::= t = t \;\mid\; t \sqsubseteq t \;\mid\; R = R \;\mid\; R \sqsubseteq R \\ \text{index form} \quad \pi &::= \mathsf{Fix}(c) \;\mid\; \mathsf{Iter}(s) \;\mid\; \mathsf{Affine}(\textstyle\sum_i c_i s_i + o) \;\mid\; \mathsf{Concat}(s,\ldots) \end{aligned}

with \alpha a dimension variable, n_b a size n carrying basis b (and 1_\emptyset the claim-free top), \rho a row variable, \diamond the broadcast marker, and the flanks l,r sequences of dim terms.

The order is the broadcast order of the first post, with two units. Per dimension, d \sqsubseteq 1_\emptyset for every d, \mathrm{join}(d, d') = 1_\emptyset for distinct atoms d \neq d', and \mathrm{meet}(d, d') = \bot (the broadcast error) for distinct atoms — so the dimension order is a bounded lattice with top 1_\emptyset (the product unit), an antichain of size atoms in the middle, and an error bottom \bot; it is non-distributive (M_3) whenever three or more sizes meet. Concatenation adds a second unit, 0 (the coproduct unit, the empty summand), which is neither the top nor the error bottom but off the broadcast order entirely — it is the bottom of the additive order the coproduct induces — admitted only for discardable_vars. Rows lift the dimension order structurally through the marker; rank-broadening inserts 1_\emptyset at the marker; rank-polymorphism is the order relating rows of different ranks.

The elaboration \llbracket\cdot\rrbracket = \iota. Per-operation, after sizes are solved: freshen every projection identifier (locality), re-derive the operation’s constraints, and read each as a projection equation. Schematically, \llbracket d_1 = d_2 \rrbracket = \mathsf{Eq}(\llbracket d_1\rrbracket, \llbracket d_2\rrbracket) unions two axes into one loop (co-iteration); a broadcast inequality with a size-one operand axis, \llbracket d_{\text{result}} \sqsubseteq (d_{\text{operand}}{=}1)\rrbracket = \mathsf{Eq}(\llbracket d_{\text{operand}}\rrbracket, \mathsf{Fix}(0)), severs and pins; a Concat becomes a connected component traversed sequentially. Equality unions, broadcasting severs, concatenation couples. A reduction is emergent: a product axis the output index map omits.

Theorem 1 (Core principality). For a constraint set \Phi, the core single-stage solver computes a substitution \sigma_\star with \sigma_\star \models \Phi such that for every model \sigma \models \Phi there is a u with \sigma = u \circ \sigma_\star; the free variables of \sigma_\star are exactly those \Phi does not force. Conjectured by Star for its setting; here it should follow from monotonicity — variables solved at most once and substituted out, bounds only tightening — together with the join-collapse of incompatible caps to the top 1_\emptyset. This is the clean half.

Remark (Closing is a policy, not a principal step). The principal \sigma_\star leaves leaves and interiors free; runtime allocation needs them determinate, so a closing phase commits each — a leaf downward to the most specific shape its bounds permit, an interior upward to the unit (the claim-free top). The direction is justified (a leaf has no more-permissive source to be pressured from; an unforced interior should make no claim) and the result is sound and total, but it is not forced by \Phi, so closing is deliberately non-principal. The paper’s obligation is to state closing as a separate, characterized layer rather than fold it into Theorem 1 — and to be precise that the two-phase interleave (solve, close leaves, solve again, close interiors) preserves soundness at each step.

Theorem 2 (Core projection canonicity). Core projection inference is forced and unique up to renaming of the fresh iterator symbols: it succeeds or reports a conflict, and never resolves an ambiguity. Stronger than principality — there is no closing direction to choose, because an equivalence has no up or down — and the asymmetry with shape inference (which must choose at closing) is itself a result worth stating.

Open problem (Multi-stage). Characterize what Theorems 1 and 2 become once the stages enter: the affine index’s solve-then-evaluate stratification, the padding fixpoint frozen at finalization, and concatenation’s connected-component coupling. The expected shape of the answer: determinacy and the no-guessing property survive, but flatness does not — a check between two derived (affine or coupled) terms can fire only after the stratum that evaluates its operands, so a conflict can surface later than where the constraint was written. Stating exactly which guarantees are preserved across the seams, and where principality could break, is the paper’s central technical contribution and the place it most clearly goes past Star, which has no stages to stratify.

Theorem 3 (Soundness of projection inference w.r.t. shapes). Let the shapes of an operation be solved and closed. Then the inferred index maps address only within those shapes: every \pi_T(p) for p in the product space is a valid multi-index into T at its solved shape; co-iteration is finer than size-equality; and the coproduct cover is disjoint (at most one summand active per position). This promotes the first post’s informal argument — indices derived from the same facts as the sizes cannot contradict the sizes — to a theorem. It is the compilation-side analogue of Star’s preservation and progress: where Star shows a well-typed term does not get stuck on a structural index, OCANNL shows a solved operation does not generate an out-of-bounds loop nest. The locality discipline (global sizes, local identities) is a premise here, not a convenience — it is what makes “co-iteration is finer than size-equality” true rather than merely hoped for.

The positioning is the design-space paragraph above: non-distributive lattice versus distributive lattice, sizes-in-the-solver versus sizes-untyped versus sizes-refined, polymorphism-by-re-evaluation versus polymorphism-by-generalization. And the limitations are honest: OCANNL’s rows are flat sequences, not Star’s nested algebraic shapes, which buys positional einsum matching and clean strides at the cost of the pytree-style nesting that Star’s recursive-types future work points toward; and OCANNL has not taken the refinement-types road, so its size arithmetic is a bespoke solver, not a reusable type-level discipline.

Where this leaves the series

Four posts found a familiar operation hiding inside a humbler one and reused the core rather than extending it. This post found a familiar system sitting beside OCANNL and reused the comparison rather than the code. Star and OCANNL are two points on one map. They agree on the deep structure — broadcasting is the meet, concatenation is a variant is a coproduct, a shape is not its index — because that structure is not anyone’s invention but the shape of the problem. They diverge on the bet: Star types the correspondence between shape and index and stops there, winning static safety inside the ML tradition at the cost of leaving sizes to runtime and boilerplate to the programmer; OCANNL computes along the correspondence, winning shape inference and a loop nest at the cost of a bespoke solver and a metatheory still to be written. The first bet is a type system. The second is the thing you reach for when the type system’s job is only half the problem — when, having decided a shape is not its index, you want a machine that fills in both.

The workshop paper is where the second bet gets its theorems. Jakub’s paper is where to send the reader who wants to see the first bet made well.

OCANNL is open source, at github.com/ahrefs/ocannl.