[<<][compsci][>>][..]

Wed Oct 7 10:04:35 CEST 2009

## Linear types

I'm having a look at this survey[1] about linear types, regions and
capabilities.
At any point in time, the heap consists of a linear upper structure
(a forest), whose leafs form the boundary with a nonlinear lower
structure (an arbitrary graph).
It is possible to lift this requirement using _focus_.
Wadler noted that this is extremely restrictive. ... This leads to
an explicitly threaded programming style (i.e. `uncons' and a linear
stack of values) which is heavy and over-sequentialised.
Temporary aliasing is possible, provided there is only one remaining
pointer when a variable recovers its original linear type. (Wadler's
ad-hoc `let!' is essentially the style in which the PF primitives are
implemented.) Apparently there is a cleaner idea hidden.
Only state has to be linear, a state transformer can safely be
nonlinear. Monads are a language design in which state is implicit
and only state transformers are first-class values.
In principle one could type-check a monad's implementation using a
linear type system (it allows in-place updates) and type-check its
clients using a standard type system.
Linearity is meant to enforce the absence of aliasing. Regions are
intended to control aliasing.
Then, Baker's regions provide some annotation that can be used to
perform 1) collection at function exit and 2) in-place update for
intermediate data.
Then some about `letregion', regions that coincide with lexical scope
which with proper escape analysis can be implemented as a stack. This
then leads to type-and-effect[2] systems.
The calculus of capabilities is a low-level type-and-effect system.
Then it becomes a bit too abstract. I follow the general idea though:
distinguish pointers (shared environment) from the right to deallocate
or dereference (linear capabilities).
Skipping to the practical: Cyclone, a ``safe C'', provides fine
grained control over allocation/deallocation without sacrificing
safety.
Cyclone is a complex programming language. Simplified calculi
describe its foundations and discuss interesting connections between
linearity, regions and monads.
[1] http://lambda-the-ultimate.org/node/3581#comment
[2] http://en.wikipedia.org/wiki/Effect_system

[Reply][About]

[<<][compsci][>>][..]