论文标题
具有级别的多维阵列
Multi-dimensional Arrays with Levels
论文作者
论文摘要
我们探索了一个通用矩形多维阵列的数据结构。 n维数组的形状通常由n个自然数的元组给出。 该元组中的每个元素都定义了相应轴的长度。 如果我们将此元组视为阵列，则该阵列的形状由单个自然数n描述。 自然数量本身也可以视为一个阵列，其形状由自然数字1（或任何单胎集的元素）描述。 该观察结果产生了阵列类型的层次结构，其中L+1级的形状是自然数的L级级阵列。 当将阵列视为容器时，这种层次结构自然会发生，这使得可以定义等级和水平 - 晶型操作。 前者可以在大多数阵列语言中找到，而后者可以在大型超平面上进行部分选择，这在实践中通常很有用。 在本文中，我们介绍了具有级别的阵列的AGDA形式化。 我们表明，所提出的形式主义支持标准的等级 - 晶型阵列操作，而类型系统可以静态保证索引在范围内。 我们概括了排名运算符的概念，以便它适用于任意级别的数组，并且我们展示了为什么在实践中可能有用。
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.
