Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Large quantification

Начинаю прозревать, как понимать proof irrelevant quantification/erasure и large quantification в теории типов.

В MLTT бывают П-типы, мы будем обозначать из через (x : X) -> Y(x), это типы лямбда выражений, которые делают чего хотят с иксом, и возвращают значения Y(x) типа, тоже зависимого от X.
В System F (и самых разных её обобщениях) также бывают ∀-типы, их мы будем обозначать через [X : ∗] -> Y[X], в них тип результата тоже может зависеть от x, однако “анализировать” x в ходе вычислений нельзя, имеет место erasure, x нужен только для тайпчекинга и рассуждений о свойствах программы, а в рантайм не просачивается. Вообще говоря вместо звёздочки означающей “тип” мы будем в записи [X : T] -> Y[X] допускать и другие тайпклассы T, такие как Nat, List или Monoid, об я ещё поговорю ниже.

Когда я рассуждаю о теориях типов я подспудно всегда думаю об intended-семантике, т.е. что теория типов это внутренний язык какой-то локально декартово-замкнутой (∞, 1)-категории C с какими-то дополнительными плюшками (типа существования в ней натуральных чисел, классификаторов объектов и т.д.), и типы суть объекты категории, а термы — морфизмы, зависимые типы — расслоения. И мне всё не давал покою вопрос: какая же семантика у ∀-типов?
Спойлер: это расслоенные категории (https://ncatlab.org/nlab/show/Grothendieck+fibration). Причём, как правило, эти категории по отношению к C большие, и расслоены также над большими категориями. Ниже мы сможем без труда восстановить и классический пример — (большую) категорию модулей Mod, расслоенную над (большой) категорией колец Ring.

Понять это мне не удавалось потому, что я раньше я думал только об одном естественном классе в теории типов, классе всех типов ∗. Однако продуктивнее сперва подумать о вещах попроще.

Когда мы пишем (n : Nat), мы подразумеваем, что n принадлежит вполне конкретному типу Nat. Типу для которого выполняется каноничность, т.е. любой замкнутый терм этого типа подстановочно равен какому-то конкретному каноническому представителю Nat (т.е. натуральному числу). Благодаря этому знанию мы можем применять к элементам n : Nat элиминатор, не нарушая тотальности языка.

Когда мы пишем [n : Nat], мы подразумеваем, что n имеет тип, в котором всё ещё есть элемент zero, и к элементам которого всё ещё можно применять succ, но элиминаторы к n теперь применять нельзя, потому что каноничность не гарантирована, типу n позволено иметь произвольное количество дополнительных экзотических элементов. Отметим, что при определении типов конечных чисел Fin[n : Nat] или конечных списков Vec[n : Nat][T : ∗], к индексам n применяются succ и zero, однако нигде не используются элиминаторы, что позволяет совершенно спокойно использовать квадратные скобки. Именно в этом отличие между индексами и параметрами; именно это гарантирует, что индексы имеют значение только при тайпчекинге, но не в рантайме. Отметим, что у стандартных вселенных в MLTT элиминаторов нет, поэтому квантификация по типу всегда ∀.

Nat определяется как инициальный объект в категории Nat-алгебр — алгебр над функтором N -> (zero : N, succ : N -> N). Теперь предположим у нас есть терм t[n], где к n разрешается применять конструкторы zero и succ (это значит n должен быть из какой-то Nat-алгебры), однако не разрешается применять элиминатор (значит не требуется инициальности), стало быть наш терм полиморфен по входному типу: это может быть любой тип из категории Nat-алгебр. Так вот полиморфно-зависимый от [n : Nat] терм порождает категорию расслоенную над категорией Nat-алгебр.

Теперь можно без труда понять и что такое ∗: это (большая по отношению к C) категория всех вселенных C. Соответственно полиморфные типы, такие как List[T : ∗], также образуют большую категорию, расслоенную над ∗. Для каждого конкретного типа List[T] это фиксированный тип, для каждой фиксированной вселенной List(T : U) это просто отображение из U в другую вселенную, но вот целиком эта полиморфная штука — категория, расслоенная над ∗. Точно также и привычные нам тайпклассы, такие как Monoid = [T : ∗](id : T, compose : T × T -> T, associator : ...), образуют категории, расслоенные над ∗. И первый пример, категорию Nat-алгебр, разумеется, тоже можно задать через тайпкласс Nat = [T : ∗](zero : T, succ : T -> T), и она, разумеется, тоже расслоена над ∗. Если я правильно понимаю, расслоенность над ∗ означает в точности, что категория “большая” относительно С. В теории множеств NBG критерий малости именно такой, там постулируется, что класс K представим множеством тогда и только тогда, когда нет изоморфизма между K и V, где V класс всех множеств.

В статье “I Got Plenty o’ Nuttin’” Connor McBride ставит вопрос «What is an icon?», в смысле аналог типа T для proof-irrelevant quantification, мне кажется, мы можем ответить на этот вопрос для индуктивных типов, а для понимания как это должно работать с кортежами и П-типами (общее говоря, коиндуктивными типами) можем воспользоваться подходом из статьи: 0(A, B) должно быть (0A, 0B), т.е. 0(A, B) это максимально общая категория одновременно расслоенная над категорией 0A и 0B, а 0(x : X -> B[x]) это максимально общая категория, расслоенная над каждой из категорий B[x]. Нетрудно увидеть, что при таком подходе, если категория X имеет инициальный объект X, терм t : [x : X] -> Y(x) можно читать и как t : (x : X) -> Y(x). Менее понятно, как это всё выглядит в присутствии линейных типов.

Ещё надо внимательно подумать, какая квантификация имеет место у id-типов. Правда ли что Id[T : ∗](a b : T)?
Или может быть всё-таки Id[T : ∗][a : T](b : T), где Id[T : ∗][a : T] автоматически обладает структурой алгебры Хопфа, как нам подсказывает квантовомеханическая интуиция?
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.
  • 6 comments