Data structures in programming language with linear types

Assume we are dealing with a programming language that has support for linear types (terms of linear type can be used at most once, so to say). This allows for treating some computational effects (such as mutation, even changing the type of the operand) in a way that is problematic for languages, the type systems of which operate only on "eternal truths".

Many data structures can be characterized with inductive types (lists and trees are canonical examples). If we add linear inductive types to the mix, we can also handle mutable data structures.

However, it is not clear to me how to represent data structures that exhibit sharing and cyclic references in a programming language with linear types (examples of such data structures are DAGs and other graphs, represented by adjacency lists or something else, cyclic lists). Can we do that? If it isn't possible, in which way should we extend the language so as to accommodate such data structures?

The most involved example I've found so far is a doubly-linked list. Are there other examples?

Linearity is not a sufficient constraint to pin down a unique stateful representation, and so the answer to your question depends on how you interpret linear logic in terms of state. This will typically be reflected in how you must interpret the $!A$ modality.

If your intended semantics of references says that all pointers are unique values (i.e., there is at most a single reference to an object) then dags and graph structures are not expressible, for the sort of tautological reason that a dag may contain multiple references to the same object. In this case, $!A$ must be a computation which creates a new value of type $A$, since you want maps $\delta_A : !A \multimap !A \otimes !A$ and $\epsilon_A : !A \multimap A$.

However, suppose that you want $!A$ to represent sharing. Then, objects can be garbage-collected with reference counting, with the maps $\delta_A : !A \multimap !A \otimes !A$ and $\epsilon_A : !A \multimap A$ can be realized as operations which just bump reference counts. In this case, you can't use linearity to assume that it's always safe to mutate values, since there's sharing. But you can ensure that all memory allocation is explicit in your program, and that there are no cycles in the heap.

Most practical implementations of linear types use neither of these two interpretations. Instead, references are viewed as freely duplicable entities, and what we track linearly are in fact capabilities. Capabilities are not runtime values; they are purely conceptual entities which are intended to represent the permission to access a reference. The idea is that you program in a permission-passing style, and so even if there are many references to the same object, a read or modification of a piece of state can only occur if you also have the capability to access it. And since the capability is linear, you know that only you can change it.

$$\array{ \mathsf{new} & : & \forall \alpha. \;\alpha \multimap \exists c : \iota. \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{get} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \multimap \alpha \otimes \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{set} & : & \forall \alpha, c:\iota. \;\mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \otimes \alpha \multimap \mathsf{cap}(c) \otimes \mathsf{ref}(\alpha, c) \\ \mathsf{copy} & : & \forall \alpha, c:\iota.\; \mathsf{ref}(\alpha,c) \multimap \mathsf{ref}(\alpha,c) \otimes \mathsf{ref}(\alpha,c) }$$

In the API sketched above, $c$ ranges over $\iota$, some domain of compile-time indices, and $\alpha$ ranges over types. We have a type $\mathsf{cap}(c)$ which is a capability indexed by $c$, and a type $\mathsf{ref}(\alpha, c)$, which is a type of references to $\alpha$ accessed by a capability $c$. Calling $\mathsf{get}$ and $\mathsf{set}$ on a reference requires the capability $c$, and calling $\mathsf{new}$ creates a new reference and a new capability sharing a common index. However, $\mathsf{copy}$-ing a reference does not require access to any capability, so anyone can copy a reference as long as they don't look inside it.

• Thank you for a thought-provoking answer. I'm interested though, is there a (technical) distinction between aliasing and sharing? Are there any systems that can gradually go from linear (at most one reference) to shared by at most n references to shared in an unrestricted manner? – user3722 Feb 10 '11 at 15:20
• 1. Aliasing and sharing are synonyms. 2. Yes, capability-style interpretations, augmented with Boyland's fractional permissions permit this. See also Pottier's recent work on capability calculi for theory, and Aldrich and Bierhof's work on Plural for implementation. – Neel Krishnaswami Feb 10 '11 at 19:22