Oct. 23rd, 2016

akuklev: (ДР Цертуса 2011)
Когда мы говорим 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.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 28th, 2017 04:46 pm
Powered by Dreamwidth Studios