Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Ещё одно введение в теории типов

В математике понятие “теория типов” развивается, и ещё непонятно в какой общности нужно будет давать определение. В контексте информатики теориями типов называют обобщения λ — просто типизированного лямбда-исчисления.

В сущности, теория типов — набор правил, которые позволяют конструировать выражения из подвыражений, в ситуации когда не любые выражений комбинируются, а только правильно стыкующиеся. Чтобы выразить “стыкуемость” вводится понятие типов (и набор правил, как эти типы записывать). Если терм x имеет тип T, пишут x : T. В λ всегда имеется какой-то набор базовых типов (например, тип Nat, содержащий все натуральные числа), и типы, получаемые из базовых X и Y путём применения оператора X -> Y.

После того как описано, какие бывают типы, можно записывать те самые правила конструирования выражений. Например:
  f : X -> Y    x : X
————————————––––––––––—
         f(x)


Для того, чтобы получившиеся выражения тоже можно было стыковать с чем-то дальше, в теорию типов добавляются дополнительные виды правил, как минимум требуется указать тип для любого сконструированного выражения:
  f : X -> Y    x : X
————————————––––––––––—
       f(x) : Y


Но в более сложных системах может хотеться, чтобы можно было применить f : X -> Y к такому x : X', что X и X' не совпадают “побуквенно”, но одно и то же по-существу (ну либо X' является подтипом X). Тогда нам нужны ещё правила конверсии типов, которые говорят в каких случаях X' ≼ X. Давайте предположим, что мы добавили в базовые типы нашего λ кроме самого Nat ещё типы Fin(n) дла каждого n : Nat, содержащие натуральные числа меньше n. То есть, у нас появились зависимые типы (такие операторы, которые превращают выражение какого-то фиксированного типа в тип, Fin(n) — как раз пример такого). Теперь нам хочется, чтобы туда, где требуется Fin(n) можно было подставить Fin(m), если n и m равны. То есть нам уже нужны правила равенства и для выражений. И правило, что если n = m, то Fin(n) ≼ Fin(m).

Существует два принципиально разных подхода к онтологии теорий типов — либо мы считаем, что есть некое данное свыше множество “сырых выражений” которые мы типизируем, либо мы вместе с типами задаём, какие выражения их населяют, с строим теорию снизу-вверх.

λ(Nat) и λ(Nat, Fin) можно сформулировать обоими способами. Можно сказать, что тип Nat состоит из лямбда-выражений
(\f ↦ (\x ↦ x))
(\f ↦ (\x ↦ f(x)))
(\f ↦ (\x ↦ f(f(x))))
...
А типы Fin(n) из нижних подмножеств этих выражений. Типы X -> Y, понятное, дело, тоже из лямбда-выражений. Тогда у нас, получается, любые типы состоят из лямбда-выражений, и для выражения любой “программы” не требуется ничего, кроме абстракции и применения. Между прочим, эта система типов позволяет записать в точности все рекурсивные функции, тотальность которых доказывается в арифметике первого порядка PA, и наоборот любому утверждению на языке арифметике первого порядка можно сопоставить функцию, определимую в этой теории типов, тотальность которой эквивалентна верности исходного утверждения. Можно также расширить λ(Nat, Fin) до λ×→(Nat, Fin) типом пар X × Y, и сказать что пара (x, y) это на самом деле лямбда-выражение (\f ↦ f(x)(y)). Всё ещё все типы населены только лямда-выражениями. Кстати, добавления типа пар добавляет λ только выразительности, но не силы — определимые там и там рекурсивные функции совпадают.

Такой подход называется PTS — Pure Type Systems. Активно разрабатываемая сейчас система Cedille показывается, что в рамках PTS можно сделать очень мощные системы типов, в частности включающие MLTT c Π, Σ и W-типами (более того, индексированными индуктивными типами), а ещё вероятно интенсиональными Id-типами (без UIP), но без вселенных и large elimination.

Можно, наоборот, сказать, что в λ(Nat) тип Nat состоит из особенных атомов Zero, Succ(Zero), Succ(Succ(Zero)) и т.д., и для них есть оператор паттерн-матчинга, а лямбда-выражения между двумя типами строятся индуктивно при помощи собственно конструкторов лямбда-выражений и операторов паттерн-матчинга. На этом пути, добавляя другие базовые типы и конструкторы типов мы тоже можем обобщать теорию без видимых пределов.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments