bamalip: (Default)
Известно, что модели теорий зависимых типов это LCCC (с вариациями в формулировках, основанных на расслоенных категориях). Вопрос в том, как правильно определять это "LCCC". Потому как в монографиях Курьена или Джеккобса это все долго и нудно. Во-первых хочется, чтобы работало с линейными типами (программирование квантовых нововведений и все такое; ну и обычные языки этой темой начали интересоваться), т.е. недекартово обобщение, во-вторых, чтобы бодро и современно, а не ещё одна монография на тыщу страниц с диаграммным поиском. А то Гротендик, конечно, молодец со своей "йогой шести операций", но там опять же нудно и долго, потому что через 1-категории, потому что в то время, когда это писалось, ничего адекватнее не было. Но сейчас замечательно. Получается сформулировать удивительно просто - это высшая кубическая замкнутая категория, тонкости только в том, в каком виде высшая и в каком смысле замкнутая, чтобы все остальное вылезало отсюда автоматом.

Сермяжная польза такая, что получается, можно получить отсюда трансляции между языками ТК и вариантов ТТ, представляя синтаксис ТТ как инициальную высшую категорию с подходящей структурой. Ну, это общие слова про модную тему, сейчас много кто здесь ведет раскопки. В качестве немедленных результатов - категория для классической SystemF, и как результат решение скандала с Хаскеллем. Немедленно получается какой-то относительно простой вариант равенства. Можно удобно в таком сеттинге формулировать то, чем я занимался в прошлом году (хотя кому это нужно). Мне интереснее, что можно продвигаться в плане юзабельного языка на чистых топосах, с одной стороны, и в плане языковых механизмов для "ad-hoc полиморфизма" без этого ужасного резолвинга инстансов тайп-классов.

Еще хотелось бы перенести обратно на категории известные доказательства нормализуемости/cut-elimination. Для мета-разбирательств с тотальностью/консистентностью, как обычно. Не уверен, что в этом присутствует большой смысл, но имеется такой жанр и мода на него тоже не утихает. Интересно, в частности, насколько безопасны сильные формы universe polymorphism-а для случая очень предикативных иерархий.
bamalip: (NGE)
Мне на выходных ставили вопрос о сигма-типах (но тогда происходили слишком бурные события):
http://zeit-raffer.livejournal.com/169637.html?thread=733605#t733605

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

Пусть заданы (B : Type) (F : B -> Type)

Тип сигмы кодируется как (Sigma := Pack record (b : B)(f : F b)), где под record понимается контекст (как и везде в файлах с расширением macro).

С первой проекцией проблем не возникает (pr1 : Sigma B F -> B).

Для кодирования второй проекции нам нужно выписать ее тип. Это (s : Sigma B F) -> F (pr1 s)
Она должна кодироваться сечением расслоения Pack record (b : B) (f1,f2 : F b) -> Pack record (b : B) (f : F b). Его можно задать как Pack.map (\{b,f} -> {b,f,f}).

Выше написано то, что происходит в сетоидно-категорной кодировке. Что там будет с сигмами в "Симплетоне", я еще не знаю.

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

Можно определить функтор, выделяющий в каждом объекте A минимальный подобъект, т.е. инициальный объект в C/A. Этот функтор оказывается комонадой. И вместо того, чтобы строить инициальную алгебру сразу, можно взять минимальную подалгебру простой черчевской.

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

Следите на новостями!
bamalip: (NGE)
У кого круче тайп-фу - у Кметта или у Киселева?

цитата:

- А вы отгадайте… Если кит и вдруг на слона налезет? Кто кого сборет? Отгадайте.
- Не знаю, — говорит солдат. — Ну, скажи, кто?
- И я не знаю, — говорит Ося. — И папа не знает, и дядя. Никто.

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


[Poll #2051191]
bamalip: (NGE)
я тут за последние недели наконец полюбил теорию типов и перестал беспокоиться.

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

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

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

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

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

Если тут есть типовики, хватайте идею, обобщайте HoTT, индуцируйте лучше нас!
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

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:04 am
Powered by Dreamwidth Studios