The linear type system I described above, while the most common foundation discussed today, is only half of the original form of linear logic proposed by logician Jean-Yves Girard many decades ago, today called Classical Linear Logic for reasons I will not get into. This half contains the constructs that would be most recognizable to programmers. However, what we find when moving from traditional to linear type systems is that each of the type constructs programmers are familiar with actually split into two different linear type constructs. Structs and variants are one half of these split constructs, but as it turns out, their counterparts may also be of interest to programmers because they each represent a different use case of the original construct that was lost in the move to a linear type system.
The first of these constructs is the counterpart to
structs, and when placed in the proper context should be
an idea quite familiar to many programmers. The traditional
use case of structs was to group together fields
of related data, the use case that linear structs maintain.
However, the later use case was to group together operations,
a style usually associated with object-oriented programming.
Perhaps it is unsurprising that the object-oriented notion
of a class conflates grouping together data with
grouping together operations.
However, the resource interpretation forces the distinction,
because linear structs are usually the wrong construct
for grouping together operations; they imply that all
operations in the struct must be called at some point.
This is usually not what we want.
A collection of operations is usually meant to describe an interface, as potential operations that could be called, as chosen by the caller. The linear resource interpretation, then, is that exactly one of these operations must be called, and that which one is called is the choice of the caller. Thus we arrive at the counterpart of linear structs, which is best conceived of as a choice type constructor, although it can also be interpreted as a sort of linear interface in the object-oriented sense.
One complication in trying to support this construct in a Rust-like language is that it needs to store actual operations,
not just data. As Rust programmers know, Rust actually
does not have one type representing operations, but
instead creates a closure type for every
particular first-class function we require,
representing its function pointer and closed environment,
and uses its trait system to classify
all functions of a particular type.
It is actually quite easy to describe a choice as a trait:
trait MyChoice {
fn choice1(self) -> i32;
fn choice2(self) -> i64;
}
It is not so easy to build a resource using this trait though. My thinking in this setting is that much like there is anonymous function syntax to create a closure without needing to write boilerplate, we can regard choice as a sort of “generalized” closure in that it stores an environment but has multiple function pointers that can be called, all using the same stored environment. One possible syntax could look like:
let x = 3;
let c = choice{
chooseAsI32 : x + 5,
chooseAsString : format(x + 5)
};
return c.chooseAsI32();
Importantly, only the expression that gets chosen will ever get evaluated.
I am choosing to require method call syntax when actually making a choice, in order to be consistent with the idea that making a choice actually performs an operation rather than merely accessing data. It may make sense to provide a convenient syntax for specifying parameters to be used by this method call.
let x = 3;
let c = choice{
chooseAsI32 : x + 5,
chooseAsString : format(x + 5),
withParameter : |z| x + z
};
return c.withParameter(3);
This is just one hypothetical syntax and isn’t meant to be a suggestion; the concept is what matters here.
For the purposes of this document, let us also have a syntax for auto-implementing a specific choice-like trait.
let x = 3;
let c = choice MyChoice {
choice1 : x + 5,
choice2 : x + 5 as i64
};
return c.choice2();
The simplified type rules for choice:
\[\begin{matrix} G \vdash e_1 : T_1 & G \vdash e_2 : T_2 \\ \hline G \vdash \texttt{Choice}\{ \texttt{c1} : || e_1, \texttt{c2} : || e_2\} : \texttt{Choice<}T_1, T_2\texttt{>} \end{matrix}\] \[\begin{matrix} G \vdash e : \texttt{Choice<}T_1, T_2\texttt{>} \\ \hline G \vdash e\texttt{.c1}() : T_1 \end{matrix}\] \[\begin{matrix} G \vdash e : \texttt{Choice<}T_1, T_2\texttt{>} \\ \hline G \vdash e\texttt{.c2}() : T_2 \end{matrix}\]