Про Йонеду и про должения
Mar. 22nd, 2012 06:54 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonЛемму Йонеды называют самой сложной тривиальной вещью в математике. Сегодня мы попробуем закодировать ее на Окамле и понять ее связь с продолжениями (continuations). Лемма эта из теории категорий, я буду объяснять на пальцах, не слишком строго. В категории у нас есть коллекция объектов (порой очень большая, настолько, что это даже не обязательно множество) и коллекция стрелок между ними, также называемых морфизмами. Знакомый нам пример категории - где объекты это типы данных, а стрелки - функции между ними. Функтором называется отображение одной категории в другую (или в ту же, тогда это эндофунктор), сохраняющее структуру - "рисунок" стрелок. Он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно. Конструкторы типов, вроде списка или дерева, - примеры (эндо)функторов в знакомой нам категории. Функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list, а функции вроде int -> string превращает в функции вроде int list -> string list. Такие вещи очень просто записываются на хаскеле, но сегодня я хочу использовать окамл, все-таки он наследник categorical abstract machine language. На окамле функтор в общем виде можно так, например, описать:
Это сигнатура модуля, "интерфейс". Реализуя его для конкретных конструкторов типов, вроде списка или дерева, мы получим конкретные функторы.
Если мы в некоторой категории С возьмем произвольный объект А, то мы можем придумать такой функтор h_A, который всякий объект Х из той же категории отображает во множество Hom(A,X) всех стрелок из А в Х, имеющихся в этой категории. Он отображает С в Set, но в языках программирования у нас все функторы - эндофункторы, работающие в пределах одной и той же категории типов (часто именуемой Hask). Однако если под объектом int понимать множество значений типа int, а под стрелкой int -> string множество функций из int в string, то можно помирить Hask и Set.
Так, если мы выберем в качестве объекта А тип string, то можем построить функтор h_string:
где << - композиция функций:
Он значения типа Х превращает в функции из 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) есть взаимно-однозначное соответствие. Вот как это выглодит на окамле:
Здесь 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 как раз и определяют те два изоморфизма. Проверить формально, что они друг для друга обратные, можно, аккуратно подставив определения, это оставлю в качестве домашнего задания.
А вот пример кода, их использующий:
Возьмем в качестве функтора 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). Пример: опишем тип дерева и функцию подсчета его размера:
Здесь рекурсия не хвостовая, она будет жрать стек и может привести к его переполнению. Чтобы сделать хвостовую рекурсию, можно применить CPT:
В примере мы вычисляем размер дерева, переводим его в строку и выводим. У нас есть исходная функция tree_size типа 'a tree -> int, ее результат используется в string_of_int типа int -> string, это здесь локальное продолжение tree_size. Полученная в результате continuation-passing преобразования хвостато-рекурсивная tree_size2 принимает продолжение string_of_int в качестве параметра и возвращает уже строку. Внутри нее та же картина: раньше мы вычисляли размеры поддеревьев и использовали их для вычисления размера текущего дерева, теперь же это использование результата, продолжение, само стало функцией-аргументом, которая применяется к возвращаемому значению. Такие дела.
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 в качестве параметра и возвращает уже строку. Внутри нее та же картина: раньше мы вычисляли размеры поддеревьев и использовали их для вычисления размера текущего дерева, теперь же это использование результата, продолжение, само стало функцией-аргументом, которая применяется к возвращаемому значению. Такие дела.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-07-16 06:28 pm (UTC)А с чего бы отображению (какому именно, кстати? ) добавлять точки?
no subject
Date: 2012-07-16 06:54 pm (UTC)Но в оригинале же вопрос стоял о "head не может быть применён к пустому списку". Почему же не может? Вот в объекте List(A) пустой список есть.
"добавлять точки"
Ну, когда два объекта объединяются, т.е. A+B, в сумме как-бы есть точки обоих. (исходя из определения, что ко-продукт состоит из пар (i,Ai) - вот и пытаюсь осознать, как выглядит отображение из List(A) в (i,Ai), где точке "пустой список" соответствует ЧТО-ТО (0,0) - но это не может быть точкой, т.к. точки у 0 нет)
no subject
Date: 2012-07-16 07:03 pm (UTC)Каких еще пар? В определении такого не было.
В ЯП [a] + 0 будет Either [a] _|_. Там всякий список xs превратится в Left xs. А c Right ни одного значения не будет.
no subject
Date: 2012-07-16 07:17 pm (UTC)Вот у нас есть f: A->C, g: B->C, [f;g]: (A+B)->C . Как [f;g] "переводит" одно значение типа A+B в _одно_ значение типа C? В общем случае, как [f_i] переводит одно значение типа ⊔A_i в одно значение типа С?
Я сейчас уже не найду, где видел определение с парами, но оно makes a lot of sense: глядя на точку из (A+B), мы можем сказать, какое i ему соответствует, а потому _которую_ из f_i "применить" к той точке.
no subject
Date: 2012-07-16 07:41 pm (UTC)Но это необязательно должны быть пары. Например, в категории, где объекты - натуральные числа, а стрелки идут из больших в меньшие (отношение >), копроизведение a и b - это просто min(a,b), число, без всяких пар.
no subject
Date: 2012-07-16 08:26 pm (UTC)no subject
Date: 2012-07-16 09:00 pm (UTC)Именно, что "можно представить". Точкам всё равно, как я их себе представляю :)
no subject
Date: 2012-07-16 07:21 pm (UTC)Да, всякий список xs превратится в Left xs. Но head для всякого ли списка будет Left a? Вот именно, что для пустого списка будет Right. И поскольку его нельзя создать, вот тут у меня и выходит затык с пониманием. Это можно как-то осознать, наверное, если перестать думать о точках, а рассматривать композиции функций. Важно не наличие "точки" (0,0), а условие, когда head commutes со стрелкой из 0.
no subject
Date: 2012-07-16 07:44 pm (UTC)