* * *

Jul. 20th, 2017 07:21 pm
bamalip: (Default)
https://ua.censor.net.ua/photo_news/448219/boyiovyky_prodovjuyut_yurodstvuvaty_i_tantsyuvaty_na_kistkah_ubytyh_nymy_lyudeyi_kazanskyyi_pro_mityngrekviyem

Люди, які в 2014 році заявляли, що в "Боїнгу" були несвіжі трупи, і катастрофа була підлаштована, тепер вдають, що їм шкода загиблих пасажирів. У маскараді використовували дітей, яких одягли в ангелів і змусили покладати до пам'ятника дитячі іграшки. Рідкісне за своєю мерзенністю лицемірство", - написав блогер.


(примерно такое же у меня впечатление от лживых и противоречивых заявлений от бывшего работодателя о причинах прекращения того еще проекта).
bamalip: (NGE)
Когда переходишь с Джавы на Скалу, то сразу радуешься возможности записывать тип функции как A=>B и ее значение явной лямбдой. Прикольно же! Но все, наверное, знают такой психофизиологический эффект. Если несколько раз ел соленое, то хочется сладкого, несколько раз сладкое - хочется соленого, а потом и еще и кислого. А воду хочется пить всегда. Вот так же и с лямбдами. Я тут летом месяц попрограммировал на чистой лямбде (наш ОМ). И в данным момент мне приятно от лямбд, наоборот, освобождаться, на уровне синтаксиса. Не знаю, насколько это неожиданно, но от явных кванторов и стрелочек можно избавиться практически полностью, используя привычный синтаксис "аргументы функции в скобочках". Так сейчас и пишу. Причем это все будет почти тривиально рассахариваться из ЕХЕ в ОМ-style лямбду, а затем резаться на файлы-термы. А вот скобочки, в отличие от лямбд, воспринимаются нейтрально, не надоедают, они как вода. Я никогда не писал на старом Лиспе или новой Кложе, но сейчас скобочки идут вполне свободно. Впрочем я знаю, что в некоторых современных языках считается модным избавляться как раз от скобочек.

Кстати, скобочки это тоже довольно новое изобратение в нотации, в математических книгах начала века вместо них пользуются какими-то точечками для явного указания приоритетов операций, что выглядит совершенно нечитабельно, если глаз не привык. Так что даже такая привычная вещь, как скобочки, это тоже формально-лингвистическое достижение!

Desiderius Erasmus coined the term lunula to refer to the rounded parentheses, recalling the round shape of the moon.
bamalip: (NGE)
Наша "индукция" не живет сама по себе, для типа Bool или другого. Она представлена в виде трансляции формальных систем (язык + правила вывода и аксиомы): `CIC -t-> CoC`. Реализация аксиом CIC, таким образом, представляет собой только половину проблемы, другая половина - это описание трансляции всех языковых выражений. Первая половина, аксиомы, у нас реализована (да, для Bool), вторая, трансляция АСТ, витает в виде идеи (расслоения). Надо реализовать. Причем реализовать можно как (1) в общепринято-математическом виде "семантика, модель, тра-ля-ля", типа монографии Джекобса на 700 страниц, либо (2) записать тайпчеканную тотальную функцию на Агде или Леан. Второй вариант выйдет короче и будет надежнее, и непосредственно может быть портирован в Эрланг и/или ЕХЕ как работающий транслятор. Поэтому мне он видится более экономным по времени.

В упрощенном виде "для статьи" можно функцию трансляции ограничить до `(CoC+Bool) -a-> (CoC+records) -b-> CoC`. Минимальная часть `CoC -a0-> CoC` все равно нетривиальна. Она представляется в виде композиции `CoC --> (CategoryTheory) --> CoC`, где в промежутке у нас язык, состоящих из термов некоторой "синтаксической категории". Я могу оптимизировать этот участок, "посчитав" композицию в голове и не упоминая категорную часть явно, но разобраться полностью, как она устроена, я все равно должен. Отсюда игры с Hask, в котором реализована SystemF, как более простой вариант по сравнению с полными зав-типами. Всё связано!

Можно поставить вопрос о публикации отдельной статьи об аксиоме индукции для Bool (могу и для Nat, так солиднее), но я не уверен, что в ней есть смысл отдельно от всей трансляции `CIC -t-> CoC`. Можно написать, что это первая статья из серии статей, например.

Ситуация осложняется или улучшается тем, что я за лето в несколько шагов упрощал свои идеи по реализации кодировки. Я не знаю, хорошо это или плохо (может показаться, что мы меняем цели, и чего-то не достигаем), но если бы я просто "прыгал под деревом" в попытках сразу "сорвать банан", то я бы еще не сделал даже того, что уже сделано сейчас (да, Bool), потому что изначально реализация индукции виделась гораздо объемнее (включая портирование категорной библиотечки на ОМ). Сейчас я доделываю очередной раунд упрощения, будет неимоверно просто. Это хорошо, но при написании статьи надо выбирать, описывать ли все версии кодировки или какую-то одну (первую? последнюю? или опять серию статей?).

Дальше, для программистской части, нам нужен тайпчекер и транслятор `макросы->CoC`. Отдельный тайпчекер желателен, чтобы не попать в ситуацию, из которой уже который год пытается выбраться С++ со своими темплейтами, которые подставляются до тайпчека. Основное новшество по сравнению с ОМ тайпчекера здесь будет в сборе информации о записях/рекордах, которая потом пойдет в транслятор. Кроме того у нас осталась задача из ОМ: надо договориться, как ОМ режет дерево файловой системы на модули Эрланга и как это описывается в исходных файлах ЕХЕ (простейший вариант: 1 файл ЕХЕ -> 1 файл Эрланга).

Дальше необходимо выбрать систему описания типобезопасных макросов, тем более, что образцов для подражания у нас достаточно (это подразумевает расширение парсера и транслятора). Дальше портировать на язык макросов те функции трансляции верхнего языка, которые у нас будут уже к этому моменту реализованы на Леан или Агде. Так постепенно начнет проявляться ЕХЕ, если мы к тому времени будем еще живы и трудоспособны.
bamalip: (NGE)
Я пишу здесь постоянно, над чем работаю, но обычно это выглядит черезчур фрагментарно, поэтому сейчас я попытаюсь описать текущее положение вещей в нашем проекте в рамках одного поста.

____________________________________________________________________

Что уже есть?

Стек языков состоит из OM (низкоуровневый) и ЕХЕ (высокоуровневый).

OM - это реализация CoC, Calculus of Construction, с иерархией универсумов, с опциональной предикативностью. Фактически ОМ - это лямбда-исчисление с зависимыми типами. Сейчас мы транслируем его в Эрланг, но запланированы и другие бекэнды.

В репозитории на данный момент можно ознакомиться с таким исходным кодом:

OM, транслятор, на Эрланге
- парсер https://github.com/groupoid/om/blob/master/src/om_parse.erl
- тайпчекер https://github.com/groupoid/om/blob/master/src/om_type.erl
- стиратель https://github.com/groupoid/om/blob/master/src/om_erase.erl
- кодогенератор https://github.com/groupoid/om/blob/master/src/om_extract.erl
+ стиратель я сейчас дорабатываю (и в будущем мы планируем его улучшать и улучшать)

OM, работающие примеры библиотек, на ОМ
- "normal" https://github.com/groupoid/om/tree/master/priv/normal - это минимальная практическая библиотека, созданная по образцу библиотеки для языка Морте от Габриэля Гонзалеза, для индуктивных типов используется простейшая кодировка Черча (или Бёма-Берардуччи, если угодно), есть минимальная реализация монады IO.
- "new-setoids" https://github.com/groupoid/om/tree/master/priv/new-setoids - это реализация структуры "сетоид", на которой мы планировали делать кодировку, но потом переключились на следующий, немного урезанный вариант; в перспективе мы доделаем все варианты кодировок да рабочего состояния и проведем бенчмарки.
- "posets" https://github.com/groupoid/om/tree/master/priv/posets - реализация структуры "нерефлексивных частично-упорядоченных множеств", которые являются урезанным вариантом сетоидов и записываются в теории типов короче, чем сетоиды; здесь реализовано вручную несколько простейших типов данных, в частности тип Bool, вместе с зависимым элиминатором https://github.com/groupoid/om/tree/master/priv/posets/Data/Bool/
+ планируется написать все библиотеки на верхнем языке ЕХЕ (сейчас на ОМ писать вручную очень трудоемко) и держать в репозитории ОМ оттранслированный вариант для самостоятельного использования.
+ планируется дописать (уже начатые) библиотеки girard, hurkens, russell, в которых будут реализованы известные логические парадоксы, показывающие неконсистентность теории типов с импредикативной иерархией универсумов.

ЕХЕ - это реализация CIC, Calculus of Inductive Constructions, с минималистичным, но юзабельным синтаксисом (синтаксис на данный момент еще не совсем зафиксирован, subject to change). ЕХЕ транслируется в ОМ.

По техническим причинам нам удобно разделить ЕХЕ на
- ядро имеет типы `record`, которые используются как модули или как структуры, они прозрачно транслируются в ОМ как "контексты" (т.е. просто последовательности типов и термов);
- над ним слой метапрограммирования, который позволяет записывать и исполнять макросы, транслирующие верхний язык в ядро;
- на макросах мы пишем библиотечку для собственно кодировки (будут разные варианты, которые можно будет переключать при компиляции);
- верхний "прикладной" язык, собственно само ЕХЕ, в котором при помощи макросов из предыдущего слоя можно использовать индуктивные и коиндуктивные типы, data, codata, (в перспективе и индуктивно-индуктивные, mutual).

Скорее всего синтаксис ядра будет просто подъязыком верхнего языка.

В репозитории на данный момент можно ознакомиться с таким исходным кодом:

EXE, транслятор, на Эрланге
- парсер ядра https://github.com/groupoid/exe/blob/master/src/macro_parser.yrl
+ в разработке - синтаксический механизм нотаций, они же миксфиксные операторы, они же просто сахар

ЕХЕ, примеры кода, на ЕХЕ
- пример кодировки для типа Bool, https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.Bool.macro (этот исходный код должен транслироваться в ту библиотечку, которая сейчас лежит в ОМ -> https://github.com/groupoid/om/tree/master/priv/posets/Data/Bool/
- см. в том же каталоге кодировки некоторых других типов, например свободной монады https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.FreeMonad.macro
+ макросы, которые будут генерировать все это для любых типов

____________________________________________________________________

Как оно работает?

Полностью идею кодировки мы начали последовательно излагать вот здесь: https://github.com/groupoid/om/blob/master/doc/tale.tex однако переключились на непосредственно написание компилятора. Документация это хорошо и важно, но приоритетнее - рабочий код. Надеемся в скором времени дописать все подробно. А коротко я сейчас изложу, у нас уже появилось несколько вариантов.

Прежде всего - то, что реализовано, работает в CoC с добавлением непредикативной иерархии. Это немного печально (ввиду проблем с консистентностью), но мы надеемся сделать ограниченный вариант, который будет умещаться в исходный CoC с одной *, консистентность которого доказана.

На чем основана исходная идея.

Есть на свете такая теория категорий. Если читатель о ней знает, это хорошо, а если нет, то я отсылаю его к учебникам, в одном посте это описать трудно. В мире теории категорий имеются некоторые способы характеризации объектов, называемые универсальным свойством, и некоторые теоремы о них. В частности, есть способы вычисления сопряженных функторов, основанный на теореме Фрейда о сопряженных функторах (их есть несколько). Эта информация общеизвестна в среде алгебраистов, например, в популярный учебник Ленга входит описание процедуры конструирования подобным приемом алгебраического замыкания поля. Нам сейчас будет достаточно такого факта, что инициальный объект совпадает (с точностью до изоморфизма) с пределом тождественного функтора.

То была алгебра, а вот computer science. В мире теории типов известно, что аксиомы, описывающие индуктивные типы данных (их конструкторы и элиминаторы), выглядят не очень просто (как бы ad hoc), если смотреть на них невооруженным взглядом, но на самом деле они просто означают инициальность объекта, заданного типом и конструкторами (F-algebra), в категории подобных объектов (теория категорий, как всегда, все упрощает). Это значит, что мы можем применить для построения индуктивных типов теорему из предыдущего абзаца.

Тут возникает интересный момент. В теории типов есть как бы общеизвестная вера в то, что рекурсор (non-dependent eliminator) представляет собой более слабое свойство, чем индукция (dependent eliminator). В то же время из теории категорий мы знаем, что универсальное свойство определяет объект однозначно, а в случае инициального объекта в категории алгебр инициальность задается, фактически, рекурсором. Это значит, что все свойства нашей алгебры вытекают из ее инициальности, в частности, из рекурсора можно получить индукцию. Тут есть тонкий момент - все категорные конструкции формулируются в присутствии предзаданного хорошо ведущего себя равенства на морфизмах, в то время как в теории типов равенство является внутренней конструкцией, у которой может быть много сложных свойств, зависящих от дополнительных аксиом. Упрощая, мы можем сказать так: без равенства мы можем получить только рекурсор из индукции; в присутствии хорошего равенства мы можем, наоборот, получить индукцию из рекурсора.

Механизм получения индукции за счет равенства основывается на представлении зависимых типов в рамках теории категорий через расслоения. Зависимый тип (D: B -> Type) при этом задается как морфизм (p: Sigma B P -> B), который просто проектирует зависимую пару на первое поле. В топологии (см. HoTT) такой подход называют "расслоениями". В обратную сторону, если задан произвольный морфизм (p: E -> B), который мы понимаем как расслоение с проекцией p, мы можем получить из него зависимый тип (D: B -> Type), вычисляя в каждой точке (b: B) ее прообраз при проекции p (для чего нам потребуется использовать некоторое равенство на элементах B). В теории типов помимо упомянутой здесь зависимой суммы Sigma используют еще Pi, зависимое произведение. При нашем кодировании зависимых типов расслоениями элементам зависимого поизведения соотвествуют морфизмы-сечения для проекции p, т.е. такие (s: B -> E), которые после умножения их на p дают единицу. Пример реализации этой конструкции можно увидеть тут:
ЕХЕ - https://github.com/groupoid/exe/blob/master/prelude/macro.new/Mini.macro#L71
ОМ - https://github.com/groupoid/om/blob/master/priv/posets/sec2all

На вход индукции мы передаем предикат - зависимый тип, закодированный в виде проекции (p: E -> B). Индукция требует дополнительную информацию о предикате, тип которой определяется типами конструкторов исследуемого индуктивного типа; она в точности соответствует утверждению о том, что на E задана структура F-алгебры. Теперь достаточно применить рекурсор к E, получив отображение (I -> E) из инициального объекта, которое оказывается сечением расслоения, а значит, задает ту самую зависимую функцию, которая окажется значением "доказанной" таким способом аксиомы индукции. Реализация:
ЕХЕ - https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.Bool.macro#L128
ОМ - https://github.com/groupoid/om/blob/master/priv/posets/Data/Bool/induc

Итак, мы кодируем типы исходного лямбда-исчисления - объектами выбранной категории, зависимые типы - расслоениями, зависимые функции - сечениями, индуктивные типы - пределами тождественного функтора на категории алгебр, зависимый элиминатор - конструкцией, описанной в предыдущем абзаце.

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

Собственно, сейчас в коде реализована последняя конструкция. Необходимое для трансляции отображение исходных типов на объекты выбранной категории еще не воплощено в коде, и будет реализовано на языке макросов. Конечно, все это немного громоздко.

____________________________________________________________________

Что еще запланировано?

Буквально вчера я закоммитил вариант упрощенной кодировки, который не опирается на слой категорных абстраций, но в некотором смысле делает то же самое. Пока не ясно, удастся ли довести его до полной трансляции CIC->CoC, но если удастся, то это будет неплохая оптимизация. https://github.com/groupoid/exe/tree/master/prelude/smart-simpleton

Кроме того, есть мысли по поводу кодировки в предикативной иерархии универсумов, но потребуется время, чтобы довести их до рабочего варианта (или опровергнуть идею). Ожидается, что она будет более сложной и будет использовать категорные доктрины (идемпотентные 2-монады).

____________________________________________________________________


Вопросы и комменты приветствуются.
bamalip: (NGE)
По итогам недели у нас анонс. Грядет еще один вариант кодировки, более приспособленный для ТТ, чем для ТК. Я обратил внимание, что у нас типы выглядят как зависимая пара (el : El) (ok : Ok el) для некоторых типов (El : *) (Ok : El -> *). Второе поле здесь (как предикат) вырезает из первой некоторую часть, на которой у нас выполняются необходимые для структуры аксиомы. Проблема была в том, что предикат записывался так, как нам диктовала ТК, и чтобы вытащить из него то, что нужно для ТТ, нужно было попотеть и выписать километры категорной библиотечки. Сейчас мне пришло в голову (и кое-что получилось сделать на бумаге), что в (Ok) мы можем сразу всунуть то, что нам нужно для ТТ (элиминатор), а получится объект, который изоморфен тому, что был раньше, и он будет удовлетворять всем требуемым свойствам индуктивного типа - хоть теоркатегорным, хоть теортиповым. Пока что в работе два варианта: в одном элиминатор принимает предикат (P : El -> *), во втором, более сложном, (P : ∀ (el : El) -> ∀ (ok : Ok : el) -> *). Сейчас нужно проверить, что такие типы образуют модель CoC. Кроме того, я еще не умею получать конструкторы общего вида.

Безусловно, нужно выписать получающиеся модели в том виде, как это делает, например, Джекобс (на 700 страниц!) и сверить с теми результатами о кодировках, на которые ссылается, например, Пенг-Фу. Хотя на самом дела лучшим сертификатом корректности окажется работающий компилятор.
bamalip: (NGE)
https://gist.github.com/zraffer/ea667528479de6cdbadbd52ad0f9bbef/c2d28323614712a1525874feeb46fa4d90414e8d

нормальная форма занимает 581453 байт

"слово, которое трудно сказать"
bamalip: (NGE)
я тут за последние недели наконец полюбил теорию типов и перестал беспокоиться.

раньше у меня была иллюзия, что ТТ - это просто "теория одной категории", а вот ТК безусловно шире охватывает и глубже проникает в реальность.
и даже HoTT как-то окончательно не убеждала - подумаешь, еще одна категория группоидов.

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

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

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

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

Если тут есть типовики, хватайте идею, обобщайте HoTT, индуцируйте лучше нас!
bamalip: (NGE)
LaTeX в атоме прекрасно работает почти "из коробки" (достаточно установить пару пакетов из репозитория)

Вот я нарисовал оглавление длинного пути, где мы, следуя строгой математической традиции, старательно вводим все определения перед использованием:

latex-in-atom.png

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

PS: текст планируется не слишком математический, примерно для уровня программистов (см. предыдущий пост). Просто я начал писать сразу про тип List и наткнулся на то, что кучу терминов надо так или иначе вводить и определять, а если делать это настолько минималистично, как это сделано сейчас на нашем сайте (там для тех, кто в курсе!:)), то такое объяснение вызовет еще больше вопросов. А статью впоследствии напишем компутер-сайенсовую отдельно, с явным указанием правил вывода и всего такого, согласно жанру.

* * *

May. 3rd, 2016 06:18 pm
bamalip: (NGE)
сущность котегорий и кодеровок немедля будет описана детективным языком для вящего понимания рачительных читателей!

ждите в следующем номере: умопомрачительная история о пределе и конструкторах.

bamalip: (NGE)
Создаем пределы.

Есть такая типичная ситуация -- мы строим категорию на основе другой, базовой категории. Классический случай -- объекты с дополнительной структурой. Если у нас категория алгебр, то стирающий функтор создает пределы [1]. С коалгебрами дуально - стирающий создает копределы. Это означает, что носитель (ко)предела совпадает с (ко)пределом носителей, а структуру (ко)алгебры можно вытащить из универсальных свойств (ко)предела.

Нас сейчас будет интересовать частный случай - алгебры, структура которых имеет тот же тип, что и конструкторы заданного индуктивного типа. Как мы уже знаем, инициальная алгебра в такой категории - это сам индуктивный тип, причем его можно вычислить как предел тождественного функтора в этой категории. Ее носитель - это предел стирающего функтора. Как нам из общих соображений (понятия created limit) построить конкретные конструкторы, т.е. вычислить предел в категории (ко)алгебр?

Поскольку мы ориентируемся на создание макроса, который будет разбирать конструкцию индуктивного типа на некоторые базовые шаги, мы опишем, как эти шаги влияют на формулу для предела.

Рассмотрим самый общий случай. Категорию диалгебр Dialg P над категорией сетоидов Set будем задавать профунктором P : Set° x Set -> Set. Стирающий функтор обозначим U : Dialg P -> Set. Эта категория обладает универсальным свойством: задание функтора G : D -> Dialg P эквивалентно заданию функтора G'=UG : D -> Set одновременно с концом End P(G'(-), G'(-)). Пределы в Set мы строить умеем, поэтому можно сразу записать U(Lim G) = Lim G'. Нам не хватает структуры диалгебры, т.е. значения P(Lim G', Lim G'). Фактически, пределы в Dialg P задает функция qP,D,G : End P(G'(-), G'(-)) -> P(Lim G', Lim G'). Для получения нужных нам конструкторов достаточно вызвать эту функцию на стирающем функторе U.

Как строить q для P, описывающих алгебры над полиномиальными функторами?

Пусть P0 (A, B) = B, что соответствует простейшему конструктору без аргументов, например Zero : Nat.
Тогда q0(e) : Lim G'; q0(e) = e. Эта запись правомочна, поскольку конец (End), зависящий только от одного аргумента, совпадает с пределом.

Пусть известна q для профунктора P. Проведем вычисления для более сложного профунктора P1 (A, B) = X -> P (A, B). Это означает добавление к конструктору одного аргумента фиксированного типа.
Положим q1(e) : X -> P(Lim G', Lim G'); q1(e)(x)(A) = e(A)(x).

Пусть известна q для профунктора P. Проведем вычисления для более сложного профунктора P2 (A, B) = A -> P (A, B). Это означает добавление к конструктору одного рекурсивного аргумента.
Положим q2(e) : Lim G' -> P(Lim G', Lim G'); q2(e)(l)(A) = e(A)(l(A)).

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

[1] https://ncatlab.org/nlab/show/created+limit
bamalip: (NGE)
А в предикативном случае, если не использовать пополнения (сложно!), то та же Черчевская техника дает такую диаграмму вместо индукции:

I_{n} : *{n}, I_{n+1} : *{n+1} - экземпляры нашей инициальной алгебры в соответствующих универсумах

P : I_{n} -> *{n} - зависимый тип (плюс исходные данные индукции)
π : ΣP -> I_{n} - представление того же зав.типа в виде расслоения над инициальной алгеброй (удобно для категорных конструкций)
i_{ΣP} : I_{n+1} -> ΣP - катаморфизм, который строится рекурсором
i_{I_{n}} : I_{n+1} -> I_{n} - катаморфизм, тоже строится рекурсором, определяет отличие (и связь) инкарнаций нашего индуктивного типа в разных универсумах

Вся хитрость в том, что последний морфизм не обязательно равен единице.
Если он будет равен единице, то у нас будет работать та же схема, что и в непредикативном случае, и коммутативность треугольника из последних трех морфизмов даст желанную аксиому индукции.
Если он не равен единице, а определяет некий подобъект, то его можно интерпретировать так, что ослабленная индукция для зав.типа P над I_{n} строит функцию не на всем I_{n}, а на его подтипе I_{n+1}.
А если нужна функция на I_{n}, то надо брать изначально P над I_{n-1}.
Как-то так.
"Индукция со сдвигом".

Подчеркиваю, в этом посте имеются в виду объекты в нашей почти-черчевкой кодировке. Для избавления от сдвига я и пытался сделать что-то с пополнениями.
bamalip: (NGE)
другой вывод, более конструктивный, который можно обнаружить, рассмотрев нашу конструкцию в контексте n-категорий: кодирование инициальных объектов пределами можно не только обобщить на высшие размерности, но и упростить в размерности нуль, при этом получится исходная кодировка Черча. Это то, чего долго хотелось - единой стройной картины без мистики, объясняющей, почему стирание (erasure) предела дает нам Черча. Оказывается, стирание - это декатегорификация, при которой мы от (1,1)-категорий и конструкций на них переходим к (0,1)-категориям и конструциям на них. 2-морфизмы (равенства сетоидов) при этом испаряются. От обычного предела на сетоидах после такой операции остается обычное теор-типовое зависимое произведение, которое мы и видим в Черче-Берардуччи. Ура!

Другая сторона медали - повышение размерности - состоит в том, что мы можем строить всякие 2-пределы или 2-копределы на 1-категориях при помощи несложного (в непредикативном случае несложного...) обобщения кодировки. Это дает возможность, в том числе, вычислять всякие "индуктивно определенные категории", вроде категории последовательностей объектов на исходной категории. Эта часть нашего механизма работает.
bamalip: (NGE)
(уроки из опыта прошлой недели)

Есть классический подход (1), принятый в математике, - сначала определить произведения множеств (сетоидов) и произведения категорий, а потом бинарные операции (умножение морфизмов) определять, исходя из произведения: mul : A*A->A . Такой подход приводит к достаточно прозрачной нотации для бесточечной записи сложных операций, т.е. термов нашего исчисления. Например, ассоциативность можно выразить как mul.(1*mul)=mul.(mul*1).

Однако, бывают ситуации, когда мы начинаем с функций и функторов, а произведения (тип-пара, сигма, рекорды и т.д.) кодируются через него. Как тут быть?

Можно разогнаться на принятой в теории типов каррированной записи (2), и пытаться выражать все через нее: Mul : A->A->A. Теоретически этот подход в равной степени универсален. Однако он приводит к достаточно непрозрачной записи в бесточечном варианте. Например, ассоциативность теперь будет (Mul .) . Mul = (. Mul) . (.) . Mul -- если вам здесь все интуитивно понятно, то мне не совсем :) а когда мы переходим ко всяким маклейновским пентагонам, которые должны выражаться из этой ассоциативности, то непрозрачность достигает апогея - нужно ведь не только тип выразить, но еще и собрать из ассоциаторов сложную операцию. Выходом может быть отказ от бесточечной записи... одним словом, пришлось похерить, то, что я пару дней писал, из-за нечитабельности.

Но идеальное решение проще! Если мы разрешаем макросы, которые преобразовывают операции, заданные на произведении, в операции каррированного типа (эти макросы еще надо написать, да, но это проблема техники), то мы можем писать в удобном математическом синтаксисе (1), при этом не требуя выразимости произведений, кроме использования их в каррированном варианте (2). Причем, похоже, нам не нужно писать отдельные макросы для множеств (сетоидов) или категорий, достаточно реализовать их для голых типов, а привычные выражения для произведения дадут нам способ перевода (1)=>(2).

Итого, когда я совершу второй подход к снаряду с 2-категориями, то буду делать классически, через произведения, и все будет хорошо.
bamalip: (NGE)
а задумывались ли вы, дорогие читатели, что привычные вещи, как пустой тип (инициальный объект) и натурально-числовой объект - имеют свою копию в каждом универсуме, причем эти копии могут не совпадать? и ничего приятного в такой фантастике нет - мы вычисляем пустой объект, а он не совсем пустой, потому что есть другой, еще более пустой (?!). и набор натуральных чисел может оказаться разным, что может вызвать проблемы с попыткой проитерировать функцию.

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

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

как сказано:

Есть одно слово,
Которое сложно сказать.
Но скажи его раз, и железная клетка пуста
http://www.ytime.com.ua/ru/55/1739/31/

БГ - Ещё один раз (15) Рига live



Для этого нам понадобятся:

- понятие категории
- категории функторов
- опционально - эквивалентность и сопряжения функторов
- опционально - предел функтора
- категория сетоидов, включая сетоиды отображений сетоидов
- категория зависимых сетоидов DepSetoid
- слайс-категория сетоидов над сетоидом OverSetoid
- функтор между этими категориями, вычисляющий Сигма-тип (строится как инициальная алгебра, которая строится как предел)
- это функтор задает эквивалентность двух предыдущих категорий
- два сопряжения, описывающих Пи-типы (кванторы), для DepSetoid и OverSetoid
- утверждение о коммутативности треугольника, образованного эквивалентностью (Сигма-тип) и сопряжениями для Пи-типов (это основной факт семантики зависимых типов в LCCC, и он нам нужен)

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

(и меньше, вроде, не получается).

сейчас делаю несколько строчек из этого на языке макросов (который нам нужен ввиду трудности написания непосредственно на голой лямбде)
bamalip: (NGE)
Вчера пытался писать минимально сложный пример на нашем "лямбда-ассемблере". Это действительно ассемблер! Для категорной эквивалентности, записанной в две строчки на бумажке, требуется несколько десятков файлов, содержащих по несколько десятков переменных. Страшно не это, не количество. Через полдня писанины в таком режиме возникает эффект "замыливания" глаз: все имена файлов из небольшого набора, имена каталогов из того же набора, имена переменных и типов - комбинации кусочков из того же набора (а другим именам неоткуда взяться, я просто собираю сетоиды из сетоидов!). В результате ты находишься в зеркальном лабиринте, где со всех сторон видишь почти одинаковые отражения исходных двух строчек, и мозг перестает осмысленно это единообразие воспринимать. Можно сказать об этом коротко - "комбинаторный взрыв" - но обычно под этим термином понимают только количественную сложность, а тут еще сложность различения однообразности.

Вывод - только кодогенерация спасет гигантов мысли и отцов украинской демократии.
bamalip: (NGE)
прикидывал сегодня на листочке, что у нас уже есть в высокоуровневом виде [1], что надо перенести в низкоуровневый и в какой последовательности [2] (с одной стороны), и (с другой) что нам пока предстоит написать и там и там для предикативного случая.

[1] https://github.com/groupoid/exe/blob/master/prelude/lean/Initial.lean
[2] https://github.com/groupoid/om/tree/master/priv/new-setoids

Во-первых, оказывается, что оттранслировать напрямую определение категории в таком виде нельзя "одно на все случаи", не только ввиду нереализованности universe polymorphism (который скоро будет), а более потому, что понятие "тип" в высокоуровневом представлении требуется транслировать в понятие "контекст", под которым в ТТ понимается то, что можно записать слева от штопора - последовательность переменных, типы которых могут быть взаимно зависимы. Главным примером является "сетоид", который задается таким контекстом. Мы сейчас называем это простой кодировкой типа record каррированными аргументами, но по-научному это надо называть "контекст" :) Так вот, определение категории необходимо инстанциировать не только для разных универсумов вида *n, но и для различных последовательностей универсумов, определяющих вид контекста (в данном случае, задающих сетоид). Такая форма специализации определения слишком сложна, и ее, скорее всего, нет смысла засовывать в низкоуровневый язык, самое место для нее - в промежуточном языке макросов. С другой стороны, в высокоуровневом ЕХЕ необходимости в ней нет, потому что механизм сетоидов нам обеспечит кодирование произвольных индуктивных типов, и нужен будет единственный вид контекстов, - те, что определяют сетоид.

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

UPD я чителей замучал уже этими брадобреями, наверное. :) но смысл такой, что непротиворечивость (невырожденность и т.п.) теории (в данном случае, СоС) доказывается в более сложной теории, и поэтому ничего с практической точки зрения не дает - эта более сложная теория может сама быть противоречивой и тогда это доказательство ничего не значит. каждое подозрение на противоречие надо внимательно рассматривать и доводить до конца.
bamalip: (NGE)
цитата [livejournal.com profile] nponeccop:

Provable это не маркетологично. Правильные слова - формальная верификация.

https://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7:_Formally_Verified_Design_and_Tested

EAL конечно за уши притянут (формальная верификация это вишенка на торте EAL6), и EAL больше о секьюрити чем о безбажности, но тем не менее.

Хипстеры об этом просто не слышали, надо материалов насобирать от разработчиков life critical systems. Для чего надо их найти и заставить нарисовать слайды с операционными системами без динамической аллокации и шедулера.

Это пока стоит очень дорого и используется производителями авионики, компьютеров, управляющих тормозами и эйрбегами и т.п. - в общем всём без чего немыслима жизнь современного человека, но что невидимо.

Гуглить по словам formally verified rtos и formal methods in life critical

Мы же хотим это удешевить и дать хипсторам. Пусть в вашем коде будет столько багов, сколько в микроконтроллере тормозов фольксваген гольфа и форда фокуса конечно.

Profile

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

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 1920212223
24252627282930

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 20th, 2017 02:01 am
Powered by Dreamwidth Studios