Lecture
In mathematics, logic, and computer science, type theory refers to any formal system that serves as an alternative to naive set theory, accompanied by a classification of the elements of such a system by means of types forming a certain hierarchy. The term type theory is also used to refer to the study of such formalisms.
Type theory — a mathematically formalized foundation for designing, analyzing, and studying data type systems in the theory of programming languages (a branch of computer science). Many programmers use this term to refer to any analytical work that studies type systems in programming languages. In academic circles, type theory most often refers to a narrower branch of discrete mathematics, in particular the typed λ-calculus.
Modern type theory was developed in part while resolving Russell's paradox, and it is largely based on the work of Bertrand Russell and Alfred Whitehead, «Principia Mathematica» .
Figure 1 Homotopy trinitarianism as a connection between logical concepts, homotopical concepts and algebraic structures
1901 — Russell's paradox
1908 — the first theory of types (Russell, Whitehead)
1900-1930 Set theory and vicious circles. The problem of impredicativity.
1925 — Ramsey's simple theory of types, systems of “simple types” (simply typed lambda calculus)
1930-1950 The Curry-Howard correspondence
1940 — the simply typed λ-calculus
1950-1970 Dependent types. De Bruijn's Automath.
1973 — constructive type theory (Martin-Löf)
The doctrine of types goes back to B. Russell, according to whom every type is regarded as the range of significance of a propositional function. It is also held that every function has a type (its domain, its region of definition). The doctrine of types observes the principle of substituting a type (proposition) with a definitionally equivalent type (proposition).
This theory is based on the principle of hierarchy. This means that logical concepts — propositions, individuals, propositional functions — are arranged into a hierarchy of types. It is essential that an arbitrary function takes as its arguments only those concepts that precede it in the hierarchy.
By a certain type theory one usually means a higher-order applied logic in which there is a type N of natural numbers, and in which the axioms of Peano arithmetic hold
Historically the first type theory to be proposed (during the period from 1902 to 1913) is the Ramified Theory of Types (RTT), constructed by Whitehead and Russell, and finally formulated in the foundational work «Principia Mathematica». This theory is based on the principle of limiting the number of cases in which objects belong to a single type. Eight such cases are explicitly declared, and two hierarchies of types are distinguished: (simple) «types» and «orders». At the same time, the notation for «type» itself is not defined, and there are a number of other imprecisions, since the main intention was to declare unequal the types of functions of different numbers of arguments or of arguments of different types . An integral part of the theory is the axiom of reducibility.
In the 1920s, Chwistek and Ramsey proposed an unramified theory of types, now known as the «Theory of Simple Types» or Simple Type Theory (Simple Type Theory), which collapses the hierarchy of types, eliminating the need for the axiom of reducibility.
Simple type theory resolved the set-theoretic paradoxes, but the second group of semantic paradoxes, the Grelling-Nelson paradoxes
and so on, remained unresolved, and it was for these that Russell and Whitehead developed the ramified theory of types within the Principia Mathematica system.
Intuitionistic type theory (Intuitionistic Type Theory, ITT) was constructed by Per Martin-Löf.
Intuitionistic type theory (also known as constructive type theory or Martin-Löf type theory) is a type theory and an alternative foundation for mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are several versions of the theory of types: Martin-Löf proposed both intensional and extensional variants of the theory, and the early impredicative versions, whose inconsistency was proved by Girard's paradox, gave way to a predicative version. However, all versions preserve the basic construction of constructive logic using dependent types.
Martin-Löf developed the theory of types on the principles of mathematical constructivism. Constructivism requires that any existence proof contain a «witness». Thus, any proof that «there exists a prime number greater than 1000» must identify a specific number that is both prime and greater than 1000. Intuitionistic type theory achieved this design goal by adopting the BHK interpretation. An interesting consequence is that proofs become mathematical objects that can be examined, compared, and manipulated.
The type constructors in intuitionistic type theory were built so as to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication ( 
) corresponds to the function type ( 
). This correspondence is called the Curry–Howard isomorphism. Earlier theories of types also followed this isomorphism, but Martin-Löf was the first to extend it to predicate logic by introducing dependent types.
Intuitionistic logic. There is no law of the excluded middle. Any proof must be presented in general form
In intuitionistic type theory there are 3 finite types, which are then composed using 5 different type constructors. Unlike set theories, type theories are not built on a Frege-like logic. So, every feature of type theory performs a dual function, as a property of both mathematics and logic.
If you are not familiar with type theory but are familiar with set theory, here is a brief summary: Types contain terms in the same way that sets contain elements. Terms belong to one and only one type. Terms such as 
as well as 
compute ("reduce") to canonical terms, for example 4. See the article on type theory for more details.
There are 3 finite types: Type 0 contains 0 terms. Type 1 contains 1 canonical term. And type 2 contains 2 canonical terms.
Since type 0 contains 0 terms, it is also called the empty type. It is used to denote anything that cannot exist. It is also written as 
and represents something unprovable. (That is, a proof of it cannot exist.) As a result, negation is defined as a function with respect to it: 
.
Similarly, type 1 contains 1 canonical term and represents existence. It is also called the unit type. It often represents statements that can be proven, and so it is sometimes written as 
.
Finally, type 2 contains 2 canonical terms. It represents a definite choice between two values. It is used for boolean values, but not for propositions. Propositions are considered to be of type 1, and it can be proven that they will never have a proof (type 0), or they may fail to be proven in any case. (The law of excluded middle does not apply to propositions in intuitionistic type theory.)
The theory of pure type systems (PTS) generalizes all the calculi of the lambda cube and formulates rules that allow them to be computed as special cases. It was independently constructed by Berardi and Terlouw. Pure type systems operate only with the concept of type, treating all the concepts of other calculi solely as types — which is why they are called «pure». No distinction is made between terms and types, between different layers (i.e. the kinds of types are also called types, only belonging to a different universe), and even the layers themselves are not called sorts but types (more precisely, universes of types). In general form, a pure type system is given by the notion of a specification, five rigid rules, and two flexible ones (which vary from system to system). The specification of a pure type system is a triple (S,A,R), where S — the set of sorts (Sorts), A — the set of axioms (Axioms) over these sorts, and R — the set of rules (Rules).
Higher-dimensional type theories or simply higher type theories (HTT) generalize traditional type theories by allowing nontrivial equality relations to be established between types. For example, if we take the set of pairs (Cartesian products) of natural numbers nat × nat and the set of functions returning a natural number nat -> nat, we cannot claim that the elements of these sets are pairwise equal, but we can claim that these sets are equivalent. Isomorphisms between types are studied in two-dimensional, three-dimensional, and so on type theories. The whole necessary basis for formulating these theories was laid by Girard — Reynolds, but the theories themselves were formulated much later.
Homotopy type theory (HoTT) generalizes multidimensional theories by establishing type equalities at the level of topologies. In multidimensional theories, the notions of «type equivalence» and «type equality» are considered distinct. A radical innovation of homotopy type theory is the univalence axiom, which postulates that if types are topologically equivalent, then they are topologically equal.
Lambda calculus (λ-calculus) — a formal system developed by American mathematician Alonzo Church to formalize and analyze the notion of computability.
Pure λ-calculus, whose terms, also called objects («obs»), or λ-terms, are built exclusively from variables by applying application and abstraction. Initially, no constants are assumed to exist.
Lambda calculus – the simplest and most elegant algorithmically complete programming language.
Simply typed lambda calculus. Algorithmically incomplete. Any term (including one with free variables) has a normal (canonical, “computed”) form.
| t ::= | terms: |
| x | variable |
| λx. t | abstraction |
| t t | application |
Examples
(λx.x) z
(λx.x) ((λx.x) (λz. (λx.x) z))
Computation (β-reduction)
(λx.x) ((λx.x) (λz. (λx.x) z))
id (id (λz. id z))
→ id (id (λz.z))
→ id (λz.z)
→ λz.z
Encoding in terms of λ-calculus
The primary form of equivalence defined on lambda terms is alpha-equivalence. For example, 
and 
: are alpha-equivalent lambda terms, and both represent the same function (the identity function). The terms 
and 
are not alpha-equivalent, since they are not within a lambda abstraction.
β-reduction
Since the expression 
denotes a function that maps each to the value 
, to compute the expression
,
which contains both application and abstraction, it is necessary to substitute the number 3 into the term in place of the variable . This yields 
. In general form, this reasoning is written as
and is called β-reduction. An expression of the form 
, that is, the application of an abstraction to some term, is called a redex. Although β-reduction is essentially the only «essential» axiom of λ-calculus, it leads to a very rich and complex theory. Together with it, λ-calculus is Turing complete and, therefore, constitutes the simplest programming language.
-conversion expresses the idea that two functions are identical if and only if, when applied to any argument, they give the same results. -conversion converts the formulas 
and 
into one another (only if has no free occurrences in {\displaystyle f}: otherwise, the free variable would become bound by the outer abstraction after conversion, or vice versa).
Syntax of the ζ-calculus
| b ::= | terms: |
| x | variable |
| [li = ζ(xi)bi] | objects |
| b.l | method invocation |
| b1.l⇐ ζ(x)b2 | method update |
| clone(b) | cloning |
| let x=b1 in b2 | local declaration |
-calculus in theoretical computer science — a process calculus, originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the calculus of communicating systems. The goal of the -calculus is to be able to describe concurrent computations, whose configuration can change over the course of the computation.
-calculus belongs to the family of process calculi. In fact, the {\displaystyle \pi }-calculus, like λ-calculus, is so minimal that it contains no primitives such as numbers, boolean expressions, data structures, variables, functions or control flow operators (for example, if-then-else, while).
Syntax of the π-calculus
| P, Q, R ::= | terms: |
| 0 | idle process |
| x(y).P | receiving y from channel x and executing P |
| xy.P | sending y on channel x and executing P |
| P|Q | parallel execution |
| (νx)P | channel creation |
| !P | replication |
Operational semantics describes a sequential process of state changes — an abstract machine.
Polymorphism — is the use of a single piece of program code with different types in different contexts.
Kinds of polymorphism
There are many different set theories and many different type theory systems, so everything that follows is a generalization.
Although the original motivation for category theory was far from foundationalism, it turned out that the two fields have a deep connection. As John Lane Bell writes: «In fact, categories themselves can be regarded as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than to set theory». In short, a category can be viewed as a type theory by treating its objects as types (or sorts), i.e. «roughly speaking, a category can be regarded as a type theory stripped of its syntax». Thus, a number of important results follow:
This interaction, known as categorical logic, has since become the subject of active research; see, for example, the monograph by Jacobs (1999).
Comments