Rank Polymorphism Viewed as a Constraint Problem
Justin Slepak, Panagiotis Manolios and Olin Shivers.
ARRAY, 2018 © ACM
Rank polymorphism serves as a type of control flow used in
array-oriented languages, where functions are automatically lifted to
operate on high-dimensional arguments. The iteration space is derived
directly from the shape of the data, presenting a challenge to
compilation. A type system can characterize data shape, though the
level of detail is beyond what can be reasonably expected from
entirely human-generated annotations. The task of checking or
inferring shapes can be phrased as solving constraints in the theory
of the free monoid over the natural numbers, but the constraints
involve both universal and existential quantification. Here is a plan
of attack for leveraging past work on decision procedures, which has
generally focused on the purely existential fragment of the theory.
PDF (537K) © ACM