# Substructural type system

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Substructural_type_system
> Markdown URL: https://mediated.wiki/source/Substructural_type_system.md
> Source: https://en.wikipedia.org/wiki/Substructural_type_system
> Source revision: 1356581454
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Family of type systems based on substructural logic

Type systems General concepts Type safety Strong vs. weak typing Major categories Static vs. dynamic Manifest vs. inferred Nominal vs. structural Duck typing Minor categories Abstract Dependent Flow-sensitive Gradual Intersection Latent Refinement Substructural Unique Session v t e

**Substructural type systems** are a family of [type systems](/source/Type_system) analogous to [substructural logics](/source/Substructural_logic) where one or more of the [structural rules](/source/Structural_rule) are absent or only allowed under controlled circumstances. Such systems can constrain access to [system resources](/source/System_resource) such as [files](/source/Computer_file), [locks](/source/Lock_(computer_science)), and [memory](/source/Computer_memory) by keeping track of changes of state and prohibiting invalid states.[1]: 4

## Different substructural type systems

Several type systems have emerged by discarding some of the [structural rules](/source/Structural_rule) of exchange, weakening, and contraction:

Type systems Exchange Weakening Contraction Use Ordered —N/a —N/a —N/a Exactly once, in the order it was introduced Linear Allowed —N/a —N/a Exactly once Affine Allowed Allowed —N/a At most once[a] Relevant Allowed —N/a Allowed At least once Normal Allowed Allowed Allowed Arbitrarily[b]

### Ordered type system

*Ordered types* correspond to [noncommutative logic](/source/Noncommutative_logic) where exchange, contraction and weakening are discarded. This can be used to model [stack-based memory allocation](/source/Stack-based_memory_allocation) (contrast with linear types which can be used to model [heap-based memory allocation](/source/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* correspond to [linear logic](/source/Linear_logic) and ensure that objects are used exactly once. This allows the system to safely [deallocate](/source/Memory_management) an object after its use,[1]: 6 or to design [software interfaces](/source/API) that guarantee a resource cannot be used once it has been closed or transitioned to a different state.[2]

The [Clean programming language](/source/Clean_(programming_language)) makes use of [uniqueness types](/source/Uniqueness_type) (a variant of linear types) to help support concurrency, [input/output](/source/Input%2Foutput), and in-place update of [arrays](/source/Array_(data_structure)).[1]: 43

Linear type systems allow [references](/source/Reference_(computer_science)) but not [aliases](/source/Aliasing_(computing)). To enforce this, a reference goes out of [scope](/source/Scope_(programming)) after appearing on the right-hand side of an [assignment](/source/Assignment_(computer_science)), thus ensuring that only one reference to any object exists at once. Note that passing a reference as an [argument](/source/Parameter_(computer_programming)) to a [function](/source/Function_(computer_programming)) 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](/source/Quantum_computing), as it reflects the [no-cloning theorem](/source/No-cloning_theorem) of quantum states. From the [category theory](/source/Category_theory) point of view, no-cloning is a statement that there is no [diagonal functor](/source/Diagonal_functor) which could duplicate states; similarly, from the [combinatory logic](/source/Combinatory_logic) point of view, there is no K-combinator which can destroy states. From the [lambda calculus](/source/Simply_typed_lambda_calculus) point of view, a variable x can appear exactly once in a term.[3]

Linear type systems are the [internal language](/source/Internal_language) of [closed symmetric monoidal categories](/source/Closed_monoidal_category), much in the same way that [simply typed lambda calculus](/source/Simply_typed_lambda_calculus) is the language of [Cartesian closed categories](/source/Cartesian_closed_categories). More precisely, one may construct [functors](/source/Functor) 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](/source/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](/source/Relevant_logic) which allows exchange and contraction, but not weakening, which translates to every variable being used at least once.

## The resource interpretation

See also: [Linear logic § The resource interpretation](/source/Linear_logic#The_resource_interpretation)

The nomenclature offered by substructural type systems is useful to characterize [resource management](/source/Resource_management_(computing)) aspects of a language. Resource management is the aspect of language safety concerned with ensuring that each [allocated resource](/source/System_resource) is deallocated exactly once. Thus, **the resource interpretation** is only concerned with uses that transfer ownership – *moving*, where ownership is the responsibility to free the resource.

Uses that don't transfer ownership – *borrowing* – are not in scope of this interpretation, but *lifetime semantics* further restrict these uses to be between allocation and deallocation.

Type Disowning move Obligatory move Move quantification Enforcible function call state machine Normal No No Any number of times Topological ordering Affine Yes No At most once Ordering Linear Yes Yes Exactly once Ordering and completion

### Resource-affine types

Under the resource interpretation, an *affine* type cannot be spent more than once.

As an example, the same variant of [Hoare's vending machine](/source/Linear_logic#The_resource_interpretation) can be expressed in English, logic and in [Rust](/source/Rust_(programming_language)):

Vending machine 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 an 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.

In other words, an affine type system can express the [typestate pattern](/source/Typestate_analysis): Functions can consume and return an object wrapped in different types, acting like state transitions in a [state machine](/source/State_machine) that stores its state as a type in the caller's context – a *typestate*. An [API](/source/API) can exploit this to statically enforce that its functions are called in a correct order.

What it doesn't mean, however, is that a variable can't be used without using it up:

// This function just borrows a coin: The ampersand means borrow.
fn validate(_: &Coin) -> Result<(), ()> { Ok(()) }

// The same coin variable can be used infinitely many times
// as long as it is not moved.
let coin = Coin {};
loop {
    validate(&coin)?;
}

What Rust is not able to express is a coin type that cannot go out of scope – that would take a linear type.

### Resource-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 an invalid program.

{
    // Must be passed on, not dropped.
    let token = HotPotato {};

    // Suppose not every branch does away with it:
    if !queue.is_full() {
        queue.push(token);
    }

    // Compilation error: Holding an undroppable object as the scope ends.
}

An attraction with linear types is that destructors become regular functions that can take arguments, can fail and so on.[5] This may for example avoid the need to keep state that is only used for destruction. A general advantage of passing function dependencies explicitly is that the order of function calls – destruction order – becomes statically verifiable in terms of the arguments' lifetimes. Compared to internal references, this does not require lifetime annotations as in Rust.

As with manual resource management, a practical problem is that any [early return](/source/Return_early), as is typical of error handling, must achieve the same cleanup. This becomes pedantic in languages that have [stack unwinding](/source/Stack_unwinding), where every function call is a potential early return. However, as a close analogy, the semantic of implicitly inserted destructor calls can be restored with deferred function calls.[6]

### Resource-normal types

Under the resource interpretation, a *normal* type does not restrict how many times a variable can be moved from. [C++](/source/C%2B%2B) (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](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*]:

- [ATS](/source/ATS_(programming_language))

- [Clean](/source/Clean_(programming_language))

- [Idris](/source/Idris_(programming_language))

- [Mercury](/source/Mercury_(programming_language))

- [F*](/source/F*_(programming_language))

- [LinearML](https://github.com/pikatchu/LinearML)

- [Alms](http://users.eecs.northwestern.edu/~jesse/pubs/alms/)

- [Haskell](/source/Haskell) with [Glasgow Haskell Compiler](/source/Glasgow_Haskell_Compiler) (GHC) 9.0.1 or above[7]

- [Granule](https://granule-project.github.io/)

- [Rust](/source/Rust_(programming_language))

- [Swift](/source/Swift_(programming_language)) 5.9 and above[8]

## See also

- [Effect system](/source/Effect_system)

- [Linear logic](/source/Linear_logic)

- [Affine logic](/source/Affine_logic)

## Notes

1. **[^](#cite_ref-2)** The explanation for affine type systems is best understood if rephrased as “every *occurrence* of a variable is used at most once”.

1. **[^](#cite_ref-3)** Every variable may be used arbitrarily.

## References

1. ^ [***a***](#cite_ref-Walker_1-0) [***b***](#cite_ref-Walker_1-1) [***c***](#cite_ref-Walker_1-2) [***d***](#cite_ref-Walker_1-3) Walker, David (2002). "Substructural Type Systems". In [Pierce, Benjamin C.](/source/Benjamin_C._Pierce) (ed.). [*Advanced Topics in Types and Programming Languages*](https://mitpress-request.mit.edu/sites/default/files/titles/content/9780262162289_sch_0001.pdf) (PDF). MIT Press. pp. 3–43. [ISBN](/source/ISBN_(identifier)) [0-262-16228-8](https://en.wikipedia.org/wiki/Special:BookSources/0-262-16228-8).

1. **[^](#cite_ref-BernardyEtAl_4-0)** Bernardy, Jean-Philippe; Boespflug, Mathieu; Newton, Ryan R; [Peyton Jones, Simon](/source/Simon_Peyton_Jones); Spiwack, Arnaud (2017). ["Linear Haskell: practical linearity in a higher-order polymorphic language"](https://dl.acm.org/doi/pdf/10.1145/3158093). *Proceedings of the ACM on Programming Languages*. **2**: 1–29. [arXiv](/source/ArXiv_(identifier)):[1710.09756](https://arxiv.org/abs/1710.09756). [doi](/source/Doi_(identifier)):[10.1145/3158093](https://doi.org/10.1145%2F3158093). [S2CID](/source/S2CID_(identifier)) [9019395](https://api.semanticscholar.org/CorpusID:9019395).

1. **[^](#cite_ref-Baez_5-0)** Baez, John C.; Stay, Mike (2010). "Physics, Topology, Logic and Computation: A Rosetta Stone". In Springer (ed.). [*New Structures for Physics*](http://math.ucr.edu/home/baez/rosetta/rose3.pdf) (PDF). pp. 95–174.

1. **[^](#cite_ref-Ambler_6-0)** Ambler, S. (1991). [*First order logic in symmetric monoidal closed categories*](http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-194/) (PhD). U. of Edinburgh.

1. **[^](#cite_ref-7)** ["Vale's Vision"](https://vale.dev/vision/vision). Retrieved 6 December 2023. Higher RAII, a form of linear typing that enables destructors with parameters and returns.

1. **[^](#cite_ref-defer_8-0)** ["Go by Example: Defer"](https://gobyexample.com/defer). Retrieved 5 December 2023. Defer is used to ensure that a function call is performed later in a program's execution, usually for purposes of cleanup. defer is often used where e.g. *ensure* and *finally* would be used in other languages.

1. **[^](#cite_ref-9)** ["6.4.19. Linear types — Glasgow Haskell Compiler 9.7.20230513 User's Guide"](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html). *ghc.gitlab.haskell.org*. Retrieved 2023-05-14.

1. **[^](#cite_ref-10)** Hudson @twostraws, Paul. ["Noncopyable structs and enums – available from Swift 5.9"](https://www.hackingwithswift.com/swift/5.9/noncopyable-structs-and-enums). *Hacking with Swift*.

---
Adapted from the Wikipedia article [Substructural type system](https://en.wikipedia.org/wiki/Substructural_type_system) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Substructural_type_system?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.