Editing Type theory (section)

===Linguistics===
Type theory is also widely used in [[formal semantics (linguistics)|formal theories of semantics]] of [[natural language]]s,<ref>{{Cite book|last1=Chatzikyriakidis|first1=Stergios|url=https://books.google.com/books?id=iEEUDgAAQBAJ|title=Modern Perspectives in Type-Theoretical Semantics|last2=Luo|first2=Zhaohui|date=2017-02-07|publisher=Springer|isbn=978-3-319-50422-3|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074711/https://books.google.com/books?id=iEEUDgAAQBAJ|url-status=live}}</ref><ref>{{Cite book|last=Winter|first=Yoad|url=https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|title=Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language|date=2016-04-08|publisher=Edinburgh University Press|isbn=978-0-7486-7777-1|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074717/https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|url-status=live}}</ref> especially [[Montague grammar]]<ref>Cooper, Robin. "[http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf Type theory and semantics in flux] {{Webarchive|url=https://web.archive.org/web/20220510190635/http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf|date=2022-05-10}}." Handbook of the Philosophy of Science 14 (2012): 271-323.</ref> and its descendants. In particular, [[categorial grammar]]s and [[pregroup grammar]]s extensively use type constructors to define the types (''noun'', ''verb'', etc.) of words.

The most common construction takes the basic types <math>e</math> and <math>t</math> for individuals and [[truth-value]]s, respectively, and defines the set of types recursively as follows:
* if <math>a</math> and <math>b</math> are types, then so is <math>\langle a,b\rangle</math>;
* nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type <math>\langle a,b\rangle</math> is the type of [[Function (mathematics)|functions]] from entities of type <math>a</math> to entities of type <math>b</math>. Thus one has types like <math>\langle e,t\rangle</math> which are interpreted as elements of the set of functions from entities to truth-values, i.e. [[indicator function]]s of sets of entities. An expression of type <math>\langle\langle e,t\rangle,t\rangle</math> 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 [[Generalized quantifier|natural language quantifiers]], like '' everybody'' or ''nobody'' ([[Richard Montague|Montague]] 1973, [[Jon Barwise|Barwise]] and Cooper 1981).<ref>Barwise, Jon; Cooper, Robin (1981) [https://philpapers.org/rec/BARGQA Generalized quantifiers and natural language] ''Linguistics and Philosophy'' '''4''' (2):159--219 (1981)</ref>

[[Type theory with records]] is a [[formal semantics (linguistics)|formal semantics]] representation framework, using ''[[Record_(computer_science)|records]]'' to express ''type theory types''. It has been used in [[natural language processing]], principally [[computational semantics]] and [[dialogue systems]].<ref>{{cite journal|last = Cooper| first = Robin| year = 2005| title = Records and Record Types in Semantic Theory| journal = Journal of Logic and Computation| volume = 15| issue = 2| pages = 99–112| doi = 10.1093/logcom/exi004}}</ref><ref>Cooper, Robin (2010). ''Type theory and semantics in flux''. ''Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics''. Elsevier.</ref>