Semantics Club 15 12 2000
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 l
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 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