support for linear values/data

[GoogleCodeExporter]

This is a rather vague feature request.

Basis is the substructural type system for a region based memory management 
system from 
Matthew Flatt's thesis.

The gist is this:

a0 = newRegion
(r0, a1) = newRef a0
r1 = stroreRef r0 val
(v, r2) = readRef r1
dropRef r2

The rN and aN can be used (exactly/at most) once. This guarantees the region 
system's 
soundness.

My first idea that syntactically this could be modelled like the "lazy" 
modifier on values, perhaps 
adding "linear" modifier on the value's type.

then newRegion's type would become

newRegion :: linear Region

and

newRef :: Region -> (linear Reference, linear Region)

Just an idea.

Original issue reported on code.google.com by ggr...@gmail.com on 26 Jul 2007 at 2:35

[GoogleCodeExporter]

link: http://ttic.uchicago.edu/~fluet/research/thesis/index.html

Original comment by ggr...@gmail.com on 26 Jul 2007 at 2:41

• Changed state: New

[GoogleCodeExporter]

more indication that this is a useful concept:

<http://lambda-the-ultimate.org/node/2818>

(regrettably I did not read this paper, yet)

Original comment by ggr...@gmail.com on 22 May 2008 at 12:10

[GoogleCodeExporter]

Possible implementation.

Introduce a type function

linear :: a ~> a
{linear a} = primitive

It is basically an 'identity view' on the datatype, but with special 
unification behavior, namely {linear a} expanding to a "Linear" TcTv, which 
accepts only one unification, and rejects others. The inner 'a' behaves 
normally.

Original comment by ggr...@gmail.com on 13 Jan 2011 at 10:46

[GoogleCodeExporter]

Idea for the syntax: {1 Int} or even {Int} for the linear modality.

Original comment by ggr...@gmail.com on 20 Jan 2011 at 10:02