Is there a use for linear logic?

Philip Wadler

University of Glasgow?

March 1991

Abstract

Past attempts to apply Girard's linear logic have either had a clear relation to the theory (Lafont, Holmstr?om, Abramsky) or a clear practical value (Guzm?an and Hudak, Wadler), but not both. This paper defines a sequence of languages based on linear logic that span the gap between theory and practice. Type reconstruction in a linear type system can derive information about sharing. An approach to linear type reconstruction based on use types is presented. Applications to the array update problem are considered.

1 Introduction

Storage reuse; single threading; in-place update; sharing analysis; linearity: any problem with so many names must be important. Girard's linear logic has intrigued computer scientists with its promise to focus new light on this old subject. (It also hints at enlightenment with regard to parallelism, but that's a topic for other papers.)

Attempts to apply linear logic fall into two camps, the theoreticians and the practitioners. On the theoretical side sit Lafont [Laf88], Holmstr?om [Hol88], and Abramsky [Abr90]. Their languages correspond to linear logic in a precise way, via the Curry-Howard isomorphism. On the practical side sit Guzm?an and Hudak [GH90] and Wadler [Wad90]. Their languages are inspired by linear logic, but the connection is of a vaguer and looser kind. (Another practioner is Wakeling, who has implemented Wadler's system [Wak90].) The goal of this paper is to build a bridge between the camps. It begins by defining a language that corresponds closely to linear logic; it is a slight variation of a language described by Abramsky [Abr90]. The suitability of this language for practical purposes is examined, and it is found to be lacking in some respects. Variants of the language are defined to remedy these shortcomings. One variant, motivated by the standard encoding

?Author's address: Department of Computing Science, University of Glasgow, G12 8QQ, Scotland. Electronic mail: [email protected].

To appear in ACM/IFIP Symposium on Partial Evaluation and Semantics Based Program Manipulation (PEPM), Yale University, June 1991.