Efficient Functional Programming using Linear Types: The Array Fragment

Abstract

Functional languages excel at describing complex programs by composition of small building blocks. Yet, it can be difficult to predict the performance properties of such compositions. Namely, whether parts of the computation are shared or duplicated is typically left to the compiler to decide heuristically. Linear types serve as a tool to specify the desired behaviour (sharing or duplication). This means that the programmer is able to predict the performance of composition solely from the types of the composed functions. Girard’s linear logic (LL) can be extended with vector types and a synchronization primitive, making a linear language with array manipulation capabilities. In this master thesis, we improve on the n-ary extension of LL by introducing a self-dual, sequential array operator with an aggregation function. We provide a functional interpretation of the resulting calculus, which forms the basis for a low-level code generator. We then illustrate the effectiveness of the extended language by writing a number of examples in compositional style, and show that they predictably compile to efficient code. Examples include kernels of classical algorithms (1-dimensional stencil, QuickHull).