I gave a talk on TYPES’23 about implementing rank-polymorphic arrays in dependently-typed theory.

The slides are available here, and the extended abstract can be found here The abstract follows.

Rank polymorphism is the ability of a function to operate on arrays of arbitrary ranks. The advantages of rank-polymorphism are twofold: very generic array combinators and the ability to specify advanced parallel algorithms such as scan or blocked matrix multiplication in a very natural combinatorial style. In this work we present an embedding of rank-polymorphic arrays within a dependently-typed language. Our embedding offers the generality of the specifications found in array languages. At the same time, we guarantee safe indexing and offer a way to reason about concurrency patterns within the given algorithm. The notion of array reshaping makes it possible to derive multiple parallel versions of the algorithm from a single specification. The overall structure of the proposed array framework is surprisingly similar to categories with families that is often used to encode type theory. Shapes are contexts, reshapes are substitutions, and arrays are well-scoped terms.