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

Когда мы говорим 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-алгебр.

Замечательная особенность параметрического полиморфизма состоит в том, что он продолжает работать и в ситуации, когда терминального объекта не существует. ( Read more... )

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

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

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