Настроение:	geeky
Музыка:	Sixth June -- Back for a Day
Entry tags:	category theory, cps, haskell, type theory

All Concepts are Kan Extensions, Part 0
Решил изучить continuation-passing style, call/cc, codensity monad, вот это все. Прочитал статью, в которой в числе прочего утверждается, что многие оптимизирующие преобразования программ суть реализации категорной конструкции под названием правое расширение Кана. Типа вся сущность СиПиЭс была изложена в упражнениях к десятой главе известной книги ``Categories for the working mathematician''. Хорошо бы понять так ли это.

Сегодня будет разогрев.



Одним из наиболее часто встречающихся примеров [ковариантных] функторов в computer science являются параметрические структуры данных. Если у вас есть контейнер F, в который вы можете засунуть выражения произвольного типа A, то это эндофунктор для [некоторой] категории множеств и функций. Точно описать эту категорию сложно, но вычислительный смысл очень простой: любую функцию из A в B можно поднять до функции из F A в F B, при этом будут выполнятся ожидаемые для функторов отношения. Вот, например, список в Haskell определяется так:

data List a = Nil | Cons a (List a)

List -- это функтор из Set в Set:
map :: (A → B) → List A → List B
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

Ну и выполняются: map id xs = xs и map (f ∘ g) xs = map f (map g xs). Чем не функтор?

Нужно отметить, что с пришествием зависимых типов, стало возможным определять функторы, отличные от эндофункторов на Set. Например, берете любой тип деревьев, цепляете к нему дополнительный конструктор для переменных (переменные типа конечных множеств), получаете семейство над натуральными числами. Это будет функтор из категории конечных множеств в категорию множеств. Произвольная функция из одного конечного множества в другое это ``переименование переменных'', а соответствующий map переименовывает все переменные в вашей древовидной структуре. Если задать операцию подстановки, то это будет монада. Если хотите почитать про монады в computer science, то начните с этого ответа. Pigworker -- это ник Конора МакБрайда. ``Он бог, от него сияние исходит''.


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

newtype List a = Abstr {apply :: forall z . (Monoid z) => (a -> z) -> z}

Утверждается, что это тоже самое, что и List, определенный выше. Чрезвычайно поучительно попытаться определить для этого типа обычные конструкторы Nil и Cons, а также функции голова/хвост (Ответ тут). Реклама говорит, что когда допилят вычислительную сторону унивалентности, то определения функций можно будет автоматически переносить между эквивалентными представлениями... удачи им с этим.

Этот новый тип обладает O(1) сложностью для cons, snoc и append. Утверждается, что этот трюк с уменьшением сложности есть частный случай общей конструкции, связанной с ``правыми расширениями Кана''. Поговорим об этом в следующих выпусках.



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

Картинка для привлечения внимания: