Composable Efficient Array Computations Using Linear Types

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 typi-cally left to the compiler to decide heuristically. We propose the use linear types as a tool to specify the desired behavior (sharing or duplication). This means that the programmer is able to predict the performance of composition solely from the types of the composed functions. In this paper, we focus on the array-manipulation fragment of such a language. Technically, we extend Girard’s linear logic (LL) with vector types and a synchronization primitive. These extensions allow expressing array-processing programs in a compositional fashion. We illustrate the effectiveness of our 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 (FFT, 1-dimensional stencil, QuickHull)