Убогонькая единичка

[deniok]

По поводу сегодняшнего LtU: S has a left inverse

Shin-Cheng Mu типа открыл обратный к S комбинатор:

-- классический коннектор
s :: (a -> b -> c) -> (a -> b) -> a -> c
s = \ f g x -> f x (g x)
-- обратный к нему
s' :: ((a -> b) -> a -> c) -> a -> b -> c
s' = \ f x y -> f (const y) x

Shin-Cheng Mu пишет, что

s' . s = id

и я губу-то и раскатал.

Увы, всё не так сладко. Если вывести тип

(s' . s) :: (a -> b -> c) -> a -> b -> c

то видно, что это - ограниченная версия id с более частным principle type, чем настоящая id. То есть

(s' . s) (++)  == (++)
(s' . s) foldr == foldr

но для арности меньшей 2х это не канает. Жалко.


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

Comments

[lomeo.livejournal.com]

Не надо выводить тип.

У тебя s' . s, а s ожидает первым параметром (a -> b -> c)

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

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

Статью, кстати, я тоже читал, она вроде презентации была сделана, да?

[deni-ok.livejournal.com]

Простой единицы хотел :) Чтобы интересные пары f и g вылезали бы из

s . f . s' = g
f = s' . g . s

А так классы допустимых f и g больно узкие...

[lomeo.livejournal.com]

Вот ты мне скажи - какой в этом практический смысл?

[deni-ok.livejournal.com]

Ну ты прямо VladD2 какой-то :)))

[lomeo.livejournal.com]

А-ха!! :-))

Не-е-е.. Я про другое - я одно время интересовался реверсированием функций, это мой интерес был вызван практической проблемой. Честно говоря, уже не помню какой, но усредняя, это что то вроде универсального лифтинга:

f :: a -> b -- преобразователь
g :: b -> b -- трансформер

lift f g = f' . g . f where f' = reverse f

В этом смысле id как a -> a имеет мало смысла. Вот я и спросил, зачем в реверсивных функциях чистый id :-)

[deni-ok.livejournal.com]

Во! Так для того, чтобы лифтинг был универсальным, не портящим тип трансформера, как раз и надо, чтобы для f :: a -> b тип обратного f' был f' :: b -> a. А требование, чтобы тождественный трансформер id :: b -> b оставался тождественным: f' . id . f = id сразу дает f' . f = id. Настоящему id ;)

[lomeo.livejournal.com]

Где? :-)

Это всего лишь общий полиморфный тип a -> a, который зависит от a из типа f.
А f у нас что? Правильно S-комбинатор, значит и id будет (a->b->c)->(a->b->c)

[deni-ok.livejournal.com]

> Где? :-)

У тебя в примере :-)))

[deni-ok.livejournal.com]

Когда какое-то нетривиальное преобразование дает id, то это потом можно приспособить для нужд народного хозяйства.

В бананах в космосе функция

copy :: Functor f => Rec f -> Rec f
copy (In x) = In (fmap copy x)

тождественный id, на основании чего легким движением руки из неё получается катаморфизм. Меняем применение конструктора In :: f (Rec f) -> Rec f не на себя, а на произвольную phi :: f a -> a и получаем

cata :: Functor f => (f a -> a) -> Rec f -> a
cata phi (In x) = phi (fmap (cata phi) x)

Здесь id задана на Rec f, что позволяет покрыть все рекурсивные типы, для которых можно написать instance Functor.

Я и стал думать, что можно из s и s' вытащить...

[lomeo.livejournal.com]

Я бананы в космосе давно читал, не помню. Обязательно перечитаю, а пока:

copy = cata In, т.е. id твой внутри, на месте его может быть любая функция f a -> a, для рекурсивного f.

Это к аналогиям...

...Честно говоря, я не понимаю, чего ты хочешь :-) Можешь для тупых подробнее объяснить? А то может я вообще о другом говорю?

[deni-ok.livejournal.com]

Да ничего конкретного. Я попытался поиграть с паттерном s' . f . s и сразу увидел что типы результата и f слишком специфические. А в математике такой паттерн часто даёт интересное преобразование - вот я и попробовал.

Офтоп,...

[palm-mute.livejournal.com]

...но кстати о бананах в космосе, попался сегодня замечательный функциональный перл: Data types `a la carte. Фикспойнты функторов применяются в полный рост.

Re: Офтоп,...

[deni-ok.livejournal.com]

Спасибо, посмотрел. Я сейчас тщательно читаю бананы в космосе, конспект
выкладываю. Продолжать?

[palm-mute.livejournal.com]

Конечно, продолжать.

[ilya-portnov.livejournal.com]

Хм. Сейчас поковырялся с этим s' в бестиповой лямбде. Та же самая штука выходит, конечно. Зато (s' . id) оказывается уже обыкновенной обратной функцией к s: (s' . id) . s = id.

[deni-ok.livejournal.com]

Дело не в типизации. В выражении (s' . id) . s, если его развернуть в лямбду, по-прежнему будут три свободные переменные. А в правой части - в id - свободных переменных нет:

id = \x -> x

То есть

id 42              ~> 42
((s' . id) . s) 42 ~> хрена лысого :) 

[ilya-portnov.livejournal.com]

Гм.
s' id = (\f x y.f (const y) x) id = \x y.id (const y) x = \x y.const y x = \x y.y;
(s' id) s = (\x.(\y.y)) s = \y.y
Где ошибка?

[deni-ok.livejournal.com]

А куда композитор делся? Который в Хаскелле (.), в комбинаторной логике B, а в лямбде \f g x -> f (g x)

[deni-ok.livejournal.com]

То есть

s' . id = (.) s' id = (\ f g x -> f (g  x) ) s' id = \x -> s' (id x) = ...

[ilya-portnov.livejournal.com]

Угу, с дополнительным оператором в середине оно конечно всё по-другому будет. Но в лямбде ведь применить одну функцию к другой можно и без всяких "композиторов". Что я и проделал выше. Точку только вот зря там поставил... ;)

[deni-ok.livejournal.com]

Ага, понял

s' id = flip const

Но это не универсально. s' из-за const в своём определении затирает часть информации безвозвратно:

Prelude> :t (s' map)
(s' map) :: [b] -> a -> [a]

Применим к массиву символов и числу

Prelude> (s' map) "abcd" 1
[1,1,1,1]

Опс - символы пропали. С map, к тому же, конструкцию (s' map) s не сделать. Вобщем, о том и речь - неуниверсально это...