Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to system resources such as files, locks, and memory by keeping track of changes of state that occur and preventing invalid states.[1]: 4
Different substructural type systems
Several type systems have emerged by discarding some of the structural rules of exchange, weakening, and contraction:
| Exchange | Weakening | Contraction | Use | |
|---|---|---|---|---|
| Ordered | — | — | — | Exactly once in order |
| Linear | Allowed | — | — | Exactly once |
| Affine | Allowed | Allowed | — | At most once |
| Relevant | Allowed | — | Allowed | At least once |
| Normal | Allowed | Allowed | Allowed | Arbitrarily |
- Ordered type systems (discard exchange, weakening and contraction): Every variable is used exactly once in the order it was introduced.
- Linear type systems (allow exchange, but neither weakening nor contraction): Every variable is used exactly once.
- Affine type systems (allow exchange and weakening, but not contraction): Every variable is used at most once.
- Relevant type systems (allow exchange and contraction, but not weakening): Every variable is used at least once.
- Normal type systems (allow exchange, weakening and contraction): Every variable may be used arbitrarily.
The explanation for affine type systems is best understood if rephrased as “every occurrence of a variable is used at most once”.
Ordered type system
Ordered types correspond to noncommutative logic where exchange, contraction and weakening are discarded. This can be used to model stack-based memory allocation (contrast with linear types which can be used to model heap-based memory allocation).[1]: 30–31 Without the exchange property, an object may only be used when at the top of the modelled stack, after which it is popped off, resulting in every variable being used exactly once in the order it was introduced.
Linear type systems
Linear types corresponds to linear logic and ensures that objects are used exactly once. This allows the system to safely deallocate an object after its use,[1]: 6 or to design software interfaces that guarantee a resource cannot be used once it has been closed or transitioned to a different state.[2]
The Clean programming language makes use of uniqueness types (a variant of linear types) to help support concurrency, input/output, and in-place update of arrays.[1]: 43
Linear type systems allow references but not aliases. To enforce this, a reference goes out of scope after appearing on the right-hand side of an assignment, thus ensuring that only one reference to any object exists at once. Note that passing a reference as an argument to a function is a form of assignment, as the function parameter will be assigned the value inside the function, and therefore such use of a reference also causes it to go out of scope.
The single-reference property makes linear type systems suitable as programming languages for quantum computing, as it reflects the no-cloning theorem of quantum states. From the category theory point of view, no-cloning is a statement that there is no diagonal functor which could duplicate states; similarly, from the combinatory logic point of view, there is no K-combinator which can destroy states. From the lambda calculus point of view, a variable x can appear exactly once in a term.[3]
Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories.[4]
Affine type systems
Affine types are a version of linear types allowing to discard (i.e. not use) a resource, corresponding to affine logic. An affine resource can be used at most once, while a linear one must be used exactly once.
Relevant type system
Relevant types correspond to relevant logic which allows exchange and contraction, but not weakening, which translates to every variable being used at least once.
The resource interpretation
Most programming languages are not characterizable in this nomenclature by how many times a variable can be used, in the literal sense, but specifically disowned (by move or destroy).
Resource management is the aspect of language safety concerned with ensuring that each resource allocation is deallocated exactly once. This motivates protecting variables that hold resources from incorrect or accidental copying or discarding, as well as distinguishing ownership transfer from other variable uses. A type system that facilitates this may offer notions of responsibility for destruction – ownership, transfer of ownership – move and extent of ownership – lifetime as well as uses without ownership transfer – borrowing. To characterize these aspects of a language, it is therefore useful to bend the definition of use in the definition to mean ending the lifetime of a variable.
Affine types
Under the resource interpretation, an affine type can not be spent more than once.
As an example, the same variant of Hoare's vending machine can be expressed in English, logic and in Rust:
| English | Logic | Rust |
|---|---|---|
| A coin can buy you a piece of candy, a drink, or go out of scope. |
Coin ⊸ Candy Coin ⊸ Drink Coin ⊸ ⊤ |
fn buy_candy(_: Coin) -> Candy { Candy{} }
fn buy_drink(_: Coin) -> Drink { Drink{} }
|
What it means for Coin to be a affine type in this example (which it is unless it implements the Copy trait) is that trying to spend the same coin twice is an invalid program that the compiler is entitled to reject:
let coin = Coin{};
let candy = buy_candy(coin); // The lifetime of the coin variable ends here.
let drink = buy_drink(coin); // Compilation error: Use of moved variable that does not possess the Copy trait.
This demonstrates that an affine type system is able to express the typestate pattern: An API designer can use types consumed and returned by functions to model allowable state transitions of an underlying state that the API abstracts, thereby enforcing correct use of the API at compile time.
What it doesn't mean, however, is that a variable can't be used without using it up:
// The ampersand means borrow: This function just borrows a coin.
fn validate(_: &Coin) -> Result<(), ()> { Ok(()) }
// The same coin can be used indefinitely:
let coin = Coin{};
loop {
validate(&coin)?;
}
What Rust is not able to express is a coin type that may not go out of scope – that would take a linear type.
Linear types
Under the resource interpretation, a linear type not only can be moved, like an affine type, but must be moved – going out of scope is a compilation error.
{
// Must be passed on, not dropped.
let hot_potato = HotPotato{};
// Suppose we fail to pass it to a function that accepts it:
//accept(hot_potato);
// Compilation error: We must not hold a HotPotato object as the scope ends.
}
Normal types
Under the resource interpretation, a normal type does not restrict how many times a variable can be moved from. C++ (specifically nondestructive move semantics) falls in this category.
auto coin = std::unique_ptr<Coin>();
auto candy = buy_candy(std::move(coin));
auto drink = buy_drink(std::move(coin)); // This is valid C++.
Programming languages
The following programming languages support linear or affine types[citation needed]:
See also
References
- ^ a b c d Walker, David (2002). "Substructural Type Systems". In Pierce, Benjamin C. (ed.). Advanced Topics in Types and Programming Languages (PDF). MIT Press. pp. 3–43. ISBN 0-262-16228-8.
- ^ Bernardy, Jean-Philippe; Boespflug, Mathieu; Newton, Ryan R; Peyton Jones, Simon; Spiwack, Arnaud (2017). "Linear Haskell: practical linearity in a higher-order polymorphic language". Proceedings of the ACM on Programming Languages. 2: 1–29. arXiv:1710.09756. doi:10.1145/3158093. S2CID 9019395.
- ^ Baez, John C.; Stay, Mike (2010). "Physics, Topology, Logic and Computation: A Rosetta Stone". In Springer (ed.). New Structures for Physics (PDF). pp. 95–174.
- ^ Ambler, S. (1991). First order logic in symmetric monoidal closed categories (PhD). U. of Edinburgh.
- ^ "6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide". ghc.gitlab.haskell.org. Retrieved 2023-05-14.