Substructural type systems are a family of
type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
s analogous to
substructural logic
In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are r ...
s 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
Lock(s) may refer to:
Common meanings
*Lock and key, a mechanical device used to secure items of importance
*Lock (water navigation), a device for boats to transit between different levels of water, as in a canal
Arts and entertainment
* ''Lock ...
and
memory
Memory is the faculty of the mind by which data or information is encoded, stored, and retrieved when needed. It is the retention of information over time for the purpose of influencing future action. If past events could not be remembered, ...
by keeping track of changes of state that occur and preventing invalid states.
Different substructural type systems
Several type systems have emerged by discarding some of the
structural rules of exchange, weakening, and contraction:
*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
Stack (abstract data type)#Hardware_stack, Stacks in computing architectures are regions of memory (computers), memory where data is added or removed in a LIFO (computing), last-in-first-out (LIFO) manner.
In most modern computer systems, each ...
(contrast with linear types which can be used to model heap-based memory allocation). 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, or to design
software interfaces that guarantee a resource cannot be used once it has been closed or transitioned to a different state.
The
Clean programming language makes use of
uniqueness type
In computing, a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it. If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code ...
s (a variant of linear types) to help support concurrency,
input/output
In computing, input/output (I/O, or informally io or IO) is the communication between an information processing system, such as a computer, and the outside world, possibly a human or another information processing system. Inputs are the signals ...
, and in-place update of arrays.
Linear type systems allow
reference
Reference is a relationship between objects in which one object designates, or acts as a means by which to connect to or link to, another object. The first object in this relation is said to ''refer to'' the second object. It is called a '' name'' ...
s but not
alias
Alias may refer to:
* Pseudonym
* Pen name
* Nickname
Arts and entertainment Film and television
* ''Alias'' (2013 film), a 2013 Canadian documentary film
* ''Alias'' (TV series), an American action thriller series 2001–2006
* ''Alias the ...
es. To enforce this, a reference goes out of
scope
Scope or scopes may refer to:
People with the surname
* Jamie Scope (born 1986), English footballer
* John T. Scopes (1900–1970), central figure in the Scopes Trial regarding the teaching of evolution
Arts, media, and entertainment
* Cinem ...
after appearing on the right-hand side of an
assignment
Assignment, assign or The Assignment may refer to:
* Homework
* Sex assignment
* The process of sending National Basketball Association players to its development league; see
Computing
* Assignment (computer science), a type of modification to ...
, thus ensuring that only one reference to any object exists at once. Note that passing a reference as an
argument
An argument is a statement or group of statements called premises intended to determine the degree of truth or acceptability of another statement called conclusion. Arguments can be studied from three main perspectives: the logical, the dialectic ...
to a
function
Function or functionality may refer to:
Computing
* Function key, a type of key on computer keyboards
* Function model, a structured representation of processes in a system
* Function object or functor or functionoid, a concept of object-oriente ...
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.
A linear type system is similar to
C++
C++ (pronounced "C plus plus") is a high-level general-purpose programming language created by Danish computer scientist Bjarne Stroustrup as an extension of the C programming language, or "C with Classes". The language has expanded significan ...
's
unique_ptr class
Class or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used differentl ...
, which behaves like a pointer but can only be moved (i.e. not copied) in an assignment. Although the linearity constraint is checked at
compile time
In computer science, compile time (or compile-time) describes the time window during which a computer program is compiled.
The term is used as an adjective to describe concepts related to the context of program compilation, as opposed to concept ...
, dereferencing an invalidated unique_ptr causes undefined behavior at
run-time. Similarly, the
Rust
Rust is an iron oxide, a usually reddish-brown oxide formed by the reaction of iron and oxygen in the catalytic presence of water or air moisture. Rust consists of hydrous iron(III) oxides (Fe2O3·nH2O) and iron(III) oxide-hydroxide (FeO(OH ...
programming language has partial support to linear types through the use of lint annotations but differently from C++ the moved from variable cannot be used again.
The single-reference property makes linear type systems suitable as programming languages for
quantum computation, as it reflects the
no-cloning theorem In physics, the no-cloning theorem states that it is impossible to create an independent and identical copy of an arbitrary unknown quantum state, a statement which has profound implications in the field of quantum computing among others. The theore ...
of quantum states. From the
category theory point of view, no-cloning is a statement that there is no
diagonal functor In category theory, a branch of mathematics, the diagonal functor \mathcal \rightarrow \mathcal \times \mathcal is given by \Delta(a) = \langle a,a \rangle, which maps objects as well as morphisms. This functor can be employed to give a succinct al ...
which could duplicate states; similarly, from the
combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comput ...
point of view, there is no K-combinator which can destroy states. From the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
point of view, a variable ''x'' can appear exactly once in a term.
Linear type systems are the
internal language
__NOTOC__
Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science.
In broad terms, categ ...
of
closed symmetric monoidal categories, much in the same way that
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
is the language of
Cartesian closed categories
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in ma ...
. More precisely, one may construct
functor
In mathematics, specifically category theory, a functor is a Map (mathematics), mapping between Category (mathematics), categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) ar ...
s between the category of linear type systems and the category of closed symmetric monoidal categories.
Affine type systems
Affine types are a version of linear types allowing to ''discard'' (i.e. ''not use'') a resource, corresponding to
affine logic 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.
The name "affine logic" is associated with linear logic, to which it differs by all ...
. 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 Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but ...
which allows exchange and contraction, but not weakening, which translates to every variable being used at least once.
Programming languages
The following programming languages support linear or affine types:
*
C++
C++ (pronounced "C plus plus") is a high-level general-purpose programming language created by Danish computer scientist Bjarne Stroustrup as an extension of the C programming language, or "C with Classes". The language has expanded significan ...
*
ATS
*
Clean
*
Idris
*
Mercury
*
F*
LinearMLAlms*
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
with
GHC 9.0.1 or above.
Linear types
/ref>
Granule
* Rust
Rust is an iron oxide, a usually reddish-brown oxide formed by the reaction of iron and oxygen in the catalytic presence of water or air moisture. Rust consists of hydrous iron(III) oxides (Fe2O3·nH2O) and iron(III) oxide-hydroxide (FeO(OH ...
* Nim
See also
* Effect system
In computing, an effect system is a formal system that describes the computational effects of computer programs, such as side effects. An effect system can be used to provide a compile-time check of the possible effects of the program.
The effect ...
* Linear logic
* Affine logic 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.
The name "affine logic" is associated with linear logic, to which it differs by all ...
Notes
References
*
*
*
* {{cite book , last1=Baez , first1=John C. , last2=Stay , first2=Mike , url=http://math.ucr.edu/home/baez/rosetta/rose3.pdf , chapter=Physics, Topology, Logic and Computation: A Rosetta Stone , date=2010 , title=New Structures for Physics , editor=Springer , pages=95–174
Type theory