Rank Polymorphism at Work

This pearl demonstrates how rank‑polymorphism enables programmers to abstract performance‑tuning aspects into the ranks and shapes of function arguments. Using prefix sum as an example, we show how a single, generic rank‑polymorphic specification can represent an entire class of traditionally separate algorithmic specifications that differ in performance characteristics but not in the overall outcome. The genuine elegance of this approach lies in the observation that, once encoded within a dependently‑typed language, we can prove that certain classes of argument reshaping do not affect the overall computational outcome. Consequently, this establishes the equivalence of all corresponding algorithmic specifications, which in classic (typically imperative) settings would be extremely tedious, if feasible at all.