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

[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

[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]

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