Wed Oct 7 10:04:35 CEST 2009

Linear types

I'm having a look at this survey[1] about linear types, regions and

  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

  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