| Type systems |
|---|
| General concepts |
| Major categories |
|
| Minor categories |
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. [1] : 4
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 |
The explanation for affine type systems is best understood if rephrased as “every occurrence of a variable is used at most once”.
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 types correspond to linear logic and ensure 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 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 types correspond to relevant logic which allows exchange and contraction, but not weakening, which translates to every variable being used at least once.
The nomenclature offered by substructural type systems is useful to characterize resource management aspects of a language. Resource management is the aspect of language safety concerned with ensuring that each allocated 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.
| Disowning move | Obligatory move | Move quantification | Enforcible function call state machine | |
|---|---|---|---|---|
| Normal type | No | No | Any number of times | Topological ordering |
| Affine type | Yes | No | At most once | Ordering |
| Linear type | Yes | Yes | Exactly once | Ordering and completion |
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 ⊸ ⊤ | fnbuy_candy(_: Coin)-> Candy{Candy{}}fnbuy_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:
letcoin=Coin{};letcandy=buy_candy(coin);// The lifetime of the coin variable ends here.letdrink=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.fnvalidate(_: &Coin)-> Result<(),()>{Ok(())}// The same coin variable can be used infinitely many times// as long as it is not moved.letcoin=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.
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.lettoken=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, 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. [6]
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.
autocoin=std::unique_ptr<Coin>();autocandy=buy_candy(std::move(coin));autodrink=buy_drink(std::move(coin));// This is valid C++.The following programming languages support linear or affine types[ citation needed ]:
In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument.
Affine may describe any of various topics concerned with connections or affinities.
It may refer to:
In logic, a substructural logic is a logic lacking one of the usual structural rules, such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are relevance logic and linear logic.
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.
Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening.
Noncommutative logic is an extension of linear logic that combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek calculus. Its sequent calculus relies on the structure of order varieties, and the correctness criterion for its proof nets is given in terms of partial permutations. It also has a denotational semantics in which formulas are interpreted by modules over some specific Hopf algebras.
Resource acquisition is initialization (RAII) is a programming idiom used in several object-oriented, statically typed programming languages to describe a particular language behavior. In RAII, holding a resource is a class invariant, and is tied to object lifetime. Resource allocation is done during object creation, by the constructor, while resource deallocation (release) is done during object destruction, by the destructor. In other words, resource acquisition must succeed for initialization to succeed. Thus the resource is guaranteed to be held between when initialization finishes and finalization starts, and to be held only when the object is alive. Thus if there are no object leaks, there are no resource leaks.
In the logical discipline of proof theory, a structural rule is an inference rule of a sequent calculus that does not refer to any logical connective but instead operates on the sequents directly. Structural rules often mimic the intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as substructural logics.
Categorial grammar is a family of formalisms in natural language syntax that share the central assumption that syntactic constituents combine as functions and arguments. Categorial grammar posits a close relationship between the syntax and semantic composition, since it typically treats syntactic categories as corresponding to semantic types. Categorial grammars were developed in the 1930s by Kazimierz Ajdukiewicz and in the 1950s by Yehoshua Bar-Hillel and Joachim Lambek. It saw a surge of interest in the 1970s following the work of Richard Montague, whose Montague grammar assumed a similar view of syntax. It continues to be a major paradigm, particularly within formal semantics.
Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.
In computer science, a programming language is said to have first-class functions if it treats functions as first-class citizens. This means the language supports passing functions as arguments to other functions, returning them as the values from other functions, and assigning them to variables or storing them in data structures. Some programming language theorists require support for anonymous functions as well. In languages with first-class functions, the names of functions do not have any special status; they are treated like ordinary variables with a function type. The term was coined by Christopher Strachey in the context of "functions as first-class citizens" in the mid-1960s.
In mathematics, especially in category theory, a closed monoidal category is a category that is both a monoidal category and a closed category in such a way that the structures are compatible.
In computer programming, an automatic variable is a local variable which is allocated and deallocated automatically when program flow enters and leaves the variable's scope. The scope is the lexical context, particularly the function or block in which a variable is defined. Local data is typically invisible outside the function or lexical context where it is defined. Local data is also invisible and inaccessible to a called function, but is not deallocated, coming back in scope as the execution thread returns to the caller.
In object-oriented programming, a destructor is a method which is invoked mechanically just before the memory of the object is released. It can happen when its lifetime is bound to scope and the execution leaves the scope, when it is embedded in another object whose lifetime ends, or when it was allocated dynamically and is released explicitly. Its main purpose is to free the resources which were acquired by the object during its life and/or deregister from other entities which may keep references to it. Use of destructors is needed for the process of Resource Acquisition Is Initialization (RAII).
Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.
T-norm fuzzy logics are a family of non-classical logics, informally delimited by having a semantics that takes the real unit interval [0, 1] for the system of truth values and functions called t-norms for permissible interpretations of conjunction. They are mainly used in applied fuzzy logic and fuzzy set theory as a theoretical basis for approximate reasoning.
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic logic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a 1958 special issue dedicated to Paul Bernays on his 70th birthday.
Pregroup grammar (PG) is a grammar formalism intimately related to categorial grammars. Much like categorial grammar (CG), PG is a kind of type logical grammar. Unlike CG, however, PG does not have a distinguished function type. Rather, PG uses inverse types combined with its monoidal operation.
Higher RAII, a form of linear typing that enables destructors with parameters and returns.
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.