Editing Type theory (section)

==History==
{{Main|History of type theory}}
Type theory was created to avoid [[paradox]]es in [[naive set theory]] and [[formal logic]]{{efn|name= kleeneRosser |1= The [[Kleene–Rosser paradox]] "The Inconsistency of Certain Formal Logics" on page 636 ''Annals of Mathematics'' '''36''' number 3  (July 1935), showed that <math> 1=2 </math>.<ref name= KleeneRosser> {{Cite journal |first1=S. C. |last1=Kleene |name-list-style=amp |first2=J. B. |last2=Rosser |title=The inconsistency of certain formal logics |journal=[[Annals of Mathematics]] |volume=36 |issue=3 |pages=630–636 |year=1935 |doi=10.2307/1968646 |jstor=1968646 }}</ref>}}, such as [[Russell's paradox]] which demonstrates that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, [[Bertrand Russell]] proposed various solutions to this problem.

By 1908, Russell arrived at a [[History_of_type_theory#The_1908_"ramified"_theory_of_types|ramified theory of types]] together with an [[axiom of reducibility]], both of which appeared in [[Alfred North Whitehead|Whitehead]] and [[Bertrand Russell|Russell]]'s ''[[Principia Mathematica]]'' published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of [[subtyping|subtype]]s of that type,{{efn|name=JuliaSample|1= In [[Julia (programming language)|Julia]]'s type system, for example, abstract types have no instances, but can have subtype,<ref name=juliaSample >Balbaert, Ivo (2015) ''Getting Started With Julia Programming'' ISBN 978-1-78328-479-5</ref>{{rp|110}} whereas concrete types do not have subtypes but can have instances, for "[[Julia (programming language)#Language features|documentation, optimization, and dispatch]]".<ref name=juliaTypes >docs.julialang.org [https://docs.julialang.org/en/v1/manual/types/ v.1 Types] {{Webarchive|url=https://web.archive.org/web/20220324054245/https://docs.julialang.org/en/v1/manual/types/|date=2022-03-24}}</ref>}} thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as [[Zermelo–Fraenkel set theory|Zermelo-Fraenkel set theory]].<ref name="sepErp">''Stanford Encyclopedia of Philosophy'' [https://plato.stanford.edu/entries/russell-paradox/#ERP (rev. Mon Oct 12, 2020) Russell’s Paradox] {{Webarchive|url=https://web.archive.org/web/20211218023900/https://plato.stanford.edu/entries/russell-paradox/#ERP|date=December 18, 2021}} 3. Early Responses to the Paradox</ref>

Type theory is particularly popular in conjunction with [[Alonzo Church]]'s [[lambda calculus]]. One notable early example of type theory is Church's [[simply typed lambda calculus]]. Church's theory of types<ref name="church">{{cite journal|author-link=Alonzo Church|first=Alonzo|last=Church|title=A formulation of the simple theory of types|journal=The Journal of Symbolic Logic|volume=5|issue=2|pages=56–68|year=1940|doi=10.2307/2266170|jstor=2266170|s2cid=15889861}}</ref> helped the formal system avoid the [[Kleene–Rosser paradox]] that afflicted the original untyped lambda calculus. Church demonstrated{{efn|name=logisticMethod|1= Church demonstrated his ''logistic method'' with his simple theory of types,<ref name=church/> and explained his method in 1956,<ref name=intro>Alonzo Church (1956) [https://archive.org/details/dli.ernet.449121/page/85/mode/2up?q=logistic Introduction To Mathematical Logic Vol 1]</ref> pages 47-68.}} that it could serve as a [[Foundations of mathematics|foundation of mathematics]] and it was referred to as a [[higher-order logic]].

In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is [[Per Martin-Löf]]'s [[intuitionistic type theory]], which was proposed as a foundation for [[Constructivism (mathematics)|constructive mathematics]]. Another is [[Thierry Coquand]]'s [[calculus of constructions]], which is used as the foundation by [[Rocq (software)|Rocq]] (previously known as ''Coq''), [[Lean (proof assistant)|Lean]], and other computer [[Proof assistant|proof assistants]]. Type theory is an active area of research, one direction being the development of [[homotopy type theory]].