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

[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

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

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