Semantics Club 02 02 2001
This is the continuation of a talk given at the end of last year.Linear typing has been advocated as a means to evaluate programs using in-place modifications yet retaining a functional semantics. In previous work we have combined this idea with resource annotations to obtain a linearly typed functional language whose programs can be run in heap space O(x).
An annoying fact about linear typing is that it assumes that (almost) every usage of a variable is potentially modifying and therefore rules out many programs which would be perfectly ok under the in-place-update semantics. A simple example is
f(l : int list) = if sum(l)=0 then reverse(l) else lhere reverse is a function that reverses a list (in-place) and sum(l) is a function returning the sum of the integer entries of a list. The program will be ruled out by a linear type system because l is used twice, but should be accepted on the grounds that the first usage of l is "read-only".
In the past there have been several proposals to formalise "read-only" uses (eg by Wadler, Odersky, Smetsers); we add a new one which we feel is more natural and fits better into the context of resource-sensitive programming.
Our proposal gives free variables in a term one of the following three annotations depending on how the variable's content become altered.
We give rules which show how these annotations are introduced and used in order to justify certain instances of contraction, i.e., multiple usage of variables.
We prove the typing rules sound in the sense that we show that the imperative evaluation of a well-typed program computes its purely functional denotation.
We were unable to see how the typing rules fit into a well-known categorical formalism, e.g. monads, comonads, adjoints. Suggestions from the audience would be very welcome