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

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

Еще хотелось бы перенести обратно на категории известные доказательства нормализуемости/cut-elimination. Для мета-разбирательств с тотальностью/консистентностью, как обычно. Не уверен, что в этом присутствует большой смысл, но имеется такой жанр и мода на него тоже не утихает. Интересно, в частности, насколько безопасны сильные формы universe polymorphism-а для случая очень предикативных иерархий.
bamalip: (NGE)
плейлисты с выступлениями: https://www.youtube.com/user/DrBartosz/playlists

сейчас началась запись серии видео по мотивам серии блогопостов, посвященных, как вы уже догадались, теории категорий.
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)
цитата:

category theory is not a foundation for mathematics. Category theory is a language that can be used to describe lots of kinds of mathematics, including some foundations of mathematics


Достаточно адекватный аналог этого заявления на айтишном языке:
"L4 это не микроядро, это гипервизор."
(и в принципе это зависит от use case)

* * *

Aug. 8th, 2016 08:31 pm
bamalip: (NGE)
Category Theory for the Working Hacker by Philip "Free Theorem" Wadler

Достаточно ли популярно он там излагает, подходяще для рабочих хакеров?
bamalip: (NGE)
Зачастую попытки втиснуть в 1-категорию информацию о разных уровнях приводят к запутанной структуре. Опишем структуру на 2-категории, идеальным образом задающую язык с типами SystemF и тайпклассами. В следующих версиях попытаемся это описание улучшить (прежде всего, ленивость). Все 2-категории с такой структурой можно считать моделями нашей теории типов (все вместе они образуют большую 3-категорию), а инициальную из них можно называть синтаксической категорией - все элементы последней будут описываться деревьями-словами соответствующего языка, на ней будут выполняться обобщенные бесплатные теоремы, и даже рекурсор у нее будет, как в лучших домах Лондона, Парижа и Филадельфии.

Чтобы понимать прагматику, мы скажем, что объекты нашей произвольной 2-категории описывают тайпклассы (каждый с параметром из некоторого кайнда). Выделен один фиксированный объект Type, он же *, означающий базовый кайнд всех типов (с пустым тайпклассом). Наша 2-категория должна иметь конечные произведения и быть декартово замкнутой, что сразу порождает остальные кайнды. Type должен иметь конечные пределы, копределы, быть декартово замкнутым (это простые алгебраические типы). Задана операция перехода к дуальному объекты (прагматика такая, что каждый тайпкласс означает категорию и мы хотим менять стрелочки) (TODO - вместо этого можно рассматривать отдельно профункторы).

Для порождения тайпклассов мы возьмем операцию взятия категории диалгебр на профункторе, вернее, интернализованную версию (TODO - упростить/обобщить до "взвешенных 2-пределов"). В принципе, можно считать предыдущую операцию опциональной, рассматривая тайпклассы как сахар; это соответствует разделению языка на верхний (с тайпклассами) и нижний (без них).

Кванторы на типах. Это сопряженные 1-морфизмы к константному A->(A^B). (TODO - проверить выразимость всех расширений Кана и поменять эту аксиому на них). Фактически это пределы (т.е. мы реализуем часть бесплатных аксиом).

Минимальная и максимальная неподвижные точки функтора. Вычисляются через кванторы.

Основной эффект ленивости: изоморфность минимальной и максимальной неподвижных точек. (TODO: усложнить утверждение, добавив явную ленивость, и ограничив аксиому только ленивыми (lifted) типами).

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

Сейчас произошел вброс на высшем уровне http://math.andrej.com/2016/08/06/hask-is-not-a-category/

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

Вобщем я решил стартовать с самого простого варианта, пока даже без ленивости. Так что это будет не Хаскелль, а, допустим, фрагмент Идриса без зав-типов, с System F. Не будет кучи "расширений", все изображено компактно. В следующей версии добавим опциональную ленивость. Будет undefined. Ужасного seq не будет, поскольку это костыль для достижения неленивости в изначально ленивом мире. В неленивом мире seq не нужен. Тьюринг-полноты пока не будет, но мы над этим работаем.

И еще. В посте по ссылке обыгрывается глагол pretend. Привычная Hask pretends быть категорией, но не определена достаточно хорошо. Та категория, которую я сейчас опишу, pretends на соответствие Хаскеллю, но слишком хороша для него. И даже наоборот, я бы сказал, реальный Хаскелль - это инженерное решение, стремящееся в идеале соответствовать ей.

UPD. 2-Hask, v0.1
bamalip: (NGE)
Мысли по поводу нового варианта получения инициальной алгебры, то что сейчас в процессе.

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

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

Следите на новостями!
bamalip: (NGE)
вот нашел краткое введение в категории, где акцент сделан именно там где надо нам - на способ получения неподвижных точек функтора
http://www.cs.indiana.edu/cmcs/categories.pdf

qualia

Aug. 2nd, 2016 05:07 pm
bamalip: (NGE)
через гугл+ рекомендуют:

Using category theory to assess the relationship between consciousness and integrated information theory
http://www.sciencedirect.com/science/article/pii/S0168010215002989
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
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)
Дж.Баез долго молчал (=не делал прямых заявлений о метавопросе), и тут прорвало!
Foundations of Mathematics

Если коротко, то в списке рассылки по основаниям "фильтруют" темы, и создается впечатление, будто ТМ до сих пор занимает какие-то позиции. Развернулось обсуждение и как бы срач на академическом уровне )))

Что примечательно - приводится цитата Ю.Манина (учебник которого по линейной алгебре я уже успел тут рекомендовать для тренировки мозгов как самый хардкорный), где тот в полуформальном контексте использует термин "аттракторы" :)
bamalip: (NGE)
категорные психологи нашли непонятный доклад непонятного ученого - вроде про ИИ, но якобы и про теорию типов, и даже до теории категорий речь доходит.
http://vk.com/wall-65754727_18

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

Category Theory Seminar Notes
Category Theory Course Notes

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
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:41 pm
Powered by Dreamwidth Studios