Substructural type system

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 can constrain access to system resources such as files, locks, and memory by keeping track of changes of state and prohibiting invalid states.

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 can constrain access to system resources such as files, locks, and memory by keeping track of changes of state and prohibiting invalid states. 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: Functions can consume and return an object wrapped in different types, acting like state transitions in a state machine that stores its state as a type in the caller's context – a typestate. An 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. { // 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. 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, as is typical of error handling, must achieve the same cleanup. This becomes pedantic in languages that have 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. auto coin = std::unique_ptr (); auto candy = buy_candy(std::move(coin)); auto drink = buy_drink(std::move(coin)); // This is valid C++. ==See also== Effect system Linear logic Affine logic ==Notes==

Text derived from https://en.wikipedia.org/w/index.php?oldid=1369973577 under CC BY-SA 4.0; modifications have been made.