Multi-dimensional Arrays with Levels

Artjoms Šinkarovs
(Heriot-Watt University)

We explore a data structure that generalises rectangular multi-dimensional arrays. The shape of an n-dimensional array is typically given by a tuple of n natural numbers. Each element in that tuple defines the length of the corresponding axis. If we treat this tuple as an array, the shape of that array is described by the single natural number n. A natural number itself can be also treated as an array with the shape described by the natural number 1 (or the element of any singleton set). This observation gives rise to the hierarchy of array types where the shape of an array of level l+1 is a level-l array of natural numbers. Such a hierarchy occurs naturally when treating arrays as containers, which makes it possible to define both rank- and level-polymorphic operations. The former can be found in most array languages, whereas the latter gives rise to partial selections on a large set of hyperplanes, which is often useful in practice. In this paper we present an Agda formalisation of arrays with levels. We show that the proposed formalism supports standard rank-polymorphic array operations, while type system gives static guarantees that indexing is within bounds. We generalise the notion of ranked operator so that it becomes applicable on arrays of arbitrary levels and we show why this may be useful in practice.

In Max S. New and Sam Lindley: Proceedings Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020), Dublin, Ireland, 25th April 2020, Electronic Proceedings in Theoretical Computer Science 317, pp. 57–71.
Published: 1st May 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: