Почитал про point-free style в haskell wiki, осталось впечатление чёрной магии. Хочу изучить эту тему систематически. Меня интересует, существует ли развитая теория, на которой всё это основано ? Может быть есть алгоритм, позволяющий переходить к point-free форме, или определять что её не существует ? Поиск по форуму навёл меня на комбинаторную логику, но ведь тот же лямбда-бот не раскладывает выражения на примитивы, а использует довольно высокоуровневые функции как map, join и др. Куда копать дальше ?

Здравствуйте, Аноним, Вы писали:

А>Почитал про point-free style в haskell wiki, осталось впечатление чёрной магии. Хочу изучить эту тему систематически. Меня интересует, существует ли развитая теория, на которой всё это основано ? Может быть есть алгоритм, позволяющий переходить к point-free форме, или определять что её не существует ? Поиск по форуму навёл меня на комбинаторную логику, но ведь тот же лямбда-бот не раскладывает выражения на примитивы, а использует довольно высокоуровневые функции как map, join и др. Куда копать дальше ?

http://en.wikipedia.org/wiki/SKI_combinator_calculus

Здравствуйте, <Аноним>, Вы писали:

А>Почитал про point-free style в haskell wiki, осталось впечатление чёрной магии. Хочу изучить эту тему систематически. Меня интересует, существует ли развитая теория, на которой всё это основано ? Может быть есть алгоритм, позволяющий переходить к point-free форме, или определять что её не существует ? Поиск по форуму навёл меня на комбинаторную логику, но ведь тот же лямбда-бот не раскладывает выражения на примитивы, а использует довольно высокоуровневые функции как map, join и др. Куда копать дальше ?

point-free форма существует всегда.
Есть несложный способ преобразовать любое выражение лямбда-исчисления в эквивалентное выражение комбинаторной логики.

-- избавляемся от единственного вхождения переменной
flip f x y = f y x -- используем стандартный комбинатор

(\x -> f x)         = f -- карринг в чистом виде
(\x -> f x y)       = (\x -> (flip f) y x)  -- прибегаем к комбинатору flip
                    = (flip f) y
                    = flip f y
                    = f `flip` y -- удобно записать это в инфиксной форме
(\x -> f x y z...t) = (\x -> (f `flip` y) x z...t) -- а дальше как с гусём (см. выше)
                    ...
                    = f `flip` y `flip` z `flip` ... `flip` t

-- разбираемся со множественным вхождением переменной
twice f x = f x x -- вводим ещё один комбинатор (в Прелюдии его нет)

(\x -> f x x)   = (\x -> (twice f) x) -- прибегаем к комбинатору и затем к каррингу
                = (twice f)
(\x -> f x x x) = (\x -> (f x x) x)
                = (\x -> (twice f) x x)
                = (\x -> (twice (twice f)) x)
                = (twice (twice f))
                = (twice.twice) f) -- (.) - ещё один стандартный комбинатор, но здесь его можно трактовать как сахар

-- если аргумент сам является функцией...
id x = x -- используем стандартный комбинатор

(\x -> x y...z) = (\x -> id x y...z) -- а дальше как с гусём
                = id `flip` y `flip` ... `flip` z

-- наконец, если аргумент не используется вообще
const c x = c -- используем стандартный комбинатор

(\x -> f) = const f

То есть,
1) с помощью id убираем x с первых мест \x->(....(x ...)....) --> \x->(....(id x ...)....)
2) с помощью flip вытаскиваем все x в хвост \x->(..x..x..x..) --> \x->(flip.flip.flip.flip.....) x x x
3) с помощью twice оставляем единственное вхождение \x->(....) x x x --> \x->(twice.twice.twice) (....) x
4) если вхождений вообще нет — делаем одно фиктивное \x->(....) --> \x->const(....) x
4) используем карринг \x->(....)x --> (....)

Таким образом, с помощью 4 комбинаторов id, const, flip, twice мы научились приводить к point-free виду любые лямбда-термы.
В комбинаторной логике им соответствуют
id = I
const = K
flip = C
twice = W

Дальше берём любой понравившийся нам базис комбинаторов (базис — это то, через что можно выразить всё остальное). Подобно тому, как в булевой логике есть базисы AND-OR-NOT, и даже NAND и NOR.

Традиционно используется базис SKI, хотя он избыточен — I можно выразить в базисе SK. Но это, скорее, академические изыски, чем практика.
В данном случае удобнее сразу взять базис BKCW, разработанный, кстати, Хаскеллом Карри.