Martin Hofmann, David Aspinall
Linear typing schemes guarantee single-theadedness and hence the
soundness of in-place update with respect to a functional semantics.
But linear schemes are restrictive in practice, and more restrictive
than necessary to guarantee the soundness of in-place update. This
has prompted research into additional static analysis or more
sophisticated typing disciplines, to determine when in-place update
may be safely used, or to combine linear and non-linear schemes. This
workcontributes to this line of research.
We propose a new typing scheme which better approximates the semantic
property of soundness of in-place update for a functional
semantics. Our typing scheme includes both tensor and cartesian
products, which allows data structures with or without sharing to be
defined. We begin from the familiar observation that some data is used
only in a ``read-only'' context after which it may be safely re-used
before being destroyed. A formalization of our translation into
in-place update together with a machine model semantics allows us to
refine this observation. We consider three usage aspects apparent
from the semantics, which are used to annotate function argument
types. The aspects are (1)~used destructively, (2)~used read-only but
shared with result, and (3)~used read-only and not shared.