слово о трансдюсерах
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-26 03:16 pm (UTC)Интересно, как выглядит конструктивное доказательство того, что это не функтор.
no subject
Date: 2014-09-26 03:26 pm (UTC)а, например, a->x - функтор. Но это же XA, так что, пока что полиномиально.
Но и (x->a)->x - функтор. Но каким образом XAX полином - не знаю. Может, я не понял чего, и не все функторы полиномиальные.
no subject
Date: 2014-09-26 03:54 pm (UTC)no subject
Date: 2014-09-26 04:07 pm (UTC)(функториальность, по-моему, доказывается построением элемента типа:
(a b c : Set)->(F : Set->Set)->(fmap : {a b : Set} (a->b)->F a->F b)->(f : a->b)->(g : b->c)->(fmap (g . f) == (fmap g) . (fmap f))
no subject
Date: 2014-09-26 04:13 pm (UTC)data Functor {F : Set -> Set} (fmap : {a b : Set} -> (a -> b) -> F a -> F b) : Set where fun : ((a b c : Set) -> (f : a -> b) -> (g : b -> c) -> (fmap (g . f)) == ((fmap g) . (fmap f))) -> Functor fmapIf \A -> F X = X -> A, then \A -> Functor {F} _ = \A -> Functor {\X -> (X -> A)} ((a->b)->(a->A)->(b->A))
Since this should work for any a, it should even work for a = A. In that case the existence of Functor ((A->b)->(A->A)->(b->A)) is equivalent to the ability to build the inverse of an arbitrary function (A->b). (Let's see if it's actually the inverse; but even weaker statement of existence of a function in opposite direction is already important, as below)
For example, the existence of such a Functor for A = ⊥ would mean that (fmap ⊥-elim id) is the proof that all types are empty (for any type a there would exist an arrow a→⊥). So F can't be a functor for arbitrary A.
It seems it doesn't even need to be a inverse. Just an arrow in the opposite direction. This looks like an Axiom of Choice.
So, the outcome so far is two-fold: X->A is not a Functor for arbitrary type A, because otherwise it is possible to prove all types are empty; and being able to build an arrow A->X for all X is equivalent to having an Axiom of Choice. Since it is a axiom, we can either accept it, or reject it - can't prove that it's impossible.