слово о трансдюсерах
Sep. 21st, 2014 04:41 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonПосмотрел тут свежее выступление известного программиста компьютеров в гамаке Р. Хики. Доклад про трансменьшители.
Помните, во всяких учебниках про ФП есть упражнения по выражению различных функций над списками через fold? Почему именно через fold, а не что-то другое? Да потому что это Котоморфизм Всемогущий: тот самый уникальный морфизм, что идет от инициального объекта к каждому другому, в данном случае в категории алгебр заданного эндофунктора. Ведь что такое список с элементами типа Е? Каждое его значение это либо константа 1 (Nil, [] - ей изоморфны), либо пара (произведение) из Е и аналогичного списка - хвоста. Т.е. 1 + Е*Х. Берем функтор F(X) = 1 + E*X. Нам нужна рекурсивная конструкция, чтобы вместо Х везде был "список из Е", а значит надо ListE = 1 + E * (ListE) = F(ListE). Раз получили ListE = F(ListE), значит нужна неподвижная точка. Построить ее несложно:
newtype Fix f = Fx (f (Fix f))
и для конструктора Fx можно сразу записать обратную функцию
Для всякого эндофунктора F и типа Т, если взять функцию alg: F T -> T, то такая тройка из F, T, и alg называется F-алгеброй. Если F - функтор, т.е. в интересующей нас категории это конструктор типов, то Fix F - уже просто тип, вполне конкретный для данного функтора. Подставив его вместо Т в определение F-алгебры, получим F-алгебру (F, Fix F, alg : F (Fix F) -> Fix F). Сравнив тип alg и Fx выше, видим, что Fx и есть такая алгебра. Утверждается, что эта алгебра для F особенная: она инициальная, т.е. служит инициальным объектом в категории F-алгебр для F, т.е. для любой другой алгебры в нем, т.е. любой пары из типа Т и функции alg : F T -> T существует функция g из инициального объекта Fix F в T. Да такая, что вот эта диаграмма коммутирует, т.е. оба пути из f (Fix f) в Т эквивалентны:
Почему такая g существует? Да потому что мы можем взять обратную для Fx функцию unFix, и просто определить g как композицию из unFix, fmap g и alg:
Поскольку g зависит от alg, опишем это как функцию g = cata alg:
Это работает для произвольного эндофунктора, так можно опрелять самые разные рекурсивные индуктивные типы, и катаморфизм для них всегда будет работать сверткой: он позволяет из значения рекурсивного типа (скажем, AST-дерева или списка) получить значение произвольного типа (например, строку), если есть функция-алгебра, умеющая делать один шаг свертки. Например, если у нас есть список интов, и мы хотим его превратить в строку, то
E = Int
F(X) = 1 + Int * X
List_Int = Fix F = 1 + Int * List_Int
T = String
alg : F T -> T = 1 + Int * String -> String
т.е. alg должна уметь делать строку из ничего (1, пустой список) и из пары элемент * строка, где та строка получена из хвоста списка этой же операцией рекурсивно. Передав такую алгебру в котоморфизм cata, получим функцию Fix f -> a т.е. List_Int -> String. Узнаете? Этот котоморфизм и есть foldr для списка! Все, что можно сделать из списка (по крайней мере операциями вроде alg - берущими по одному элементу и некоторым образом наращивающими свой результат), можно сделать fold'ом. Более того, если мы хотим выразить алгебраический тип в языке без оных но с функциями, можно использовать Church encoding или типизированный Boehm-Berarducci encoding, и результат будет выглядить точно как тот fold. А алгебра, что передается в катаморфизм, получила у Хики новое имя - reducerинновация!.
Ну так вот, увидел Хики, что fold это хорошо, но заметил, что реализуя через него операции над списками мы почему-то используем конструкторы списка. А при реализации оных для векторов - конструкторы векторов. Непорядок, недообобщение!
Только один-то конструктор он заметил, а про второй забыл:
Если conj заменить на построитель не-векторов, а [] оставить, будет банальная ошибка типов. В этой его кложури - еще и в рантайме. Ибо про функторы с алгебрами не думал, там-то тип сразу показывает о каких вариантах надо заботиться. Ну и предложил абстрагироваться, вынести конструктор из кода в параметр:
Получилось, что внутри там функция принимает такой конструктор (вроде cons или conj), фрагмент алгебры, a.k.a. reducer, и возвращает такой же. Ну а функции вида Хрень -> Хрень хорошо композятся. Придумал для такого преобразования reducer -> reducer новое имя: transducerинновация!. Но поскольку половину алгебры он в самом начале потерял, в таком виде оно не работает, конечно. Пришлось добавлять хаки. Хак первый: писал он на кложури, а она позволяет функции принимать разное число аргументов и в зависимости от этого вести себя по-разному. Ну и сделал, что ежели аргументов не дали, то пусть работает как вторая половина алгебры: пусть возвращает значение, соответствующее пустому списку. А еще захотел уметь прерывать обработку, не доходя до конца списка. Всякие хаскели это в foldr делают легко за счет ленивости: не обращайся к вычисленному хвосту, он и не будет вычисляться. А в кложури все иначе, поэтому сделал сигналирование о конце заворачиванием значения в специальную обертку, такой вот модный динамически-типизированный способ передать булев флаг. Ну и сделал третий вариант функции от двух аргументов, принимающий лишь один аргумент, в таком случае там она что-то сигналирует. В результате то, что выглядит как композиция функций, есть композиция троек функций (от 0, 1 и 2 аргументов), работающих с неожиданно типизированными вещами. Теперь весь мир побежал это дело переписывать на другие языки. Но мы-то знаем, что, учитывая форму этих алгебр-уменьшателей, речь все равно только о списках и эквивалентных им вещах, и поскольку среди всех таких структур список - самый общий (свободный моноид, панимаиш), то все эти трансменьшители сводятся к такому типу:
transducer: [a] -> [b]
Зато инновации!
Помните, во всяких учебниках про ФП есть упражнения по выражению различных функций над списками через fold? Почему именно через fold, а не что-то другое? Да потому что это Котоморфизм Всемогущий: тот самый уникальный морфизм, что идет от инициального объекта к каждому другому, в данном случае в категории алгебр заданного эндофунктора. Ведь что такое список с элементами типа Е? Каждое его значение это либо константа 1 (Nil, [] - ей изоморфны), либо пара (произведение) из Е и аналогичного списка - хвоста. Т.е. 1 + Е*Х. Берем функтор F(X) = 1 + E*X. Нам нужна рекурсивная конструкция, чтобы вместо Х везде был "список из Е", а значит надо ListE = 1 + E * (ListE) = F(ListE). Раз получили ListE = F(ListE), значит нужна неподвижная точка. Построить ее несложно:
newtype Fix f = Fx (f (Fix f))
и для конструктора Fx можно сразу записать обратную функцию
unFix :: Fix f -> f (Fix f) unFix (Fx x) = x
Для всякого эндофунктора F и типа Т, если взять функцию alg: F T -> T, то такая тройка из F, T, и alg называется F-алгеброй. Если F - функтор, т.е. в интересующей нас категории это конструктор типов, то Fix F - уже просто тип, вполне конкретный для данного функтора. Подставив его вместо Т в определение F-алгебры, получим F-алгебру (F, Fix F, alg : F (Fix F) -> Fix F). Сравнив тип alg и Fx выше, видим, что Fx и есть такая алгебра. Утверждается, что эта алгебра для F особенная: она инициальная, т.е. служит инициальным объектом в категории F-алгебр для F, т.е. для любой другой алгебры в нем, т.е. любой пары из типа Т и функции alg : F T -> T существует функция g из инициального объекта Fix F в T. Да такая, что вот эта диаграмма коммутирует, т.е. оба пути из f (Fix f) в Т эквивалентны:
Почему такая g существует? Да потому что мы можем взять обратную для Fx функцию unFix, и просто определить g как композицию из unFix, fmap g и alg:
Поскольку g зависит от alg, опишем это как функцию g = cata alg:
cata :: Functor f => (f a -> a) -> Fix f -> a cata alg = alg . fmap (cata alg) . unFix
Это работает для произвольного эндофунктора, так можно опрелять самые разные рекурсивные индуктивные типы, и катаморфизм для них всегда будет работать сверткой: он позволяет из значения рекурсивного типа (скажем, AST-дерева или списка) получить значение произвольного типа (например, строку), если есть функция-алгебра, умеющая делать один шаг свертки. Например, если у нас есть список интов, и мы хотим его превратить в строку, то
E = Int
F(X) = 1 + Int * X
List_Int = Fix F = 1 + Int * List_Int
T = String
alg : F T -> T = 1 + Int * String -> String
т.е. alg должна уметь делать строку из ничего (1, пустой список) и из пары элемент * строка, где та строка получена из хвоста списка этой же операцией рекурсивно. Передав такую алгебру в котоморфизм cata, получим функцию Fix f -> a т.е. List_Int -> String. Узнаете? Этот котоморфизм и есть foldr для списка! Все, что можно сделать из списка (по крайней мере операциями вроде alg - берущими по одному элементу и некоторым образом наращивающими свой результат), можно сделать fold'ом. Более того, если мы хотим выразить алгебраический тип в языке без оных но с функциями, можно использовать Church encoding или типизированный Boehm-Berarducci encoding, и результат будет выглядить точно как тот fold. А алгебра, что передается в катаморфизм, получила у Хики новое имя - reducerинновация!.
Ну так вот, увидел Хики, что fold это хорошо, но заметил, что реализуя через него операции над списками мы почему-то используем конструкторы списка. А при реализации оных для векторов - конструкторы векторов. Непорядок, недообобщение!
Только один-то конструктор он заметил, а про второй забыл:
Если conj заменить на построитель не-векторов, а [] оставить, будет банальная ошибка типов. В этой его кложури - еще и в рантайме. Ибо про функторы с алгебрами не думал, там-то тип сразу показывает о каких вариантах надо заботиться. Ну и предложил абстрагироваться, вынести конструктор из кода в параметр:
Получилось, что внутри там функция принимает такой конструктор (вроде cons или conj), фрагмент алгебры, a.k.a. reducer, и возвращает такой же. Ну а функции вида Хрень -> Хрень хорошо композятся. Придумал для такого преобразования reducer -> reducer новое имя: transducerинновация!. Но поскольку половину алгебры он в самом начале потерял, в таком виде оно не работает, конечно. Пришлось добавлять хаки. Хак первый: писал он на кложури, а она позволяет функции принимать разное число аргументов и в зависимости от этого вести себя по-разному. Ну и сделал, что ежели аргументов не дали, то пусть работает как вторая половина алгебры: пусть возвращает значение, соответствующее пустому списку. А еще захотел уметь прерывать обработку, не доходя до конца списка. Всякие хаскели это в foldr делают легко за счет ленивости: не обращайся к вычисленному хвосту, он и не будет вычисляться. А в кложури все иначе, поэтому сделал сигналирование о конце заворачиванием значения в специальную обертку, такой вот модный динамически-типизированный способ передать булев флаг. Ну и сделал третий вариант функции от двух аргументов, принимающий лишь один аргумент, в таком случае там она что-то сигналирует. В результате то, что выглядит как композиция функций, есть композиция троек функций (от 0, 1 и 2 аргументов), работающих с неожиданно типизированными вещами. Теперь весь мир побежал это дело переписывать на другие языки. Но мы-то знаем, что, учитывая форму этих алгебр-уменьшателей, речь все равно только о списках и эквивалентных им вещах, и поскольку среди всех таких структур список - самый общий (свободный моноид, панимаиш), то все эти трансменьшители сводятся к такому типу:
transducer: [a] -> [b]
Зато инновации!
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2014-09-21 09:55 am (UTC)no subject
Date: 2014-09-21 03:30 pm (UTC)no subject
Date: 2014-09-21 10:15 am (UTC)no subject
Date: 2014-09-21 12:15 pm (UTC)no subject
Date: 2014-09-21 12:19 pm (UTC)Немноожечко не хватает понятия (ко)алгебр над (ко)монадой и рассказа о топосах этих (ко)алгебр в топосе.
Если монада T над неким топосом имеет правый сопряжённый, то категория T-алгебр (над этой монадой) — топос.
no subject
Date: 2014-09-21 12:25 pm (UTC)ой. существование g определено через существование fmap g...
Там сложнее, и необходимо не просто unFix, а именно изоморфизм, а от функтора требуется сохранение пределов. Функция g существует как раз из-за сохранения пределов.
no subject
Date: 2014-09-21 12:30 pm (UTC)no subject
Date: 2014-09-21 02:50 pm (UTC)или может лучше сказать, что полиномиальные эндофункторы сохраняют пределы (а в х-е все функторы полиномиальные)
(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2014-09-21 03:50 pm (UTC)no subject
Date: 2014-09-21 04:42 pm (UTC)Раньше там и Хики красиво выступал, и Киселев бывал, и Мейер.
Ну, правда, было же в этом году некоторое количество хаскельщиков и скальщиков; эти-то по делу выступали.
no subject
Date: 2014-09-21 05:23 pm (UTC)no subject
Date: 2014-09-21 05:50 pm (UTC)no subject
Date: 2014-09-21 05:54 pm (UTC)no subject
Date: 2014-09-21 07:28 pm (UTC)Интересные ссылки:
http://conscientiousprogrammer.com/blog/2014/08/07/understanding-cloure-transducers-through-types/ (см. "the fact that munge actually internally uses a list" - example2)
http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/cjjiasy
no subject
Date: 2014-09-21 08:09 pm (UTC)no subject
Date: 2014-09-22 09:10 am (UTC)no subject
Date: 2014-09-22 10:16 am (UTC)flatmapping :: Foldable f => (a -> f b) -> Transducer b a
и там делается
flatmapping (\x -> [0 .. x])
А можно делать что-нибудь такое:
flatmapping (\x -> Set.insert a (Set.singleton b))
Ведь Set тоже Foldable.
(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2014-09-22 09:26 am (UTC)---
Пока что как следует не разобрался с темой, но вроде бы, грамотно
реализованные на хаскеле трансдюсеры иногда всё-таки могут иметь
некоторый смысл. Например, внутренние промежуточные шаги вычисления могут
запускаться с любыми подходящими структурами данных и вместо списка там
можно вставить нечто более-эффективное-в-таком-то-конкретном-случае.
Интересные ссылки:
http://conscientiousprogrammer.com/blog/2014/08/07/understanding-cloure-transducers-through-types/
(см. "the fact that munge actually internally uses a list" - example2)
http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/cjjiasy
---
Задний ум хаскелиста
Date: 2014-09-22 09:00 am (UTC)no subject
Date: 2014-09-22 01:32 pm (UTC)> transducer: [a] -> [b]
Почему именно transducer: [a] -> [b]? Почему не (Nat -> a) -> (Nat -> b), например?
no subject
Date: 2014-09-23 04:39 am (UTC)no subject
Date: 2014-09-23 09:38 am (UTC)(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2014-09-23 08:23 am (UTC)no subject
Date: 2014-09-23 09:05 am (UTC)no subject
Date: 2014-09-26 09:15 pm (UTC)