The Semantics of Rank Polymorphism

Justin Slepak; Olin Shivers; Panagiotis Manolios

arxiv: 1907.00509 · v1 · pith:KBO2IYNMnew · submitted 2019-07-01 · 💻 cs.PL

The Semantics of Rank Polymorphism

Justin Slepak , Olin Shivers , Panagiotis Manolios This is my paper

Pith reviewed 2026-05-25 11:54 UTC · model grok-4.3

classification 💻 cs.PL

keywords rank polymorphismdependent typesexistential typestype safetyarray programmingoperational semanticssoundnessAPL

0 comments

The pith

A dependent type system for rank-polymorphic languages is sound and rules out array shape errors at runtime.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Rank polymorphism lifts functions defined on low-rank arrays to apply automatically across higher-rank arrays by distributing over extra dimensions. The paper defines Remora as a core language with an operational semantics for this lifting and a static type system based on dependent types that tracks shapes and ranks. Existential abstraction handles cases where shapes or ranks are computed dynamically. The system satisfies progress and preservation, so well-typed programs cannot produce shape errors. A partially erased variant of the language yields an equivalent dynamic semantics, showing that the remaining types exactly describe the information needed at runtime.

Core claim

Remora's dependent type system, which incorporates existential abstraction for dynamically computed shapes and ranks, captures the shape-based lifting mechanism of rank polymorphism and is sound: progress and preservation hold, ensuring that array shape errors cannot occur at runtime in well-typed programs. Computations performed with fully typed terms stay in lockstep with those performed after partial type erasure, so the residual types precisely characterize the information required by the dynamic semantics.

What carries the argument

Dependent type system with existential abstraction over array shapes and ranks that encodes the lifting distribution rules.

If this is right

Well-typed programs execute without encountering array shape errors.
The dynamic semantics depends only on the residual types that remain after partial erasure.
Existential types allow programs to operate on arrays whose shapes or ranks are determined at runtime.
The argument types determine exactly how a function is lifted across higher-rank arrays.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The lockstep property between typed and erased terms supplies a route to proving correctness of optimizations that remove shape information after type checking.
The same combination of dependent types and existentials could be reused to give static guarantees for implicit broadcasting in array libraries of other languages.
Compilers could use the erased semantics as an intermediate representation that still respects the original lifting rules.

Load-bearing premise

The type rules correctly capture the shape-based distribution and lifting behavior of the dynamic semantics.

What would settle it

A concrete well-typed Remora program whose execution produces an array shape error, or a typed term and its erased counterpart whose reduction sequences diverge.

read the original abstract

Iverson's APL and its descendants (such as J, K and FISh) are examples of the family of "rank-polymorphic" programming languages. The principal control mechanism of such languages is the general lifting of functions that operate on arrays of rank (or dimension) $r$ to operate on arrays of any higher rank $r' > r$. We present a core, functional language, Remora, that captures this mechanism, and develop both a formal, dynamic semantics for the language, and an accompanying static, rank-polymorphic type system for the language. Critically, the static semantics captures the shape-based lifting mechanism of the language. We establish the usual progress and preservation properties for the type system, showing that it is sound, which means that "array shape" errors cannot occur at run time in a well-typed program. Our type system uses dependent types, including an existential type abstraction which permits programs to operate on arrays whose shape or rank is computed dynamically; however, it is restricted enough to permit static type checking. The rank-polymorphic computational paradigm is unusual in that the types of arguments affect the dynamic execution of the program -- they are what drive the rank-polymorphic distribution of a function across arrays of higher rank. To highlight this property, we additionally present a dynamic semantics for a partially erased variant of the fully-typed language and show that a computation performed with a fully-typed term stays in lock step with the computation performed with its partially erased term. The residual types thus precisely characterise the type information that is needed by the dynamic semantics, a property useful for the (eventual) construction of efficient compilers for rank-polymorphic languages.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Remora formalizes rank polymorphism with a dependent type system and claimed soundness, but the abstract leaves the actual proofs and decidability details thin.

read the letter

Remora formalizes rank polymorphism with a dependent type system and claimed soundness, but the abstract leaves the actual proofs and decidability details thin. The paper introduces a core language that directly models the lifting of functions across array ranks, which is the key mechanism in APL-family languages. It supplies both an operational semantics and a static type system built on dependent types plus existential abstraction to handle shapes or ranks that are only known at runtime. This setup is new; earlier treatments stayed at the level of informal description or implementation tricks. The lock-step equivalence between the fully typed terms and their partially erased counterparts is a useful result because it shows precisely which type information the runtime needs. That part lands cleanly and could help with compiler design for these languages. The soundness argument rests on progress and preservation, which would mean well-typed programs cannot hit shape errors. The abstract states that the type system stays restricted enough for static checking while still capturing the shape-driven distribution. If the full definitions and proofs back that up without extra restrictions that break the intended programs, the work holds together. The main soft spot is the lack of any proof sketch, type rules, or complexity argument in the abstract. Without those, it is difficult to judge whether the existentials keep type checking decidable in practice or whether the system scales beyond the core examples. The paper is for people working on formal semantics of array languages or domain-specific languages in scientific computing. A reader already familiar with dependent types and APL-style programming would get the most out of the formalization and the erasure result. It deserves peer review because the core idea is coherent and addresses a real gap, even if the presentation needs more concrete evidence to convince referees.

Referee Report

0 major / 1 minor

Summary. The paper introduces Remora, a core functional language capturing the rank-polymorphic lifting mechanism of APL-like languages. It defines a dynamic operational semantics, a dependent type system (with existential abstraction over shapes and ranks) that statically captures the lifting rules while remaining decidable, proves progress and preservation (soundness: well-typed programs produce no shape errors at runtime), and establishes a lock-step correspondence between the fully typed semantics and a partially erased dynamic semantics whose residual types characterize exactly the information needed at runtime.

Significance. If the claimed metatheorems hold, the work supplies the first formal account of type safety for rank polymorphism, directly addressing the unusual dependence of dynamic behavior on argument shapes. The existential mechanism for dynamic shapes and the erasure result are both technically useful for language design and compiler construction. The paper ships explicit definitions of the core language, type rules, and reduction relation, which supports reproducibility of the formal claims.

minor comments (1)

The abstract states that progress and preservation have been established but does not name the specific lemmas or the form of the type environment; a one-sentence pointer in the abstract to the relevant theorem numbers would help readers locate the central results.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive recommendation to accept the paper. The report accurately captures the contributions of Remora's dynamic semantics, dependent type system with existentials, soundness proofs, and erasure correspondence.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper defines a new core language Remora, its operational semantics, and a dependent type system with existentials from the ground up. It then proves standard progress and preservation (soundness) plus a lock-step erasure property. No load-bearing step reduces a claimed result to a fitted parameter, a self-citation chain, or a definitional renaming; the type rules and reduction rules are presented as independent artifacts whose correspondence is verified directly. This matches the most common honest outcome for a formal semantics paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper's central claims rest on the definition of a new language and the application of standard type-theory results to it; no free parameters are introduced and the only invented entity is the language itself.

axioms (1)

standard math Standard progress and preservation theorems can be established for the presented dependent type system
Invoked to conclude soundness from the type rules.

invented entities (1)

Remora core language no independent evidence
purpose: To serve as a minimal model that isolates the rank-polymorphic lifting mechanism
Newly defined in the paper; no independent evidence outside the definitions is supplied.

pith-pipeline@v0.9.0 · 5836 in / 1353 out tokens · 43774 ms · 2026-05-25T11:54:28.328222+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We establish the usual progress and preservation properties for the type system, showing that it is sound, which means that 'array shape' errors cannot occur at run time in a well-typed program.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.