Type theory

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

Type theory is closely related to (and in some cases overlaps with) type systems, which are a programming language feature used to reduce bugs. Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems.

Two well-known type theories that can serve as mathematical foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory.


Between 1902 and 1908 Bertrand Russell proposed various "theories of type" in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. By 1908 Russell arrived at a "ramified" theory of types together with an "axiom of reducibility" both of which featured prominently in Whitehead and Russell's Principia Mathematica published between 1910 and 1913. They attempted to resolve Russell's paradox by first creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself. In the 1920s, Leon Chwistek and Frank P. Ramsey proposed an unramified type theory, now known as the "theory of simple types" or "simple type theory", that collapsed the hierarchy of the types in the earlier ramified theory and as such did not require the axiom of reducibility.

The common usage of "type theory" is when those types are used with a term rewrite system. The most famous early example is Alonzo Church's simply typed lambda calculus. Church's theory of types[1] helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a foundation of mathematics and it was referred to as a higher-order logic.

Some other type theories include Per Martin-Löf's intuitionistic type theory, which has been the foundation used in some areas of constructive mathematics and for the proof assistant Agda. Thierry Coquand's calculus of constructions and its derivatives are the foundation used by Coq and others. The field is an area of active research, as demonstrated by homotopy type theory.

Basic concepts

In a system of type theory, each term has a type. For example, , , and are all separate terms with the type for natural numbers. Traditionally, the term is followed by a colon and its type, such as .

Type theories have explicit computation and it is encoded in rules for rewriting terms. These are called conversion rules or, if the rule only works in one direction, a reduction rule. For example, and are syntactically different terms, but the former reduces to the latter. This reduction is written .

Functions in type theory have a special reduction rule: the argument of the function call gets substituted for every occurrence of the parameter in the function definition. Let's say the function is defined as (using Church's lambda notation) or (using a more modern notation). Then, the function call would be reduced by substituting for every copy of in the body of the function definition. Thus, .

The type of a function is denoted with an arrow from the parameter type to the function's resulting type. Thus, . Calling or "applying" a function to an argument may be written with or without parentheses, so or . Not using parentheses is more common, because multiple argument functions can be defined using currying.

Difference from set theory

There are many different set theories and many different systems of type theory, so what follows are generalizations.

  • Set theory is built on top of logic. It requires a separate system like predicate logic underneath it. In type theory, concepts like "and" and "or" can be encoded as types in the type theory itself.
  • In set theory, an element can belong to multiple sets, either to a subset or to a superset. In type theory, terms (generally) belong to only one type. (Where a subset would be used, type theory tends to use a predicate function that returns true if the term is in the subset and returns false if the value is not. The union of two types can be done by creating a new type called a sum type, which contains new terms.)
  • Set theory usually encodes numbers as sets. (0 is the empty set, 1 is a set containing the empty set, etc. See Set-theoretic definition of natural numbers.) Type theory can encode numbers as functions using Church encoding or more naturally as inductive types. Inductive types create new constants for the successor function and zero, and closely resembles Peano's axioms.
  • Set theory allows set builder notation.
  • Type theory has a simple connection to constructive mathematics through the BHK interpretation. It can be connected to logic by the Curry Howard isomorphism. And some type theories are closely connected to Category theory.

Optional features


The term reduces to . Since cannot be reduced further, it is called a normal form. A system of type theory is said to be strongly normalizing if all terms have a normal form and any order of reductions reaches it. Weakly normalizing systems have a normal form but some orders of reductions may loop forever and never reach it.

For a normalizing system, some borrow the word element from set theory and use it to refer to all closed terms that can reduce to the same normal form. A closed term is one without parameters. (A term like with its parameter is called an open term.) Thus, and may be different terms but they are both from the element .

A similar idea that works for open and closed terms is convertibility. Two terms are convertible if there exists a term that they both reduce to. For example, and are convertible. As are and . However, and (where is a free variable) are not because both are in normal form and they are not the same. Confluent and weakly normalizing systems can test if two terms are convertible by checking if they both reduce to the same normal form.

Dependent types

A dependent type is a type that depends on a term or on another type. Thus, the type returned by a function may depend upon the argument to the function.

For example, a list of s of length 4 may be a different type than a list of s of length 5. In a type theory with dependent types, it is possible to define a function that takes a parameter "n" and returns a list containing "n" zeros. Calling the function with 4 would produce a term with a different type than if the function was called with 5.

Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like Idris, ATS, Agda and Epigram.

Equality types

Many systems of type theory have a type that represents equality of types and of terms. This type is different from convertibility, and is often denoted propositional equality.

In intuitionistic type theory, the equality type (also called the identity type) is known as for identity. There is a type when is a type and and are both terms of type . A term of type is interpreted as meaning that is equal to .

In practice, it is possible to build a type but there will not exist a term of that type. In intuitionistic type theory, new terms of equality start with reflexivity. If is a term of type , then there exists a term of type . More complicated equalities can be created by creating a reflexive term and then doing a reduction on one side. So if is a term of type , then there is a term of type and, by reduction, generate a term of type . Thus, in this system, the equality type denotes that two values of the same type are convertible by reductions.

Having a type for equality is important because it can be manipulated inside the system. There is usually no judgement to say two terms are not equal; instead, as in the Brouwer–Heyting–Kolmogorov interpretation, we map to , where is the bottom type having no values. There exists a term with type , but not one of type .

Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type.

Inductive types

A system of type theory requires some basic terms and types to operate on. Some systems build them out of functions using Church encoding. Other systems have inductive types: a set of base types and a set of type constructors that generate types with well-behaved properties. For example, certain recursive functions called on inductive types are guaranteed to terminate.

Coinductive type are infinite data types created by giving a function that generates the next element(s). See Coinduction and Corecursion.

Induction-induction is a feature for declaring an inductive type and a family of types that depends on the inductive type.

Induction recursion allows a wider range of well-behaved types, allowing the type and recursive functions operating on it to be defined at the same time.

Universe types

Types were created to prevent paradoxes, such as Russell's paradox. However, the motives that lead to those paradoxes—being able to say things about all types—still exist. So, many type theories have a "universe type", which contains all other types (and not itself).

In systems where you might want to say something about universe types, there is a hierarchy of universe types, each containing the one below it in the hierarchy. The hierarchy is defined as being infinite, but statements must only refer to a finite number of universe levels.

Type universes are particularly tricky in type theory. The initial proposal of intuitionistic type theory suffered from Girard's paradox.

Computational component

Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages. That is, they are said to have a "computational component". The computation is the reduction of terms of the language using rewriting rules.

A system of type theory that has a well-behaved computational component also has a simple connection to constructive mathematics through the BHK interpretation.

Non-constructive mathematics in these systems is possible by adding operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity.

Type theories




Practical impact

Programming languages

There is extensive overlap and interaction between the fields of type theory and type systems. Type systems are a programming language feature designed to identify bugs. Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory.

A prime example is Agda, a programming language which uses intuitionistic type theory for its type system. The programming language ML was developed for manipulating type theories (see LCF) and its own type system was heavily influenced by them.

Mathematical foundations

The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is current research into mathematical foundations using homotopy type theory.

Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS).[2] Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).

Proof assistants

Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:

Multiple type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.


Type theory is also widely in use in formal theories of semantics of natural languages, especially Montague grammar and its descendants. In particular, categorial grammars and pregroup grammars make extensive use of type constructors to define the types (noun, verb, etc.) of words.

The most common construction takes the basic types and for individuals and truth-values, respectively, and defines the set of types recursively as follows:

  • if and are types, then so is ;
  • nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type is the type of functions from entities of type to entities of type . Thus one has types like which are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like everybody or nobody (Montague 1973, Barwise and Cooper 1981).

Social sciences

Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.

Relation to category theory

Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections. As John Lane Bell writes: "In fact categories can themselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:[3]

The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

See also


  1. ^ Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
  2. ^ ETCS in nLab
  3. ^ John L. Bell (2012). "Types, Sets and Categories" (PDF). In Akihiro Kanamory. Handbook of the History of Logic. Volume 6. Sets and Extensions in the Twentieth Century. Elsevier. ISBN 978-0-08-093066-4.


Further reading

  • C. Aarts, R. Backhouse, P. Hoogendijk, E. Voermans & J. van der Woude (December 1992) A Relational Theory of Datatypes via ResearchGate
  • Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
  • Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 978-0-444-50170-7. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
  • Cardelli, Luca, 1997, "Type Systems," in Allen B. Tucker, ed., The Computer Science and Engineering Handbook. CRC Press: 2208–2236.
  • Collins, Jordan E. (2012). A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing. hdl:11375/12315. ISBN 978-3-8473-2963-3. Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
  • Constable, Robert L., 2002, "Naïve Computational Type Theory," in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213–259. Intended as a type theory counterpart of Paul Halmos's (1960) Naïve Set Theory
  • Thierry CoquandType Theory, Stanford Encyclopedia of Philosophy.
  • Thompson, Simon, 1991. Type Theory and Functional Programming. Addison–Wesley. ISBN 0-201-41667-0.
  • J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press, 2008, ISBN 0-521-05422-2 (also 1995, 1997). A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review
  • Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, A modern perspective on type theory: from its origins until today, Springer, 2004, ISBN 1-4020-2334-0
  • José Ferreirós, José Ferreirós Domínguez, Labyrinth of thought: a history of set theory and its role in modern mathematics, Edition 2, Springer, 2007, ISBN 3-7643-8349-6, chapter X "Logic and Type Theory in the Interwar Period".
  • T. D. L. Laan, The evolution of type theory in logic and mathematics, PhD thesis, Eindhoven University of Technology, 1997.

External links

Algebraic data type

In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

Two common classes of algebraic types are product types (i.e., tuples and records) and sum types (i.e., tagged or disjoint unions or variant types).The values of a product type typically contain several values, called fields. All values of that type have the same combination of field types. The set of all possible values of a product type is the set-theoretic product, i.e., the Cartesian product, of the sets of all possible values of its field types.

The values of a sum type are typically grouped into several classes, called variants. A value of a variant type is usually created with a quasi-functional entity called a constructor. Each variant has its own constructor, which takes a specified number of arguments with specified types. The set of all possible values of a sum type is the set-theoretic sum, i.e., the disjoint union, of the sets of all possible values of its variants. Enumerated types are a special case of sum types in which the constructors take no arguments, as exactly one value is defined for each constructor.

Values of algebraic types are analyzed with pattern matching, which identifies a value by its constructor or field names and extracts the data it contains.

Algebraic data types were introduced in Hope, a small functional programming language developed in the 1970s at the University of Edinburgh.

Blood type personality theory

A pseudoscientific belief exists in Japan and South Korea, that a person's ABO blood type is predictive of a person's personality, temperament, and compatibility with others. This superstition is similar to how astrological signs are perceived as influencing factors in a person's life in other countries.

One of the reasons Japan developed the blood type personality indicator theory was in reaction against ethnic stereotypes coming from Europe. The popular belief originates with publications by Masahiko Nomi in the 1970s.

The scientific community generally dismisses blood type personality theories as a superstition or pseudoscience because of lack of evidence or testable criteria. Although research into the causal link between blood type and personality is limited, research does not demonstrate any statistically significant association between the two. Some studies suggest that there is a statistically significant relationship between blood type and personality, although it is unclear if this is simply due to a self-fulfilling prophecy. Recently, some medical hypotheses have been proposed in support of blood type personality theory.

Dependent type

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, and Idris, dependent types may help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.[citation needed]

Two common examples of dependent types are dependent functions and dependent pairs. The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer may return an array of length , where the array length is part of the type of the array. (Note that this is different from polymorphism and generic programming, both of which include the type as an argument.) A dependent pair may have a second value of which the type depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way.

Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.

Duck typing

Duck typing in computer programming is an application of the duck test—"If it walks like a duck and it quacks like a duck, then it must be a duck"—to determine if an object can be used for a particular purpose. With normal typing, suitability is determined by an object's type. In duck typing, an object's suitability is determined by the presence of certain methods and properties, rather than the type of the object itself.

Higher-order logic

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more expressive, but their model-theoretic properties are less well-behaved than those of first-order logic.

The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher-order simple predicate logic. Here "simple" indicates that the underlying type theory is simple, not polymorphic or dependent.

Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

This includes, among other lines of work, the construction of homotopical and higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants.

There is a large overlap between the work referred to as homotopy type theory, and as the univalent foundations project. Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux.

Inductive type

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

The standard example is encoding the natural numbers using Peano's encoding.

Here, a natural number is created either from the constant "0" or by applying the function "S" to another natural number. "S" is the successor function which represents adding 1 to a number. Thus, "0" is zero, "S 0" is one, "S (S 0)" is two, "S (S (S 0))" is three, and so on.

Since their introduction, inductive types have been extended to encode more and more structures, while still being predicative and supporting structural recursion.

Intuitionistic type theory

Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.

Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

Kind (type theory)

In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted and called "type", which is the kind of any data type which does not need any type parameters.

A kind is sometimes confusingly described as the "type of a (data) type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic types to be type constructors, thus non-polymorphic types to be nullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely .

Since higher-order type operators are uncommon in programming languages, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implement parametric polymorphism. Kinds appear, either explicitly or implicitly, in languages whose type systems account for parametric polymorphism in a programatically accessible way, such as Haskell and Scala.

Mathematical structure

In mathematics, a structure on a set is an additional mathematical object that, in some manner, attaches (or relates) to that set to endow it with some additional meaning or significance.

A partial list of possible structures are measures, algebraic structures (groups, fields, etc.), topologies, metric structures (geometries), orders, events, equivalence relations, differential structures, and categories.

Sometimes, a set is endowed with more than one structure simultaneously; this enables mathematicians to study it more richly. For example, an ordering imposes a rigid form, shape, or topology on the set. As another example, if a set has both a topology and is a group, and these two structures are related in a certain way, the set becomes a topological group.

Mappings between sets which preserve structures (so that structures in the source or domain are mapped to equivalent structures in the destination or codomain) are of special interest in many fields of mathematics. Examples are homomorphisms, which preserve algebraic structures; homeomorphisms, which preserve topological structures; and diffeomorphisms, which preserve differential structures.

Myers–Briggs Type Indicator

The Myers–Briggs Type Indicator (MBTI) is an introspective self-report questionnaire with the purpose of indicating differing psychological preferences in how people perceive the world around them and make decisions.The MBTI was constructed by Katharine Cook Briggs and her daughter Isabel Briggs Myers. It is based on the conceptual theory proposed by Carl Jung, who had speculated that humans experience the world using four principal psychological functions – sensation, intuition, feeling, and thinking – and that one of these four functions is dominant for a person most of the time.The MBTI was constructed for normal populations and emphasizes the value of naturally occurring differences. "The underlying assumption of the MBTI is that we all have specific preferences in the way we construe our experiences, and these preferences underlie our interests, needs, values, and motivation."Although popular in the business sector, the MBTI exhibits significant scientific (psychometric) deficiencies, notably including poor validity (i.e. not measuring what it purports to measure, not having predictive power or not having items that can be generalized), poor reliability (giving different results for the same person on different occasions), measuring categories that are not independent (some dichotomous traits have been noted to correlate with each other), and not being comprehensive (due to missing neuroticism). The four scales used in the MBTI have some correlation with four of the Big Five personality traits, which are a more commonly accepted framework.

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type. Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming.

For example, a function append that joins two lists can be constructed so that it does not care about the type of elements: it can append lists of integers, lists of real numbers, lists of strings, and so on. Let the type variable a denote the type of elements in the lists. Then append can be typed

forall a. [a] × [a] -> [a]where [a] denotes the type of lists with elements of type a. We say that the type of append is parameterized by a for all values of a. (Note that since there is only one type variable, the function cannot be applied to just any pair of lists: the pair, as well as the result list, must consist of the same type of elements.) For each place where append is applied, a value is decided for a.

Following Christopher Strachey, parametric polymorphism may be contrasted with ad hoc polymorphism, in which a single polymorphic function can have a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied. Thus, ad hoc polymorphism can generally only support a limited number of such distinct types, since a separate implementation has to be provided for each type.

Polymorphism (computer science)

In programming languages and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types.The most commonly recognised major classes of polymorphism are:

Ad hoc polymorphism: defines a common interface for an arbitrary set of individually specified types.

Parametric polymorphism: when one or more types are not specified by name but by abstract symbols that can represent any type.

Subtyping (also called subtype polymorphism or inclusion polymorphism): when a name denotes instances of many different classes related by some common superclass.

Principia Mathematica

The Principia Mathematica (often abbreviated PM) is a three-volume work on the foundations of mathematics written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. In 1925–27, it appeared in a second edition with an important Introduction to the Second Edition, an Appendix A that replaced ✸9 and all-new Appendix B and Appendix C. PM is not to be confused with Russell's 1903 The Principles of Mathematics. PM was originally conceived as a sequel volume to Russell's 1903 Principles, but as PM states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of Principles of Mathematics... But as we advanced, it became increasingly evident that the subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions."

PM, according to its introduction, had three aims: (1) to analyze to the greatest possible extent the ideas and methods of mathematical logic and to minimize the number of primitive notions and axioms, and inference rules; (2) to precisely express mathematical propositions in symbolic logic using the most convenient notation that precise expression allows; (3) to solve the paradoxes that plagued logic and set theory at the turn of the 20th-century, like Russell's paradox.This third aim motivated the adoption of the theory of types in PM. The theory of types adopts grammatical restrictions on formulas that rules out the unrestricted comprehension of classes, properties, and functions. The effect of this is that formulas such as would allow the comprehension of objects like the Russell set turn out to be ill-formed: they violate the grammatical restrictions of the system of PM.

There is no doubt that PM is of great importance in the history of mathematics and philosophy: as Irvine has noted, it sparked interest in symbolic logic and advanced the subject by popularizing it; it showcased the powers and capacities of symbolic logic; and it showed how advances in philosophy of mathematics and symbolic logic could go hand-in-hand with tremendous fruitfulness. Indeed, PM was in part brought about by an interest in Logicism, the view on which all mathematical truths are logical truths. It was in part thanks to the advances made in PM that, despite its defects, numerous advances in meta-logic were made, including Gödel's incompleteness theorems.

For all that, PM is not widely used today: probably the foremost reason for this is its reputation for typographical complexity. Somewhat infamously, several hundred pages of

PM precede the proof of the validity of the proposition 1+1=2. Contemporary mathematicians tend to use a modernized form of the system of Zermelo–Fraenkel set theory. Nonetheless, the scholarly, historical, and philosophical interest in PM is great and ongoing: for example, the Modern Library placed it 23rd in a list of the top 100 English-language nonfiction books of the twentieth century.

Programming language theory

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It is a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.


In mathematics, a tuple is a finite ordered list (sequence) of elements. An n-tuple is a sequence (or ordered list) of n elements, where n is a non-negative integer. There is only one 0-tuple, an empty sequence, or empty tuple, as it is referred to. An n-tuple is defined inductively using the construction of an ordered pair.

Mathematicians usually write 'tuples' by listing the elements within parentheses "" and separated by commas; for example, denotes a 5-tuple. Sometimes other symbols are used to surround the elements, such as square brackets "[ ]" or angle brackets "⟨ ⟩". Braces "{ }" are only used in defining arrays in some programming languages such as C++ and Java, but not in mathematical expressions, as they are the standard notation for sets. The term tuple can often occur when discussing other mathematical objects, such as vectors.

In computer science, tuples come in many forms. In dynamically typed languages, such as Lisp, lists are commonly used as tuples.[citation needed] Most typed functional programming languages implement tuples directly as product types, tightly associated with algebraic data types, pattern matching, and destructuring assignment. Many programming languages offer an alternative to tuples, known as record types, featuring unordered elements accessed by label. A few programming languages combine ordered tuple product types and unordered record types into a single construct, as in C structs and Haskell records. Relational databases may formally identify their rows (records) as tuples.

Tuples also occur in relational algebra; when programming the semantic web with the Resource Description Framework (RDF); in linguistics; and in philosophy.

Type constructor

In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. New types can be defined by recursively composing type constructors.

For example, simply typed lambda calculus can be seen as a language with a single type constructor—the function type constructor. Product types can generally be considered "built-in" in typed lambda calculi via currying.

Abstractly, a type constructor is an n-ary type operator taking as argument zero or more types, and returning another type. Making use of currying, n-ary type operators can be (re)written as a sequence of applications of unary type operators. Therefore, we can view the type operators as a simply typed lambda calculus, which has only one basic type, usually denoted , and pronounced "type", which is the type of all types in the underlying language, which are now called proper types in order to distinguish them from the types of the type operators in their own calculus, which are called kinds.

Instituting a simply typed lambda calculus over the type operators results in more than just a formalization of type constructors though. Higher-order type operators become possible. Type operators correspond to the 2nd axis in the lambda cube, leading to the simply typed lambda-calculus with type operators, λω; while this is not so well known, combining type operators with polymorphic lambda calculus (system F) yields system F-omega.

Type physicalism

Type physicalism (also known as reductive materialism, type identity theory, mind–brain identity theory and identity theory of mind) is a physicalist theory, in the philosophy of mind. It asserts that mental events can be grouped into types, and can then be correlated with types of physical events in the brain. For example, one type of mental event, such as "mental pains" will, presumably, turn out to be describing one type of physical event (like C-fiber firings).

Type physicalism is contrasted by token identity physicalism, which argues that mental events are unlikely to have "steady" or categorical biological correlates. These positions make use of the philosophical type–token distinction (e.g., Two persons having the same "type" of car need not mean that they share a "token", a single vehicle). Type physicalism can now be understood to argue that there is identicalness between types, whereas token identity physicalism says one can only describe a particular, unique, brain event.

There are other ways a physicalist might criticize type physicalism; eliminative materialism and revisionary materialism question whether science is currently using the best categorisations. In the same way talk of demonic possession was questioned with scientific advance, categorisations like "pain" may need to be revised.

Void type

The Void type, in several programming languages derived from C and Algol68, is the type for the result of a function that returns normally, but does not provide a result value to its caller. Usually such functions are called for their side effects, such as performing some task or writing to their output parameters. The usage of the void type in such context is comparable to procedures in Pascal and syntactic constructs which define subroutines in Visual Basic. It is also similar to the unit type used in functional programming languages and type theory. See Unit type#In programming languages for a comparison.

C and C++ also support the pointer to void type (specified as void *), but this is an unrelated notion. Variables of this type are pointers to data of an unspecified type, so in this context (but not the others) void * acts roughly like a universal or top type. A program can probably convert a pointer to any type of data (except a function pointer) to a pointer to void and back to the original type without losing information, which makes these pointers useful for polymorphic functions. The C language standard does not guarantee that the different pointer types have the same size.

Computer systems
Software organization
Software notations
and tools
Software development
Theory of computation
of computing
Machine learning
Traditional logic
Predicate logic
Naive set theory
Set theory
Model theory
Proof theory

This page is based on a Wikipedia article written by authors (here).
Text is available under the CC BY-SA 3.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.