Linearity and laziness

Abstract

A criticism often levelled at functional languages is that they do not cope elegantly or efficiently with problems involving changes of state. In a recent paper [26], Wadler has proposed a new approach to these problems. His proposal involves the use of a type system based on the linear logic of Girard [7]. This allows the programmer to specify the “natural” imperative operations without at the same time sacrificing the crucial property of referential transparency.

In this paper we investigate the practicality of Wadler's approach, describing the design and implementation of a variant of Lazy ML [2]. A small example program shows how imperative operations can be used in a referentially transparent way, and at the same time it highlights some of the problems with the approach. Our implementation is based on a variant of the G-machine [15, 1]. We give some benchmark figures to compare the performance of our machine with the original one. The results are disappointing: the cost of maintaining linearity in terms of lost optimisations at compile-time, and the extra data structures that must be created at run-time more than cancels out the gains made by using linear types to reduce the amount of garbage collection. We also consider how the language and the implementation can be extended to accommodate aggregates such as arrays. Here the results are more promising: linear arrays are usually more efficient than trailered ones, but they are less efficient than destructively-updated ones. We conclude that larger aggregates are the most promising area of application for Wadler's type system.