Shape Checking of Array Programs

Shape theory provides a framework for the study of data types in which shape and data can be manipulated separately. This paper is concerned with shape checking, i.e. the detection of shape errors, such as array bound errors, without handling the data stored within. It can be seen as a form of partial evaluation in which data computations are ignored. We construct a simply-typed lambda-calculus that supports a vector type constructor, whose iteration yields types of arrays. It is expressive enough to construct all of the usual linear algebra operations. All shape errors in a term t can be detected by evaluating its shape #t. Evaluation of #t will terminate if that of t does. Keywords shape analysis, partial evaluation, arrays, higher-order. 1 Introduction Shape theory explores the consequences of manipulating shape and data separately (Jay [14]). Shape refers to the data structure in which the data is stored. For example, the shape of a three-dimensional regular array is a tuple of..