Linear Types and Program Resource Management
Resources and life cycles
Linear types and values
a = b;
Resource categories

Can the value be copied and destroyed trivially?
If yes: value belongs to category 1; this category includes all values which are merely bit patterns of fixed size: integral and floatingpoint numbers, booleans, characters, enumeration values, bit masks.

If no (it requires cleanup): are the point(s) of cleanup in the
program statically known?
If yes: (category 2) the value is used linearly, and can be (explicitly) disposed of at the appropriate place(s).

If no (the points of cleanup are not statically known): is the value immutable?
If yes: (category 3) the value can be either copied in its entirety, and the copies disposed of individually (3a); or the value can be managed through reference counting (3b), in which case a "copy" action consists of incrementing its reference count, and a "destroy" action consists of decrementing its reference count and optionally (if the count reaches zero) disposing of the value.

If no (the value is shared and mutable): is the value used from a
single thread only (or, more generally, is it only used in scope of
a specific other value which is used linearly)?
If yes: (category 4) the value can be put in a heap which is linearly owned (i.e., only accessible from one thread at a time).

If no (the value is mutable and shared between threads):
(category 5) the value can be protected by a lock; the lock is
reference counted and its disposal causes the value to be disposed.

Atoms and small integers are contained in a single machine word and
are simply copied (category 1).

Process contexts are linear (category 2), and is disposed of at
specific program points.

Message between processes are copied (category 3a).

Large binary values are managed through reference counting (category 3b).

Other Erlang terms (tuples, lists, bignums, small binaries, etc.) live
in a heap which belongs to a process which is a linear value (category 4).

Finally, certain data structures: the process registry, nonprivate tables,
etc., which are mutable and shared among processes, are managed
through the use of locks (category 5).
Intermezzo: Type notation

A ⊗ B is a linear product type — which is like a traditional
product type (aka record, struct, or tuple type, depending on language) type
except that each of its fields must be used (consumed) exactly once.

A ⊕ B is a linear sum type — which is like a normal sum type (aka tagged
union, algebraic datatype, etc.) except that the value it contains
(whichever of the variants it is) must be consumed exactly once.

∀T.A(T) is universal quantification — aka. parametric polymorphism
or generics, which is used for e.g. generic container types.

∃T.A(T) is existential quantification — such as can be used for
subtype polymorphism or typeclasses, but in what follows will be
used in a more general manner.
Resource management in a linear virtual machine
Category 1: bit patterns
copy : T → T ⊗ T dispose : T → ()
Category 2: linear values
Category 3a: resource copying
copy : T → T ⊗ T dispose : T → ()
Category 3b: reference counting
copy : T → T ⊗ T dispose : T → ()
Category 4: (defered)
Category 5: lockprotection
copy and dispose works as for a reference counted value. acquire and release work the lock.
copy : LockedT → LockedT ⊗ LockedT copy : T → T ⊗ LockedT dispose : LockedT → () acquire : LockedT → T acquire : LockedT ⊗ Timeout → T ⊕ LockedT release : T → LockedT
Category 4: heap allocation in linearly owned heap

At allocation time, the garbage collector must know all of the root
objects in the heap, in order to preserve all reachable values;

At allocation time, the location of all live pointers into the heap
must be known to the garbage collector, so that it can adjust them
appropriately when it moves objects.
Heap[h,a]
HeapPtr[T,a]
access_field : ∀h.∀a. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ F
dispose : ∀T.∀a. HeapPtr[T,a] → ()
allocate : ∀h.∀a. Heap[h,a] ⊗ _A_ ⊗ _B_ → ∃b.Heap[h,b]
RootPtr[T,h]
register_root : ∀h.∀a.∀T. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ RootPtr[T,h] read_root : ∀h.∀a.∀T. Heap[h,a] ⊗ RootPtr[T,h] → Heap[h,a] ⊗ HeapPtr[T,a] dispose_root : ∀h.∀T. RootPtr[T,h] → ()
create_heap : () → ∃h.∃a. Heap[h,a] dispose : ∀h.∀a. Heap[h,a] → ()