bamalip: (NGE)
Простая вещь, но неоконченная, поэтому трудно писать, вот основные штрихи. Мы, собсвенно, ее пока доводить до конца не собираемся, для компилятора она не нужна, но как боковая ветка нашей дороги, альтернативное изложение типовиков, которое попало мне в голову, когда я пробовал взглянуть на все это со стороны...

Обдумывал последние несколько дней такой подход. С одной стороны, я могу представить снизу-вверх наш подход к компилятору как (1) последовательное усложнение той категории, на которой мы фокусируемся на данном уровне, - т.е. как усложняется реализация типов. Мы берем исходную категорию СоС, потом переходим к контекстам (записям-рекордам, туплам, зависимым суммам), потом к сетоидам, и уж там-то нам есть где развернуться с нашей категористикой, применяя теорему о сопряженном функторе (2). Это как две последовательные стрелки. Все обсуждение при этом происходит, как видим, в идеологии ТК.

Но можно изобразить другой путь (это будут другие стрелки, образующие с первым путем как бы коммутативный квадрат).
Сначала мы усложним исходную теорию типов таким образом, чтобы зависимые функции *стали пределами*. Аксиоматически *стали пределами*, в рамках теории типов. Старые зав.функции - это как бы стертый вариант новых, истинных. Далее, мы же помним, что кодировка Ч-Б-Б - это стертый вариант истинной, так? Так вот, просто записав в нашей новой теории типов старую ЧББ, мы получим истинную. Так что проблема тут не столько в кодировке, а в том, что простым аксиомам СоС не хватает свойства пределов быть пределами. Довольно просто и элегантно. (Единственно, что мне не нравится в отказе от ТК, - это то, что ТК дает некое понимание, откуда берется кодировка - что есть алгебры, инициальные объекты и сопряженные функторы, и в их терминах можно описать кодировку как пошаговое решение задачи на знакомом ландшафте, а не озарение или фокус, как это выглядит в ТТ).

Пытаясь продумать усиленную аксиоматику, я пришел к таким выводам: в ней должна быть доказуема параметричность, известная как бесплатные теоремы. Собственно, эти теоремы устанавливают, что зав.функции являются концами. Фактически, и наша кодировка, обрабатываемая метапрограммированием (макросы), и параметричность, являющаяся метатеоремой, являются механизмами одного порядка. Видно два пути - или (1) всунуть в аксиомы все конструкции из бесплатных теорем (это громоздко технически, хотя идеологически не вносит новых понятий); или (2) попытаться скопировать часть ТК, ответственную за пределы (тем же способом, как группоиды охватываются в HoTT). Первый подход сложен, хотя дает результат в интересном виде: если в предыдущих постах я описывал конструкторы неполностью (опустил поле предиката в элементе предела), то сейчас эти же термы будут полными значениями, поскольку недостающее поле будет генерироваться теоремами/аксиомами. Второй подход более любопытен: мне кажется его можно реализовать довольно просто. Достаточно считать, что функции у нас - вроде как функторы, могут быть контравариантными (точне, ввести операцию перехода от типа к его дуальному); в частности, теперь X->Y будет контравариантным по первому аргументу; тогда тот индуктивный тип Id, который в HoTT дает равенство, перестанет быть симметричным и будет извлекать из типов их "внутренние морфизмы" вместо равенств. Дальше нужно заметить, что функции, помимо действия на элементах, должны действовать на морфизмах. Потом проверить, что это действие имеет тот же тип, что и утверждение, что тип зав.функций является пределом. И никаких теорем вводить не нужно!

Если тут есть типовики, хватайте идею, обобщайте HoTT, индуцируйте лучше нас!

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23 2425 26 27 2829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 29th, 2017 11:51 am
Powered by Dreamwidth Studios