Пример: Теория зависимых типов
Как и логика, теория типов имеет множество расширений и вариантов, включая версии первого и более высокого порядка. Одна из ветвей, известная как теория зависимых типов , используется в ряде компьютерных систем доказательства. Теория зависимых типов позволяет квантификаторам варьироваться по самим программам. Эти квантифицированные типы записываются как Π и Σ вместо ∀ и ∃ и имеют следующие правила формирования :
| Γ ⊢ A тип Γ , x: A ⊢ B тип ───────────────────────────── Π-F Γ ⊢ Π x: A. Тип B | Γ ⊢ A тип Γ , x: A ⊢ B тип ──────────────────────────── Σ-F Γ ⊢ Σ x: A. Тип B |
Эти типы являются обобщениями типов стрелки и продукта соответственно, о чем свидетельствуют их правила введения и исключения.
| Γ , x : A ⊢ π : B ──────────────────── ΠI Γ ⊢ λ x . π : Π x : A . B | Γ ⊢ π 1 : Πx : A . B Γ ⊢ π 2 : A ───────────────────────────── ΠE Γ ⊢ π 1 2 : [π2/x] B |
| Γ ⊢ π 1 : A Γ, x:A ⊢ π 2 : B ───────────────────────────── ΣI Γ ⊢ ( π 1 , 2) : Σx: A. B | Γ ⊢ π : Σ x: A. B ──────────────── ΣE1 Γ ⊢ первое число π : A | Γ ⊢ π : Σ x: A. B ──────────────────────── ΣE2 Γ ⊢ snd π : [fst π/x] B |
Теория зависимых типов в полной общности очень мощна: она способна выразить практически любое мыслимое свойство программ непосредственно в типах программы. За эту общность приходится платить высокую цену — либо проверка типов неразрешима ( экстенсиональная теория типов ), либо экстенсиональное рассуждение сложнее ( интенсиональная теория типов ). По этой причине некоторые теории зависимого типа не допускают количественной оценки произвольных программ, а скорее ограничиваются программами заданной разрешимой области индексов, например целыми числами, строками или линейными программами.
Поскольку теории зависимых типов допускают зависимость типов от программ, возникает естественный вопрос, возможно ли, чтобы программы зависели от типов или любой другой комбинации. На такие вопросы существует множество вариантов ответов. Популярный подход в теории типов заключается в том, чтобы разрешить количественную оценку программ по типам, также известный как параметрический полиморфизм ; их существует два основных вида: если типы и программы хранятся отдельно, то получается несколько более корректная система, называемая предикативным полиморфизмом ; если различие между программой и типом размыто, получается теоретико-типологический аналог логики высшего порядка, также известный как непредикативный полиморфизм . В литературе рассматривались различные комбинации зависимости и полиморфизма, наиболее известным из которых является лямбда-куб Хенка Барендрегта .
Пересечение логики и теории типов является обширной и активной областью исследований. Новые логики обычно формализуются в рамках общей теории типов, известной как логическая структура . Популярные современные логические системы, такие как исчисление конструкций и LF , основаны на теории зависимых типов высшего порядка с различными компромиссами с точки зрения разрешимости и выразительности. Эти логические структуры сами по себе всегда определяются как системы естественной дедукции, что является свидетельством универсальности подхода естественной дедукции.