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х это не канает. Жалко.


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