Перегляд вихідного коду сторінки Теорія типів

'''Теорія типів'''&nbsp;— це будь-яка [[формальна система]], що може слугувати альтернативою [[Наївна теорія множин|наївній теорії множин]]. У теорії типів кожен «терм» має «тип», а операції виконуються в узгодженості з цими типами.

Теорія типів тісно пов'язана з [[Система типізації|системами типів]]&nbsp;— особливістю [[Мова програмування|мов програмування]], яка призначена для зменшення кількості [[Баг|помилок]]. Теорія типів була розроблена для обходження парадоксів [[Формальна логіка|формальної логіки]].

Однією з найвідоміших теорій типів є [[типізоване лямбда-числення]] [[Алонзо Черч]]а та [[інтуїціоністська теорія типів]] {{Нп|Пер Мартін-Льоф|Пера Мартіна-Льофа||Per Martin-Löf}}.

== Історія ==
В проміжок між 1902 та 1908 роками [[Бертран Расселл]] запропонував різні теорії типів у відповідь до його відкриття, яке встановлювало присутність [[Парадокс Расселла|парадоксу Расселла]] у наївній теорії множин [[Готлоб Фреге|Готлоба Фреге]]. У 1908 році [[Бертран Расселл|Расселл]] винайшов «розгалужену» теорію типів та «аксіому редукції», які були опубліковані у праці [[Альфред Норт Вайтгед|Вайтгеда]] та [[Бертран Расселл|Расселла]] [[Principia Mathematica|«Principia Mathematica»]]. Вони намагалися вирішити парадокс Расселла за допомогою розробки ієрархії типів та призначенні кожної математичної сутності до типу. Сутності кожного типу будувалися сутностями типів, які розташовані нижче за ієрархією, що запобігало призначенню сутності до самої себе. У 1920-х роках [[Леон Хвістек]] та [[Френк Ремзі|Френк Пламптон Ремзі]] запропонували нерозгалужену теорію типів, яка зараз відома як «теорія простих типів» або «проста теорія типів». Ця теорія не використовувала ієрархії типів та, як наслідок, не вимагала аксіоми редукції.

Найвідомішим прикладом використання типів є {{Нп|просто типізоване лямбда-числення|||Simply typed lambda calculus}} [[Алонзо Черч]]а. Теорія типів Черча<ref name="church">[[Алонзо Черч|Alonzo Church]], [https://www.jstor.org/stable/2266170 ''A formulation of the simple theory of types''] {{Webarchive|url=https://web.archive.org/web/20181115071243/https://www.jstor.org/stable/2266170 |date=15 листопада 2018 }}, The Journal of Symbolic Logic 5(2):56&ndash;68 (1940)</ref> допомогла формальним системам уникнути {{Нп|Парадокс Кліні — Россера|парадоксу Кліні — Россера||Kleene–Rosser paradox}}, присутнього у оригінальному безтиповому лямбда-численні. Черч продемонстрував, що ця теорія може служити основою для математики.

== Базові поняття ==
У системі теорії типів кожен '''[[Терм (логіка)|терм]]''' має '''тип'''. Наприклад, <math>4</math>, <math>2+2</math> та <math>2\cdot 2</math> є окремими термами типу <math>\mathrm{nat}</math>, тобто натуральними числами. Традиційно терм супроводжується двокрапкою і його типом, наприклад, <math>2 : \mathrm{nat}</math>.

Теорії типів мають явне обчислення, яке кодується правилами [[Рерайтинг (математика)|рерайтингу]] термів. Вони називаються '''правилами перетворення''' або, якщо правило працює лише в одному напрямку, '''правилом редукції'''. Наприклад, <math>2 + 2</math> та <math>4</math> є синтаксично різними термами, але перший терм редукується до другого. На запису ця редукція має вигляд <math>2 + 2 \twoheadrightarrow 4</math>.

Функції в теорії типів мають спеціальне правило редукції: аргумент виклику функції замінюється на кожне входження параметра у визначенні функції. Нехай функція <math>\mathrm{double}</math> визначена як <math>\lambda x . x+x </math> (використовуючи лямбда нотацію Черча) або <math>x \mapsto x+x </math> (використовуючи більш сучасну нотацію). Тоді виклик функції <math>\mathrm{double}\ 2</math> редукується шляхом заміни кожної копії <math>x</math> термом <math>2</math> в тілі визначення функції. Таким чином, <math>\mathrm{double}\ 2 \twoheadrightarrow 2+2</math>.

Тип функції позначається стрілкою <math>\to</math> від типу параметра до результуючого типу функції. Таким чином, <math>\mathrm{double} : \mathrm{nat} \to \mathrm{nat}</math>. Виклик функції з деяким аргументом може бути написаний з дужками або без них, наприклад, <math>\mathrm{double}(2)</math> або <math>\mathrm{double}\ 2</math>. Зазвичай дужки не використовуються, тому що функції багатьох аргументів можуть бути визначеними за допомогою [[Каррінг (інформатика)|каррінгу]].

== Відмінності від теорії множин ==

Існує безліч різних теорій множин та різних систем теорії типів.

* Теорія множин побудована поверх логіки. Вона вимагає окремої системи, подібної [[Логіка першого порядку|логіці першого порядку]]. У теорії типів поняття типу «і» та «або» можуть бути закодовані як типи самої теорії типів.
* У теорії множин елемент може належати до безлічі різних множин, до підмножини, або до множини множин. У теорії типів терми, як правило, належать тільки до одного типу. (Там, де використовуються підмножини, теорія типів прагне використовувати [[Предикат|функцію предикатів]], яка повертає <math>true</math>, якщо терм знаходиться в підмножині, та повертає <math>false</math> в іншому випадку. Об'єднання двох типів можна зробити, створивши новий тип, який називається типом-сумою та містить нові терми.)
* Теорія множин зазвичай кодує числа як множини. (<math>0</math>&nbsp;— порожня множина, <math>1</math>&nbsp;— множина, що містить порожню множину, і&nbsp;т.&nbsp;д.) Теорія типів може кодувати числа як функції, використовуючи {{Нп|Кодування Черча|кодування Черча||Church encoding}}, або як {{Нп|Індуктивний тип|індуктивні типи||Inductive type}}. Індуктивні типи створюють нові константи для {{Нп|Функція наступник|функції наступника||Successor function}} і нуль, що дуже нагадує [[Аксіоми Пеано|аксіоми Пеано]].
* Теорія множин використовує [[Нотація побудови множини|нотацію побудови множини]].
* Теорія типів має просте з'єднання з конструктивною математикою через {{Нп|Інтерпретація Брауера — Гейтінга — Колмогорова|інтерпретацію Брауера — Гейтінга — Колмогорова||Brouwer–Heyting–Kolmogorov interpretation}} та може бути пов'язана з логікою [[Відповідність Каррі — Говарда|ізоморфізмів Каррі&nbsp;— Говарда]]. Деякі теорії типів тісно пов'язані з [[Теорія категорій|теорією категорій]].

== Додаткові визначення ==

=== Нормалізація ===
Терм <math>2 + 1</math> редукується до <math>3</math>. Так як <math>3</math> надалі не редукується, кажуть, що цей терм знаходиться у '''нормальній формі'''. Кажуть, що система теорії типів '''сильно нормалізується''', якщо всі терми мають нормальну форму та будь-який порядок редукції досягає її. '''Слабо нормалізуючи''' системи мають нормальну форму, але деякі порядки редукції можуть назавжди зациклитися та ніколи її не досягнути.

Інколи визначення '''елементу''' запозичують з теорії множин та використовують його для позначення всіх закритих термів, які редукуються до однієї нормальної форми. '''Закритим термом''' називається терм, який не має параметрів. Терм виду <math>x + 1</math> має параметр <math>x</math> та називається '''відкритим термом'''. Таким чином, <math>2 + 1</math> та <math>3 + 0</math> є різними термами, але вони обидва редукуються до елементу <math>3</math>.

Схожим поняттям, яке визначається для закритих та відкритих термів, є поняття конвертованості. Два терми називаються '''конвертованими''', якщо існує терм, до якого ці два терми редукуються. Наприклад, <math>2 + 1</math> та <math>1 + 2</math> є конвертованими. Терми <math>x + (1 + 1)</math> та <math>x + 2</math> також є конвертованими. Однак терми <math>x + 1</math> та <math>1 + x</math> (де <math>x</math> є вільною змінною) не є конвертованими, так як вони знаходяться у нормальній формі та не є однаковими. Слабо нормалізуючі системи можуть перевірити, чи є два терми конвертованими, шляхом редукції цих термів до однієї нормальної форми.

=== Залежні типи ===
{{Докладніше|Залежний тип}}
'''[[Залежний тип|Залежним типом]]''' називається тип, який залежить від термів та інших типів. Таким чином, тип, повернутий функцією, може залежати від аргументу функції.

Наприклад, список термів типу <math>\mathrm{nat}</math> із 4 елементів може відрізнятися від списку термів типу <math>\mathrm{nat}</math> із 5 елементів. У теорії типів з залежними типами можна визначити функцію, яка приймає параметр <math>n</math> і повертає список, що містить <math>n</math> нулів. Тип терму, породженого викликом функції з <math>4</math>, відрізнявся би від типу терму, породженого викликом функції з <math>5</math>.

Залежні типи відіграють центральну роль в [[Інтуїціоністська теорія типів|теорії типів Мартіна-Льофа]] та в розробці [[Функційне програмування|функційних мов програмування]], таких як {{Нп|Idris (мова програмування)|Idris||Idris (programming language)}}, {{Нп|ATS (мова програмування)|ATS||ATS (programming language)}}, [[Agda]] та {{Нп|Epigram (мова програмування)|Epigram ||Epigram (programming language)}}.

=== Типи рівності ===

Багато систем теорії типів мають тип, який представляє рівність типів та термів. Цей тип відрізняється від конвертованості та часто визначається як '''пропозиційна рівність'''.

У теорії типів Мартіна-Льофа тип рівності (який також називається типом ідентичності) позначається як <math>I</math> (від [[Англійська мова|англ.]] ''Identity''). Кажуть, що існує тип <math>I\ A\ a\ b</math>, коли <math>A</math> є типом, а <math>a</math> і <math>b</math>&nbsp;— це терми типу <math>A</math>. Терм типу <math>I\ A\ a\ b</math> інтерпретується як визначення рівності <math>a</math> та <math>b</math>.

На практиці можна побудувати тип <math>I\ \mathrm{nat}\ 3\ 4</math>, але такий тип не буде мати термів. У теорії типів Мартіна-Льофа нові терми рівності мають властивість рефлексивності. Якщо <math>3</math> є термом типу <math>\mathrm{nat}</math>, то існує терм типу <math>I\ \mathrm{nat}\ 3\ 3</math>. Більш складні рівності можуть бути створені шляхом створення рефлексивного терму та його подальшої редукції. Тобто якщо <math>2+1</math> є термом типу <math>\mathrm{nat}</math>, то існує терм типу <math>I\ \mathrm{nat}\ (2+1)\ (2+1)</math>, який редукується до терму типу <math>I\ \mathrm{nat}\ (2+1)\ 3</math>. Таким чином, у цій системі рівність типів означає те, що два значення одного типу конвертуються за допомогою редукції.

Наявність типу рівності є важливим, оскільки їм можна маніпулювати всередині системи. Ми можемо також визначити ''нерівність'' типів: як у {{Нп|Інтерпретація Брауера — Гейтінга — Колмогорова|інтерпретації Брауера — Гейтінга — Колмогорова||Brouwer–Heyting–Kolmogorov interpretation}}, відображаємо <math>\neg(a = b)</math> до <math>(a = b) \to \bot</math>. Тобто існує терм типу {{nobreak|<math>(I\ \mathrm{nat}\ 3\ 4) \to \bot</math>,}} але не існує терму типу <math>(I\ \mathrm{nat}\ 3\ 3) \to \bot</math>.

{{Нп|Гомотопічна теорія типів|||Homotopy type theory}} відрізняється від [[Інтуїціоністська теорія типів|теорії типів Мартіна-Льофа]] в основному тим, як в них визначаються типи рівності.

=== Індуктивні типи ===

Система теорії типів вимагає деяких базових термів і типів для роботи. Деякі системи будують їх з функцій за допомогою {{Нп|Кодування Черча|кодування Черча||Church encoding}}. Інші системи мають '''{{Нп|Індуктивний тип|індуктивні типи||Inductive type}}''': множину базових типів та множину [[Конструктор типу|конструкторів типів]], які генерують типи з правильними властивостями. Наприклад, [[Структурна індукція|певні рекурсивні функції]], побудовані на індуктивних типах, гарантовано припиняють свою роботу.

'''[[Коіндукція|Коіндуктивний]] тип'''&nbsp;— це нескінченний тип даних, створений шляхом задання функції, яка генерує наступний елемент.

'''{{Нп|Індукційна рекурсія|||Induction-recursion}}''' будує більш широкий діапазон типів, дозволяючи одночасно визначати тип і рекурсивні функції, що працюють на ньому.

=== Універсальний тип ===
Типи були створені для запобігання парадоксів, таких як [[Парадокс Расселла|парадокс Расселла]]. Проте мотиви, які призводять до таких парадоксів (здатність формулювати твердження про всі типи) все ще існують. Саме тому багато теорій типів мають «універсальний» тип, який містить всі інші типи (але не самого себе).

У системах, де ви можете стверджувати щось відносно універсальних типів, існує ієрархія універсальних типів, кожний з яких містить нижчий за ієрархією тип. Ця ієрархія визначається нескінченною, але ствердженя повинні стосуватися лише кінцевого числа універсальних рівнів.

Універсальні типи особливо складні в теорії типів. Первісна пропозиція теорії типів Мартіна-Льофа страждала від {{Нп|Парадокс Жирара|парадоксу Жирара||Girard's paradox}}.

=== Обчислювальна складова ===
Багато систем теорії типів, таких як {{Нп|просто типізоване лямбда-обчислення|||Simply typed lambda calculus}}, [[теорія типів Мартіна-Льофа]], [[обчислення конструкцій]], також є мовами програмування. Таким чином, кажуть, що вони мають «обчислювальну складову». Обчислення&nbsp;— це редукція термів мови за допомогою правил [[Рерайтинг (математика)|рерайтингу]].

Система теорії типів, яка має якісну обчислювальну складову, також має просте з'єднання з конструктивною математикою через {{Нп|Інтерпретація Брауера — Гейтінга — Колмогорова|інтерпретацію Брауера — Гейтінга — Колмогорова||Brouwer–Heyting–Kolmogorov interpretation}}.

== Теорії типів ==

=== Значні ===
* {{Нп|Просто типізоване лямбда-числення|||Simply typed lambda calculus}} (яке є {{Нп|Логіка вищого порядку|логікою вищого порядку||Higher-order logic}});
* [[теорія типів Мартіна-Льофа]];
* [[система F]];
* [[обчислення конструкцій]].

=== Другорядні ===
* {{Нп|Automath|||Automath}};
* деякі форми [[Комбінаторна логіка|комбінаторної логіки]];
* {{Нп|теорія типів ST|||ST type theory}};
* теорії типів, які визначені для [[лямбда-куб]]а;
* [[Типізоване лямбда-числення|типізоване лямбда-числення]];
* [[Чиста система типів|чисті системи типів]].

=== Активні ===
* {{Нп|Гомотопічна теорія типів|||Homotopy type theory}} зараз досліджується.

== Практичне використання ==

=== Мови програмування ===
{{Main|Система типізації}}

Існує тісний зв'язок між теорією типів та системами типізації. Системи типів є особливістю мов програмування, призначеної для виявлення помилок. Будь-який статичний аналіз програми, такий як алгоритми перевірки типу в фазі семантичного аналізу [[Компілятор|компілятором]], має зв'язок з теорією типів.

Яскравим прикладом є [[Agda]]&nbsp;— мова програмування, що використовує [[Теорія типів Мартіна-Льофа|теорію типів Мартіна-Льофа]] у якості своєї системи типів. Мова програмування [[ML (мова програмування)|ML]] була розроблена для маніпулювання теоріями типів та її власна система типів була під сильним впливом теорії типів.

=== Математичні основи ===
Перший комп'ютерний асистент, називався {{Нп|Automath|||Automath}}, використовував теорію типів для кодування математики на комп'ютері. {{Нп|Пер Мартін-Льоф|Мартін-Льоф||Per Martin-Löf}} спеціально розробив теорію типів, щоб кодувати всю математику для розробки нових математичних основ. Існує дослідження математичних основ з використанням {{Нп|Гомотопічна теорія типів|гомотопічної теорії типів||Homotopy type theory}}.

Математики, що працюють з [[Теорія категорій|теорією категорій]], вже мали труднощі при роботі з широко поширеною [[Теорія множин Цермело — Френкеля|теорією множин Цермело&nbsp;— Френкеля]]. Це призвело до таких пропозицій, як елементарна теорія категорій множин (ETCS<ref>{{Cite web|title=ETCS in nLab|url=https://ncatlab.org/nlab/show/ETCS|website=ncatlab.org|accessdate=2019-02-22|archive-date=23 лютого 2019|archive-url=https://web.archive.org/web/20190223020327/https://ncatlab.org/nlab/show/ETCS}}</ref>) Уільяма Ловера. Дослідники вивчають зв'язки між залежними типами (особливо типом ідентичності) та [[Алгебрична топологія|алгебричною топологією]] (зокрема [[Гомотопія|гомотопією]]).

=== Асистенти для доказів ===
Значна частина сучасних досліджень теорії типів проводиться для розвитку автоматизованої перевірки доказів, інтерактивних асистентів для доказів та автоматизованих доказів теорем. Більшість цих систем використовують теорію типів як математичну основу для кодування доказів, що не дивно, враховуючи тісний зв'язок між теорією типів і мовами програмування:
* Багато теорій типів, побудованих на {{Нп|Логіка вищого порядку|логіці вищого порядку||Higher-order logic}}, використовуються для систем {{Нп|HOL|||HOL (proof assistant)}} and {{Нп|Prototype Verification System|||Prototype Verification System}};
* [[теорія типів Мартіна-Льофа]] використовується [[Agda]]&nbsp;— мовою програмування та асистентом для доказів;
* обчислювальна теорія типів використовується {{Нп|NuPRL|||NuPRL}};
* обчислення конструкцій використовується [[Coq]] та {{Нп|Matita|||Matita}}.

Багато теорій типів використовуються асистентами для доказів {{Нп|LEGO (асистент для доказів)|LEGO||LEGO (proof assistant)}} та {{Нп|Isabelle (асистент для доказів)|Isabelle||Isabelle (proof assistant)}}. Isabelle, окрім теорій типів, також використовує [[Теорія множин Цермело — Френкеля|теорію множин Цермело&nbsp;— Френкеля]]. {{Нп|Система Mizar|Mizar||Mizar system}} є прикладом системи для доказів, яка використовує тільки теорію множин.

=== Лінгвістика ===
Теорія типів також широко використовується у формальних теоріях семантики природних мов, особливо у [[Граматика Монтегю|граматиці Монтегю]] та її нащадків. Зокрема, категориальні граматики та граматики прегруп широко використовують конструктори типів для визначення типів слів (''іменник'', ''дієслово'', тощо).

Найбільш поширена конструкція приймає базові типи <math>e</math> та <math>t</math> відповідно у якості індивіда та [[Значення істинності|значення істинності]], а потім рекурсивно визначає множину типів таким чином:
* якщо <math>a</math> та <math>b</math> є типами, то також типом є і <math>\langle a,b\rangle</math>;
* типами є тільки базові типи та ті типи, які були побудовані способом, описаним у попередньому пункті.

Комплексний тип <math>\langle a,b\rangle</math>&nbsp;— це тип [[Функція (математика)|функцій]] від об'єктів типу <math>a</math> до об'єктів типу <math>b</math>. Таким чином, існують типи виду <math>\langle e,t\rangle</math>, які інтерпретуються як елементи множини функцій від об'єктів до значень істинності, тобто [[Характеристична функція|характеристичних функцій]] множин об'єктів. Вираз типу <math>\langle\langle e,t\rangle,t\rangle</math> є функцією від множини об'єктів до значень істинності. Цей тип є стандартним типом кванторів природної мови, таких як ''всі'' або ''ніхто''.

З прикладних лінгвістичних систем можна відзначити [[логічний фреймворк]] [[Grammatical Framework]], що збудований на основі теорії типів Мартіна-Льофа.

=== Соціальні науки ===
[[Грегорі Бейтсон]] вніс теорію логічних типів до соціальних наук; його визначення [[Подвійне послання|подвійного послання]] та [[логічних рівнів]] ґрунтуються на теорії типів Расселла.

== Зв'язок з теорією категорій ==
Хоча початкова мотивація [[Теорія категорій|теорії категорій]] була далекою від фундаменталізму, вона мала глибокі зв'язки з теорією типів. Як писав Джон Белл: «Насправді, категорії можуть самі себе розглядати як теорії типів певного роду; цей факт сам по собі свідчить про те, що теорія типів більш тісно пов'язана з теорією категорій, ніж теорією множин.» Коротко кажучи, категорію можна розглядати як теорію типів, вважаючи її об'єкти типами. Нижче наведено ряд важливих результатів:<ref name="Sets and Extensions in the Twentieth Century">{{cite book|title=Handbook of the History of Logic. Volume 6. Sets and Extensions in the Twentieth Century|year=2012|publisher=Elsevier|isbn=978-0-08-093066-4|author=John L. Bell|chapter=Types, Sets and Categories|url=http://publish.uwo.ca/~jbell/types.pdf|editor=Akihiro Kanamory|accessdate=21 лютого 2019|archive-date=17 квітня 2018|archive-url=https://web.archive.org/web/20180417105624/http://publish.uwo.ca/~jbell/types.pdf}}</ref>
* декартово замкнені категорії відповідають типізованому лямбда-численню (Ламбек, 1970);
* C-моноїди (категорії з множенням, зведенням в ступінь та єдиним нетермінальним об'єктом) відповідають нетипізованому лямбда-численню (було самостійно спостережено Ламбеком та [[Дана Скотт|Скоттом]], 1980);
* локально декартово замкнені категорії відповідають теорії типів Мартіна-Льофа (1984).

== Див. також ==
* [[Тип даних]]&nbsp;— конкретні типи даних у програмуванні
* [[Система типізації]]&nbsp;— більш практичне обговорення систем типів для мов програмування

== Примітки ==
{{reflist}}

== Література ==
* C. Aarts, R. Backhouse, P. Hoogendijk, E. Voermans & J. van der Woude (December 1992) [https://www.researchgate.net/profile/Roland_Backhouse/publication/277287583_A_RELATIONAL_THEORY_OF_DATATYPES/links/563209fb08ae506cea687d68.pdf A Relational Theory of Datatypes] {{Webarchive|url=https://web.archive.org/web/20180914061428/https://www.researchgate.net/profile/Roland_Backhouse/publication/277287583_A_RELATIONAL_THEORY_OF_DATATYPES/links/563209fb08ae506cea687d68.pdf |date=14 вересня 2018 }} via [[ResearchGate]]
* {{cite book
  | first = Peter
  | last = Andrews B.
  | year = 2002
  | isbn = 978-1-4020-0763-7
  | title = An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed.
  | url = https://archive.org/details/introductiontoma0000andr_h2a3
  | publisher = Kluwer Academic Publishers.
}}
* {{cite book
 | first = Bart
 | last = Jacobs
 | title = Categorical Logic and Type Theory
 | year = 1999
 | publisher = North Holland, Elsevier
 | isbn = 0-444-50170-3
 | series = Studies in Logic and the Foundations of Mathematics 141
 | url = http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html
 | accessdate = 21 лютого 2019
 | archive-date = 26 квітня 2019
 | archive-url = https://web.archive.org/web/20190426183520/http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html
 }} Covers type theory in depth, including polymorphic and dependent type extensions. Gives [[categorical semantics]].
* Cardelli, Luca, 1997, «[http://citeseer.ist.psu.edu/cardelli97type.html Type Systems,] {{Webarchive|url=https://web.archive.org/web/20080410185229/http://citeseer.ist.psu.edu/cardelli97type.html |date=10 квітня 2008 }}» in Allen B. Tucker, ed., ''The Computer Science and Engineering Handbook''. CRC Press: 2208&ndash;2236.
* {{cite book
  | first = Jordan E.
  | last = Collins
  | year = 2012
  | isbn = 978-3-8473-2963-3
  | title = A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'
  | publisher = LAP Lambert Academic Publishing
  | url = http://hdl.handle.net/11375/12315
}} 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'.
* [[Robert Lee Constable|Constable, Robert L.]], 2002, «[https://web.archive.org/web/20120227104114/http://www.nuprl.org/documents/constable/naive.pdf Naïve Computational Type Theory,]» in H. Schwichtenberg and R. Steinbruggen (eds.), ''Proof and System-Reliability'': 213&ndash;259. Intended as a type theory counterpart of [[Paul Halmos]]'s (1960) ''[[Naive Set Theory (book)|Naïve Set Theory]]''
* [[Thierry Coquand]]&nbsp;— [http://plato.stanford.edu/entries/type-theory/ Type Theory] {{Webarchive|url=https://www.webcitation.org/6I8yplVjN?url=http://plato.stanford.edu/entries/type-theory/ |date=16 липня 2013 }}, [[Stanford Encyclopedia of Philosophy]].
* Thompson, Simon, 1991. ''[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming] {{Webarchive|url=https://web.archive.org/web/20210323203228/http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ |date=23 березня 2021 }}''. 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).<!-- no idea why these get different ISBNs, they don't appear to be different editions--> A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. [https://web.archive.org/web/20110607234927/http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf 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, [https://pure.tue.nl/ws/files/1383309/498552.pdf ''The evolution of type theory in logic and mathematics''] {{Webarchive|url=https://web.archive.org/web/20190222151932/https://pure.tue.nl/ws/files/1383309/498552.pdf |date=22 лютого 2019 }}, PhD thesis, Eindhoven University of Technology, 1997.
{{Типи даних}}
{{Математична логіка}}
[[Категорія:Математична логіка]]
[[Категорія:Теорія типів]]
[[Категорія:Типи даних]]
[[Категорія:Основи математики]]