Про Йонеду и про должения

[thedeemon]

Лемму Йонеды называют самой сложной тривиальной вещью в математике. Сегодня мы попробуем закодировать ее на Окамле и понять ее связь с продолжениями (continuations). Лемма эта из теории категорий, я буду объяснять на пальцах, не слишком строго. В категории у нас есть коллекция объектов (порой очень большая, настолько, что это даже не обязательно множество) и коллекция стрелок между ними, также называемых морфизмами. Знакомый нам пример категории - где объекты это типы данных, а стрелки - функции между ними. Функтором называется отображение одной категории в другую (или в ту же, тогда это эндофунктор), сохраняющее структуру - "рисунок" стрелок. Он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно. Конструкторы типов, вроде списка или дерева, - примеры (эндо)функторов в знакомой нам категории. Функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list, а функции вроде int -> string превращает в функции вроде int list -> string list. Такие вещи очень просто записываются на хаскеле, но сегодня я хочу использовать окамл, все-таки он наследник categorical abstract machine language. На окамле функтор в общем виде можно так, например, описать:

module type Functor = sig 
  type 'a t 
  val fmap : ('a -> 'b) -> 'a t -> 'b t 
end 

Это сигнатура модуля, "интерфейс". Реализуя его для конкретных конструкторов типов, вроде списка или дерева, мы получим конкретные функторы.

Если мы в некоторой категории С возьмем произвольный объект А, то мы можем придумать такой функтор h_A, который всякий объект Х из той же категории отображает во множество Hom(A,X) всех стрелок из А в Х, имеющихся в этой категории. Он отображает С в Set, но в языках программирования у нас все функторы - эндофункторы, работающие в пределах одной и той же категории типов (часто именуемой Hask). Однако если под объектом int понимать множество значений типа int, а под стрелкой int -> string множество функций из int в string, то можно помирить Hask и Set.

Так, если мы выберем в качестве объекта А тип string, то можем построить функтор h_string:

module H_String : Functor = struct  
  type 'a t = string -> 'a 
  let fmap : ('a -> 'b) -> (string -> 'a) -> (string -> 'b)  
           = fun fab gsa -> fab << gsa    
end

где << - композиция функций:

let (<<) f g x = f (g x)

Он значения типа Х превращает в функции из string в Х.

Если у нас есть категории С и D, и два функтора F и G, каждый из которых отображает категорию С в категорию D, то можно представить отображение одного функтора в другой. Оно каждому объекту Х из С сопоставит стрелку в D, идущую из F(X) в G(X), т.е. опишет как превратить образ, получающийся первым функтором, в образ, получающийся вторым. Такое отображение функторов (с выполненными требованиями сохранения структуры) называется естественным преобразованием. В принципе, все полиморфные функции, вроде head и tail для списков, fst и snd для туплов, - это естественные преобразования. Они работают с формой структуры данных, не трогая ее наполнение, не зная конкретного его типа, т.е. превращают один функтор в другой.

Теперь возьмем описанный выше функтор h_A, отображающий С в Set, и некоторый другой функтор F, тоже из С в Set, тогда можно рассмотреть множество отображений (естественных преобразований) из первого во второй. Назовем это множество Nat(h_A, F). Так вот, лемма Йонеды говорит, что это множество изоморфно F(A):

Напомню, что А - некоторый объект категории С, который мы зафиксировали, а F отображает объекты во множества, так что F(A) - множество, и между ним и множеством отображений Nat(h_A, F) есть взаимно-однозначное соответствие. Вот как это выглодит на окамле:

let id : 'a . 'a -> 'a = fun x -> x 

module M(F : Functor) = struct 
  type 'a natt = { fn : 'b . ('a -> 'b) -> 'b F.t }   
  let yoneda : 'a F.t -> 'a natt = fun a -> { fn = fun f -> F.fmap f a }   
  let adenoy : 'a natt -> 'a F.t = fun t -> t.fn id 
end 

Здесь F - параметр, произвольный функтор (выразимый в ЯП).
'a natt - тип, описывающий множество естественных преобразований между h_A и F, т.е. Nat(h_A, F). Каким образом? Прямо по определению: всякому объекту В исходной категории, т.е. всякому типу 'b, соответствует стрелка между его образами, получаемыми двумя функторами. Образ 'b, т.е. h_A(В), - это множество функций типа ('a -> 'b). F(B) - образ В в функторе F, записывается прямо - 'b F.t. Выражение "для любого типа 'b", то что в хаскеле обозначается "forall b .", в окамле пишется "'b .", но доступна такая конструкция не в любом месте. Она доступна, в частности, в определении структур, и тут мы описали структуру с одним полем по имени fn такого вот полиморфного типа.

Итак, мы описали Nat(h_A, F) - 'a natt, внутри которого используется F, переданный параметром модуля, а F(A) - это просто 'a F.t. Лемма говорит, что они изоморфны, т.е. между ними есть две стрелки-изоморфизма, такие, что их композиции в обе стороны (туда-сюда и сюда-туда) дают identity. Каждая такая стрелка в нашей категории - это функция. Описанные выше функции yoneda и adenoy как раз и определяют те два изоморфизма. Проверить формально, что они друг для друга обратные, можно, аккуратно подставив определения, это оставлю в качестве домашнего задания.
А вот пример кода, их использующий:

let module L = M(struct type 'a t = 'a list let fmap = List.map end) in 
let open L in 
let nt = yoneda [3; 2; 1] in 
let strings = nt.fn string_of_int in 
let floats = nt.fn float_of_int in 
List.iter print_endline strings; 
List.iter (Printf.printf "%f ") floats; 
let back = adenoy nt in 
List.iter (Printf.printf "%d ") back;; 

Возьмем в качестве функтора F список, передадим его параметром в модуль М, где описаны наши типы и функции, сообщив, что в качестве конструктора типов 'a t надо брать 'a list, а fmap - это простой List.map. Возьмем в качестве объекта А тип int, тогда F(A) - список интов. Передадим список интов [3; 2; 1] в нашу функцию-изоморфизм yoneda и получим значение nt типа int natt. Это естественное преобразование, которое для любого типа 'b из Hom(int, 'b), т.е. функции int -> 'b, сделает список значений типа 'b, т.е. F('b). Применим его для парочки типов string и float, передав функции string_of_int и float_of_int, получим автоматически список строк и список флоатов. Внутри она просто помнит список интов, полученный при рождении, и применяет к нему поэлементно переданную функцию. Это потому что в качестве функтора F мы выбрали список, а его fmap - это List.map, поэлементное преобразование. Сдругим функтором она бы делала что-то другое, но код не меняется, он сводится к использованию fmap функтора. Потом передадим это чудо-значение nt в обратный морфизм adenoy и получим back - исходный список интов. Вот и вся Йонеда.

Какое же это имеет отношение к продолжениям? Возьмем частный случай, когда в качестве F взят функтор h_С для некоторого выбранного объекта С (аналогичный нашему h_A, просто с другим объектом). Тогда для любого типа 'b его образ F('b) - это тип функций ('c -> 'b), а для типа 'a, который мы зафиксировали для h_A, F('a) - это ('c -> 'a). И тогда формулировка леммы
Nat(h_A, F) ~~ F(A)
превращается в
('b . ('a -> 'b) -> ('c -> 'b)) ~~ ('c -> 'a)
где ~~ означает взаимно-однозначное соответствие, выражаемое наличием двух изоморфизмов туда-сюда. В частности,
('c -> 'a) -> ('b . ('a -> 'b) -> ('c -> 'b))
А что это значит? Что если у нас есть функция f типа ('c -> 'a), то для любого типа 'b всякий раз, когда результат вызова f (значение типа 'a) используется для получения какого-то значения типа 'b, это самое использование можно рассматривать как продолжение f. Их можно объединить и из f и ее такого продолжения соорудить функцию типа ('c -> 'b), которая сперва к аргументу типа 'c применит f, получив 'a, а потом ее продолжение, получив 'b. Такое преобразование и есть continuation passing transform (CPT). Пример: опишем тип дерева и функцию подсчета его размера:

type 'a tree = Leaf | Node of 'a * 'a tree * 'a tree 
 
let rec tree_size = function  
  | Leaf -> 1 
  | Node(_, l, r) -> 1 + tree_size l + tree_size r 

Здесь рекурсия не хвостовая, она будет жрать стек и может привести к его переполнению. Чтобы сделать хвостовую рекурсию, можно применить CPT:

let rec tree_size2 tr k = match tr with 
  | Leaf -> k 1 
  | Node(_, l, r) -> tree_size2 l (fun lsz -> tree_size2 r (fun rsz -> k (1+lsz+rsz)));;  
 
let tr = Node("a", Leaf, Node("b", Leaf, Leaf)) in  
print_string (string_of_int (tree_size tr)); 
print_string (tree_size2 tr string_of_int);; 

В примере мы вычисляем размер дерева, переводим его в строку и выводим. У нас есть исходная функция tree_size типа 'a tree -> int, ее результат используется в string_of_int типа int -> string, это здесь локальное продолжение tree_size. Полученная в результате continuation-passing преобразования хвостато-рекурсивная tree_size2 принимает продолжение string_of_int в качестве параметра и возвращает уже строку. Внутри нее та же картина: раньше мы вычисляли размеры поддеревьев и использовали их для вычисления размера текущего дерева, теперь же это использование результата, продолжение, само стало функцией-аргументом, которая применяется к возвращаемому значению. Такие дела.

Comments

[109.livejournal.com]

отличный пост.

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

[thedeemon.livejournal.com]

Ну вот возьмем натуральные числа в качестве объектов. Если мы скажем, что стрелка соединяет А и В, когда А >= B, то все отлично, это годная категория (и id там есть - A >= A). Но вот если мы скажем, что стрелка соединяет А и В, когда А > В, то это хоть и будет похоже на категорию, но id там не будет. И просто так "добавить морфизм объекта в самого себя и заявить" не получится, ведь это будет означать, что мы постулируем А > А, а это только проблемы нам даст.

[109.livejournal.com]

дык и так думал! но я-то в категориях не шарю. а вот вова типа шарит, и пишет туториалы, чтобы другие учились:

2. A partially ordered set can be represented as a category. The set's elements are objects. Add a single arrow a → b for each pair a, b such that a < b, and unit arrow a → a for each a. For each pair of objects there's no more than one arrow, and since partial order is transitive, we have composition (a<b, b<c => a<c), and there is no need to worry about its associativity.

http://www.patryshev.com/monad/m-cex2.html

[thedeemon.livejournal.com]

Partially ordered set действительно образует категорию, просто в определение частичного порядка входит рефлексивность (a <= a).
http://en.wikipedia.org/wiki/Partially_ordered_set
Так что в этом его фрагменте я бы заменил < на <=, стало бы проще.

[109.livejournal.com]

а все arrow должны обозначать одно и то же? не может быть два типа arrows в одной категории?

[thedeemon.livejournal.com]

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

Возьмем предложенный пример с числами, пусть стрелка из А в В означает А > B, а стрелка другого типа из А в А, id, означает А = А. Допустим у нас в категории определено произведение: произведением АхВ называется такой объект, из которого есть стрелки в А и в В, при этом из любого другого объекта С, из которого тоже есть стрелки в А и В, должна быть стрелка в АхВ. Вот мы для некоторых А и В обнаружили С, из которого есть стрелки в А и в В. Значит, должна быть стрелка из С в АхВ. Но какая это стрелка, что она означает? Что С = АхВ или что С > AxB? Теряется всякая польза. А вот если стрелка означает >=, то все однозначно: АхВ - это max(A,B), поэтому если из какого-то С есть стрелки в А и В, это однозначно означает, что С >= А и С >= В, и существующая по определению произведения стрелка из С в АхВ однозначно означает С >= max(A,B). Это вполне понятный и осмысленный результат.

[109.livejournal.com]

спасибо! теперь я знаю, к кому обращаться с вопросами по теории категорий. а то ни faceted_jacinth, ни ivan_gandhi вразумительно не ответили.

[thedeemon.livejournal.com]

Я в этой теме нуб, есть и пограмотнее товарищи, тот же nivanych.

[109.livejournal.com]

тут важно, кто объяснить может в доступной форме.

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

> если нет натуральной identity,
> добавить морфизм объекта в самого себя

Более того, если для стрелок a→b→c не существует стрелки-композиции, то можно её добавить!
В итоге, можно сказать, что категория представляет собой транзитивно замкнутый граф с петельками. По сравнению с графом, есть важное свойство — сравнение стрелок. Но если это сравнение убрать, получим просто граф.
Итого, получим забывающий функтор из категории категорий в категорию графов. Он является правым сопряжённым.
Левый сопряжённый к нему, это достройка графа до категории — все стрелки объявляются разными, достраиваются id-стрелки, достраиваются композиции.

[109.livejournal.com]

> Более того, если для стрелок a→b→c не существует стрелки-композиции, то можно её добавить!

что это значит?

> По сравнению с графом, есть важное свойство — сравнение стрелок.

что это значит? можно примеры?

> забывающий функтор

что это значит?

> Он является правым сопряжённым

я боюсь, что вы немного переоценили своё умение объяснять. по крайней мере, мне.

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

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

[nivanych.livejournal.com]

> а с целью продемонстрировать знание умных слов.

Ото ж! Конечно! Не наговорился умных слов ;-)
С целью, чтобы было понятно хоть что-то и возникло любопытство по поводу остального. Да, таки лишку.

В графе могут быть стрелки a→b→c, но может не быть стрелки a→c.
В категории обязательно должна существовать композиция.
И если мы в некий граф добавляем такие композиции плюс единичные стрелки, получаем уже категорию.
Но важное свойство категории, это equational reasoning про стрелки. Мы можем сравнивать стрелки и для этого есть некоторые правила, например, из определения категорий —
(f o g) o h = f o (g o h)
Могут существовать и другие правила, если категория обладает какими-нибудь дополнительными свойствами.
Забывающий функтор, это не точное определение, это такой собирательный образ. Означает такой функтор, который "забывает" структуру. Например, можно из категории групп и их гомоморфизмов сделать функтор во множества, который будет забывать о том, что гомоморфизмы какими-то там свойствами обладают и делать их просто отображениями не групп, а множеств.
Точно так же, можно составить категорию, в которой объектами являются категории, а стрелками — функторы. Или объекты — графы, а стрелки — их гомоморфизмы.
И функтор из категории категорий в категорию графов, который будет забывать, что стрелки в категории и делать из рёбрами в графе, будет забывающим. Это пример правого сопряжённого функтора.
К нему есть другой функтор, который по двум графам и гомоморфизмам между ними продолжит графы до категории, а гомоморфизмы до функторов между этими категориями. Это пример левого сопряжённого функтора.
Сопряжённые функторы имеют строгое определение, которое я тут приводить не буду. Просто хотел привести простой пример "страшного" понятия.
Может быть, как-нибудь я напишу за эту тему, когда-то я довольно-таки интересовался нахождением способов объяснения этих понятий.
Сейчас хоть понятнее?...

Про разные типы скажу, что в определении категории такого не бывает. Просто бывают особенные категории, при определении которых специально разделяют стрелки на несколько классов. Это всё стрелки одной категории, но например, покрашенные в разные цвета ;-) И в пределах данной категории их можно соединять и получать другие стрелки, про которые тоже должны быть правила, какого цвета они получатся.

[sassa-nf.livejournal.com]

А можно про adjoints вопрос?

Вот есть у нас co-unit: F(G(Y)) -> Y. Дык, G(co-unit) вроде-бы concat получается?

[nivanych.livejournal.com]

concat — это термин для списков...
Но видимо, подразумевается композиция стрелок.
Насколько я понял, F — построение категории из графа, G — забывающий. Левый и правый сопряжённые соответственно.
F(G Y) получается Id-функтором, однако. Ко-единица сопряжения получается, это естественное преобразование Id Y → Y и суть идентичность...
Но вообще — как должна выглядеть композиция стрелок? Как нечто с двумя параметрами.
Я просто по типам не понимаю, как тут может быть выражено соединение стрелок.
Но это всё "как-то близко", да.

[sassa-nf.livejournal.com]

вообще-то я думал от concat до mu: T[T[X]]->T[X] не далеко.

Не знаю, важно ли, что G - забывающий.

Вот есть категории C и D, а F и D - adjoint. Пусть T=List: G o F. Тогда F(X) - это список в категории D, а G(F(X)) - это отображение списка в категории C.

Пусть Y - это D-object, т.е. некоторое F(X). Тогда adjoint unit соединяет X и G(F(X)), т.е. X и T(X), а adjoint co-unit соединяет F(G(Y)) и Y, т.е. F(G(F(X))) и F(X). Поскольку G отображает всю категорию D, то он отображает и co-unit в морфизм G(F(G(Y))) -> G(Y), т.е. G(F(G(F(X))))->G(F(X)), т.е. T(T(X))->T(X).


Это как бы намекает нам, что либо все adjoints являются монадами (чо, правда?..), либо не все co-units выполняют условия для mu. Вот у меня и вопрос: если второе, то какие условия и как co-unit может не выполнять?

[sassa-nf.livejournal.com]

тьфу, F и G - adjoint, конечно

[sassa-nf.livejournal.com]

Сорри, насчёт every adjoint is a monad уже выяснил: так и есть, всякий GoF является монадой, если (F,G) - adjoint.

Осталось уточнить, можно ли постановить mu=G(co-unit).

[nivanych.livejournal.com]

> (F,G) - adjoint

Обычно, пишут F -| G.
Ну а FoG является комонадой. И по (ко)монаде есть аж целых два стандартных способа получить сопряжённую пару.
Единица монады, полученной из сопряжённой пары, это единица сопряжения, а умножение μ=GεF, где ε — коединица.
В общем случае — как может GεF равняться Gε?...

[sassa-nf.livejournal.com]

"В общем случае — как может GεF равняться Gε?..."

дык, Gε применяется только к объектам категории D, потому F само собой разумеется, если исходный объект в категории C.

Ну, я извиняюсь, я ж не знаю, как это пишется на сам-деле :) Но, по-моему, μ=GεF как раз и означает то, что мне нутром чуялось, а щас вот ещё на листочке порисовал - одну диаграммку уже могу объяснить. :)

G(co-unit) - это же и есть C-образ некоторого D-arrow, ε.

С вашего позволения, μ_C=Gε_DF

[nivanych.livejournal.com]

Я уже запутался.
А в чём вопрос?

[sassa-nf.livejournal.com]

Ну, сейчас вопроса нет. А был вопрос - "правда ли, что μ - это C-образ D-стрелки ε, т.е. ко-единицы?"

А то я на бумажке из co-unit diagram такой вывод вижу, но в своих рассуждениях не уверен, и до μ=GεF ещё не дочитал.

[sassa-nf.livejournal.com]

о.... вот сегодня дошло, что значит GεF.

Я-таки неправильно понял, что это означает. μ is not the same as G(ε); это лишь часть G(ε), касающаяся D-объектов, являющихся образом каких-то C-объектов.

Поскольку ε: F.G → I_D, то оно определено и для некоторых Y, которые не являются образами чего-то из C. Поэтому G(ε): G.F.G → G is a natural transformation между функторами, которые отражают и D-объекты, которые не являются образами чего-то из C.

Тогда, конечно, тривиально μ="G(ε.F)": G.F.G.F → G.F

[nivanych.livejournal.com]

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