Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Коданные и параметричность, диалгебры

Когда мы говорим Nat-алгебра, подразумеваем объект, снабженный морфизмами zero и succ.

@Structure NatAlgebra(@on N : Type):
  zero : N
  succ : N -> N


Когда говорим Nat (индуктивный тип), подразумеваем инициальный объект в категории таких алгебр. Когда говорим CoNat (коиндуктивный тип), подразумеваем терминальный объект в категории таких алгебр, если он существует. Терминальность CoNat означает, что для всякой Nat-алгебры A существует каноническое отображение extend[A] : A.N -> CoNat.

А теперь внимание: всякая определимая синтаксически (средствами той или иной теории типов) чистая функция вида
f : [A : NatAlgebra] A.N -> X
задаёт в том числе и f* : CoNat -> X, и может благодаря параметрическому полиморфизму обязана восстанавливаться из неё: f[A] = f* ∘ extend[A]. Т.е. задать функцию из коиндуктивного типа данных структуры F с это абсолютно то же самое, что определить полиморфную функцию для всех F-алгебр.

Замечательная особенность параметрического полиморфизма состоит в том, что он продолжает работать и в ситуации, когда терминального объекта не существует. В теории типов важнейшим примером такого рода являются вселенные: мы пишем (x : Type), как будто бы Type в самом деле был терминальным объектом в категории вселенных, но там его нет: вместо одного объекта там есть направленное множество вселенных, не имеющее предела. Однако параметрический полиморфизм позволяет нам писать функции работающие для любой из этих вселенных, и, благодаря этому, работать на синтаксическом уровне так, как будто бы терминальный объект Type на самом деле существовал (с тем единственным исключением, что нужно вводить синтаксические ограничения, предотвращающие нарушение предикативности).

Разумеется, Type не единственный пример такого рода даже в рамках теоретикотиповых категорий, где морфизмов очень мало (только синтаксически-определимые отображения, в том числе только непрерывные) достаточным условием для изоморфизма является возможность определить бисимуляцию. Если же обратиться к теоретико-множественным категориям F-алгебр, то за исключением совсем тривиальных случаев в таких категориях терминальные объекты (даже слабые терминальные объекты, которые более естественно рассматривать в этом контексте) могут существовать только если мы рассматриваем алгебры не выше того или иного кардинала, но даже тогда это случается редко: в точности для счётно-категоричных теорий F, если мы ограничиваемся счётными моделями, и несчётно-категоричных моделей, если мы ограничиваемся любым другим кардиналом.

Вышеозначенная особенность теорий типов (возможность как будто работать с терминальными объектами, которых на самом деле нет) интересна с точки зрения теории моделей, особенно позитивной теории моделей (естественного обобщения классической теории моделей теорий первого порядка для теорий высшего порядка).

* * *

Коль скоро я заговорил об F-алгебрах для разных структур F, следует, наверное, обрисовать что такое F семантически и как определяется категория таких алгебр.

Посмотрим на определение структуры NatAlgebra выше. Какую информацию нам надо “записать”? Нам нужно записать входные и выходные типы наших zero и succ. Это удобнее всего сделать при помощи двух функторов I O : Type -> Type
I(N) => (Unit, N)
O(N) => (N, N)

Морфизм I(N) -> O(N) представляет из себя пару морфизмов (Unit -> N, N -> N), точно то чем нам нужно снабдить N, чтобы N стала Nat-алгеброй. Чтобы иметь возможность кодировать не только структуру, но и свойства (предикаты), нам необходимо допускать зависимость выходных типов от входных значений у этих самых морфизмов, чтобы это сделать, нужно расширить домен и кодомен функторов, вместо Type -> Type следует допускать некое произвольное расслоение T, и требовать чтобы морфизм I(X) -> O(X) был вертикальным.

Для любой one-sorted theory (моноид, группа, множество с линейным порядком) мы можем записать такие вот I и O, что вся нужная дополнительная структура и все нужные дополнительные свойства будут зашиты в морфизме I(X) -> O(X). В том числе таким образом уже можно закодировать все простые индуктивные и коиндуктивные типы включая Пи- и Сигма-типы.

Но вообще говоря структуры бывают multi-sorted, вот например когда мы хотим задать векторное пространство, мы ещё и поле указываем, над которым это векторное пространство линейно, там уже два типа (K и V) оснащаются структурами и свойствами. То бишь в общем случае у нас есть некий index set J сортов нашей теории и пара функторов I O : (J -> T) -> T, и вот тройка (J, I, O) уже и задают нашу структуру.
(J, I, O)-алгебра это просто пара, состоящая из носителя C : (J -> Type) и структуры s : I(C) -> O(C). Такие пары естественным образом образуют категорию, и вот в ней-то мы и ищем когда нам нужно инициальные и терминальные объекты. Таким образом мы получаем ещё семантику для индуктивно-индуктивных типов. Эта семантика известна как dialgebraic semantics (слово диалгебра используется в том смысле, что в определении используется два функтора), и изначально предложена Hagino, а затем сильно развита Basold'ом. В рамках диалгебраического фреймворка можно представить все встречающиеся на данный момент в языках программирования на основе MLTT типы, кроме вселенных и индуктивно-рекурсивных типов, что, кстати, наверное неспроста так совпало*.

Мне по сей день неизвестно, как в рамках диалгебраической семантики проинтерпретировать индуктивно-рекурсивные типы. Специалисты, ау! Кто-нибудь знает хоть что-нибудь про это? Оно не гуглится совершенно.

Это невероятно интересный вопрос, т.к. двойственные к ним типы — это те самые Very Dependent Types (= Reedy Limits), при помощи которых можно интерпретировать всякие симплициальные типы и обобщённые алгебраические теории (GATs).

____
* Структура a la Tarski вселенных может быть описана в терминах индукции-рекурсии, соответственно если можно будет определить структуру TarskiAlgebra, то функции полиморфные по типам [T : Type] X -> Y можно будет эквивалентно описывать как структуры полиморфные по [Univ : TarskiAlgebra] (T : Univ) X -> Y.
Subscribe

  • О программировании, из комментов у vit_r

    orleans: У ФП есть обьективные преимущества в плане исполнения на многопроцессорных системах и организации юнит тестов. Все то что можно…

  • Effect typing in short

    There are many different classes of functions out there. There are pure functions and there are functions with diverse side effects. Some can perform…

  • Towards Scala 3

    I'd like to share some ideas on features that might be included into next major Scala releases. Some of them might come in question already for Scala…

  • 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.
  • 9 comments