Observers for Linear Types

Martin Odersky

European Symposium on Programming, February 1992

Linear types provide the framework for a safe embedding of mutable
state in functional languages by enforcing the principle that
variables of linear type must be used exactly once. A potential
disadvantage of this approach is that it places read accesses to such
variables under the same restriction as write accesses, and thus
prevents reads to proceed in parallel.  We present here an extension
of linear types which augments the usual distinction between linear
and non-linear by a third state, {\em observers} of linear variables.
Since, unlike linear variables, observers can be duplicated, multiple
concurrent reads are made possible.  On the other hand, 
observers must be short-lived enough to never overlap
with mutations.  The resulting type system is in many aspects similar
to the one of ML: It is polymorphic, has principal types, and admits
a type reconstruction algorithm.