Теорія типів

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

Теорія типів тісно пов'язана з системами типів — особливістю мов програмування, яка призначена для зменшення кількості помилок. Теорія типів була розроблена для обходження парадоксів формальної логіки.

Однією з найвідоміших теорій типів є типізоване лямбда-числення Алонзо Черча та інтуїціоністська теорія типів Пера Мартіна-Льофа.

Історія

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

Найвідомішим прикладом використання типів є просто типізоване лямбда-числення Алонзо Черча. Теорія типів Черча допомогла формальним системам уникнути парадоксу Кліні — Россера, присутнього у оригінальному безтиповому лямбда-численні. Черч продемонстрував, що ця теорія може служити основою для математики.

Базові поняття

У системі теорії типів кожен терм має тип. Наприклад, $4$, $2+2$ та $2\cdot 2$ є окремими термами типу $\mathrm {nat}$, тобто натуральними числами. Традиційно терм супроводжується двокрапкою і його типом, наприклад, $2:\mathrm {nat}$.

Теорії типів мають явне обчислення, яке кодується правилами рерайтингу термів. Вони називаються правилами перетворення або, якщо правило працює лише в одному напрямку, правилом редукції. Наприклад, $2+2$ та $4$ є синтаксично різними термами, але перший терм редукується до другого. На запису ця редукція має вигляд $2+2\twoheadrightarrow 4$.

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

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

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

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

• Теорія множин побудована поверх логіки. Вона вимагає окремої системи, подібної логіці першого порядку. У теорії типів поняття типу «і» та «або» можуть бути закодовані як типи самої теорії типів.
• У теорії множин елемент може належати до безлічі різних множин, до підмножини, або до множини множин. У теорії типів терми, як правило, належать тільки до одного типу. (Там, де використовуються підмножини, теорія типів прагне використовувати функцію предикатів, яка повертає $true$, якщо терм знаходиться в підмножині, та повертає $false$ в іншому випадку. Об'єднання двох типів можна зробити, створивши новий тип, який називається типом-сумою та містить нові терми.)
• Теорія множин зазвичай кодує числа як множини. ($0$ — порожня множина, $1$ — множина, що містить порожню множину, і т. д.) Теорія типів може кодувати числа як функції, використовуючи кодування Черча, або як індуктивні типи. Індуктивні типи створюють нові константи для функції наступника і нуль, що дуже нагадує аксіоми Пеано.
• Теорія множин використовує нотацію побудови множини.
• Теорія типів має просте з'єднання з конструктивною математикою через інтерпретацію Брауера — Гейтінга — Колмогорова та може бути пов'язана з логікою ізоморфізмів Каррі — Говарда. Деякі теорії типів тісно пов'язані з теорією категорій.

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

Нормалізація

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

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

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

Залежні типи

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

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

Залежні типи відіграють центральну роль в теорії типів Мартіна-Льофа та в розробці функційних мов програмування, таких як Idris, ATS, Agda та Epigram .

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

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

У теорії типів Мартіна-Льофа тип рівності (який також називається типом ідентичності) позначається як $I$ (від англ. Identity). Кажуть, що існує тип $I\ A\ a\ b$, коли $A$ є типом, а $a$ і $b$ — це терми типу $A$. Терм типу $I\ A\ a\ b$ інтерпретується як визначення рівності $a$ та $b$.

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

Наявність типу рівності є важливим, оскільки їм можна маніпулювати всередині системи. Ми можемо також визначити нерівність типів: як у інтерпретації Брауера — Гейтінга — Колмогорова, відображаємо $\neg (a=b)$ до $(a=b)\to \bot$. Тобто існує терм типу $(I\ \mathrm {nat} \ 3\ 4)\to \bot$, але не існує терму типу $(I\ \mathrm {nat} \ 3\ 3)\to \bot$.

Гомотопічна теорія типів відрізняється від теорії типів Мартіна-Льофа в основному тим, як в них визначаються типи рівності.

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

Система теорії типів вимагає деяких базових термів і типів для роботи. Деякі системи будують їх з функцій за допомогою кодування Черча. Інші системи мають індуктивні типи: множину базових типів та множину конструкторів типів, які генерують типи з правильними властивостями. Наприклад, певні рекурсивні функції, побудовані на індуктивних типах, гарантовано припиняють свою роботу.

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

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

Універсальний тип

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

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

Універсальні типи особливо складні в теорії типів. Первісна пропозиція теорії типів Мартіна-Льофа страждала від парадоксу Жирара.

Обчислювальна складова

Багато систем теорії типів, таких як просто типізоване лямбда-обчислення, теорія типів Мартіна-Льофа, обчислення конструкцій, також є мовами програмування. Таким чином, кажуть, що вони мають «обчислювальну складову». Обчислення — це редукція термів мови за допомогою правил рерайтингу.

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

Теорії типів

Значні

• Просто типізоване лямбда-числення (яке є логікою вищого порядку);
• теорія типів Мартіна-Льофа;
• система F;
• обчислення конструкцій.

Другорядні

• Automath;
• деякі форми комбінаторної логіки;
• теорія типів ST;
• теорії типів, які визначені для лямбда-куба;
• типізоване лямбда-числення;
• чисті системи типів.

Активні

• Гомотопічна теорія типів зараз досліджується.

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

Мови програмування

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

Яскравим прикладом є Agda — мова програмування, що використовує теорію типів Мартіна-Льофа у якості своєї системи типів. Мова програмування ML була розроблена для маніпулювання теоріями типів та її власна система типів була під сильним впливом теорії типів.

Математичні основи

Перший комп'ютерний асистент, називався Automath, використовував теорію типів для кодування математики на комп'ютері. Мартін-Льоф спеціально розробив теорію типів, щоб кодувати всю математику для розробки нових математичних основ. Існує дослідження математичних основ з використанням гомотопічної теорії типів.

Математики, що працюють з теорією категорій, вже мали труднощі при роботі з широко поширеною теорією множин Цермело — Френкеля. Це призвело до таких пропозицій, як елементарна теорія категорій множин (ETCS) Уільяма Ловера. Дослідники вивчають зв'язки між залежними типами (особливо типом ідентичності) та алгебричною топологією (зокрема гомотопією).

Асистенти для доказів

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

• Багато теорій типів, побудованих на логіці вищого порядку, використовуються для систем HOL and Prototype Verification System;
• теорія типів Мартіна-Льофа використовується Agda — мовою програмування та асистентом для доказів;
• обчислювальна теорія типів використовується NuPRL;
• обчислення конструкцій використовується Coq та Matita.

Багато теорій типів використовуються асистентами для доказів LEGO та Isabelle. Isabelle, окрім теорій типів, також використовує теорію множин Цермело — Френкеля. Mizar є прикладом системи для доказів, яка використовує тільки теорію множин.

Лінгвістика

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

Найбільш поширена конструкція приймає базові типи $e$ та $t$ відповідно у якості індивіда та значення істинності, а потім рекурсивно визначає множину типів таким чином:

• якщо $a$ та $b$ є типами, то також типом є і $\langle a,b\rangle$;
• типами є тільки базові типи та ті типи, які були побудовані способом, описаним у попередньому пункті.

Комплексний тип $\langle a,b\rangle$ — це тип функцій від об'єктів типу $a$ до об'єктів типу $b$. Таким чином, існують типи виду $\langle e,t\rangle$, які інтерпретуються як елементи множини функцій від об'єктів до значень істинності, тобто характеристичних функцій множин об'єктів. Вираз типу $\langle \langle e,t\rangle ,t\rangle$ є функцією від множини об'єктів до значень істинності. Цей тип є стандартним типом кванторів природної мови, таких як всі або ніхто.

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

Соціальні науки

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

Зв'язок з теорією категорій

Хоча початкова мотивація теорії категорій була далекою від фундаменталізму, вона мала глибокі зв'язки з теорією типів. Як писав Джон Белл: «Насправді, категорії можуть самі себе розглядати як теорії типів певного роду; цей факт сам по собі свідчить про те, що теорія типів більш тісно пов'язана з теорією категорій, ніж теорією множин.» Коротко кажучи, категорію можна розглядати як теорію типів, вважаючи її об'єкти типами. Нижче наведено ряд важливих результатів:

• декартово замкнені категорії відповідають типізованому лямбда-численню (Ламбек, 1970);
• C-моноїди (категорії з множенням, зведенням в ступінь та єдиним нетермінальним об'єктом) відповідають нетипізованому лямбда-численню (було самостійно спостережено Ламбеком та Скоттом, 1980);
• локально декартово замкнені категорії відповідають теорії типів Мартіна-Льофа (1984).

Див. також

• Тип даних — конкретні типи даних у програмуванні
• Система типізації — більш практичне обговорення систем типів для мов програмування

Література

• C. Aarts, R. Backhouse, P. Hoogendijk, E. Voermans & J. van der Woude (December 1992) A Relational Theory of Datatypes [Архівовано 14 вересня 2018 у Wayback Machine.] 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 0-444-50170-3. Архів оригіналу за 26 квітня 2019. Процитовано 21 лютого 2019. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
• Cardelli, Luca, 1997, «Type Systems, [Архівовано 10 квітня 2008 у Wayback Machine.]» 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. 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 Coquand — Type Theory [Архівовано 16 липня 2013 у WebCite], Stanford Encyclopedia of Philosophy.
• Thompson, Simon, 1991. Type Theory and Functional Programming [Архівовано 23 березня 2021 у Wayback Machine.]. 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 [Архівовано 22 лютого 2019 у Wayback Machine.], PhD thesis, Eindhoven University of Technology, 1997.