Один аппликативный функтор как вычислительный базис

[thedeemon]

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

import Control.Applicative
main = print $ answer succ 0  where
  one = pure <*> (pure :: a -> b -> a)
  inc = (<*>) ((<*>) <$> pure)
  mul = (<*>) <$> pure
  h = mul <*> inc
  answer = h . h . h $ one

Аппликативный функтор характеризуется наличием двух функций с определенными свойствами:

class Functor f => Applicative f where  
  pure :: a -> f a                   -- Lift a value.  
  (<*>) :: f (a -> b) -> f a -> f b  -- Sequential application.

Фишка в том, что для ((->) a) эти две функции - комбинаторы K и S!

instance Applicative ((->) a) where
  pure = const     -- \x . \y . x
  (<*>) f g x = f x (g x)

А мы знаем, что через S и K можно выразить любую лямбда-функцию, а значит и любую вычислимую функцию. Возьмем, например, функцию
h(x) = x * (x + 1)
Она интересна тем, что использует только умножение и инкремент, и будучи трижды применена к единице, дает 42. Для арифметики на лямбдах задействуем числа Черча. Число n там представляется функцией, которая берет другую функцию и ее аргумент, и применяет ту функцию n раз. Так, единица применяет данную функцию f один раз:
one f x = f x
Чтобы увеличить n на 1, нужно применить f на один раз больше, чем это делает n:
inc n f x = f (n f x)
Умножение a на b делается применением b a раз:
mul a b f x = a (b f) x
(x тут можно "сократить" и не писать)
Тогда h будет выглядеть как
h x = mul x (inc x)

Теперь возьмем комбинаторный базис:
S x y z = (x z) (y z)
K x y = x
Пользуясь простым алгоритмом конверсии, наши арифметические функции можно выразить через S и K:
one = S K K
inc = S (S (K S) K)
mul = S (K S) K
h = S mul inc

Теперь осталось лишь вспомнить, что K = pure, S = <*>, а
pure x <*> y = x <$> y
Подставив их вместо S и K, получим программу выше.
Представляете, какие открываются горизонты? Я тоже нет. Разве что обфускатор можно написать. :)

Comments

[diam-2003.livejournal.com]

Не, две функции - это уже скучно.
Одноточечный универсальный базис слабо =) ?

[codedot.livejournal.com]

X = λx.x K S K, например, — один из одноточечных базисов комбинаторной логики. (В нем K = X X X, а S = X (X X).)

[lomeo.livejournal.com]

Клёво, спасибо!

[thedeemon.livejournal.com]

Легко, но не так весело. Просто тут приколько совпал базис с известным стандартным интерфейсом.

[codedot.livejournal.com]

Уж век как этот горизонт открыт, а все никто представить не может :)

[nealar.livejournal.com]

Вот только я дочитал про ATS! И сразу новую мозгодробилку подкинули.

[kodt-rsdn.livejournal.com]

Вместо обфускатора можно написать транслятор в унлямбду или с унлямбды. Там как раз SKI используется.

[sorhed.livejournal.com]

Как нет применения? Можно было бы отлично писать зомбей на прошлом ICFPC. :)

[thedeemon.livejournal.com]

ну так скучно в деревне :)

[thedeemon.livejournal.com]

да, транслятор в унлямбду - очень нужная в хозяйстве вещь! :)

[thedeemon.livejournal.com]

Просто в таком богатом языке-хосте это хм... Почти столь же удобно и нужно, как вычисления на шаблонах в С++. :)

[thedeemon.livejournal.com]

Этим занимаются специалисты, я в ананасах ничего не понимаю. :)

[akuklev.livejournal.com]

Это нифига не случайное совпадение, а собствено базовая мотивация интерфейса аппликативных функторов.

[thedeemon.livejournal.com]

Оно ж не для каждого ап.функтора справедливо. Одно дело засунуть в функтор и применить какую-то свою функцию, другое - как здесь - реализовать функцию на самом интерфейсе ап.функтора.

[akuklev.livejournal.com]

> Оно ж не для каждого ап.функтора справедливо.
Аппликативный функтор это функтор, "переносящий" лямбда-исчисление из одной категории в другую, так его определили. Метод "переноса" заключается в том, что мы можем переписать лямбда-выражения через S и K комбинаторы и заменить их на <*> и pure. В исходной работе по аппликатианым функторам (“Applicative programming with effects”, Conor McBride, Ross Paterson)
для <*> и pure используются обозначения \mathbb{S} и \mathbb{K}, и написано прямым текстом: «This class generalises S and K from threading an environment to threading an effect in general».

У аппликативных функторов возможен и _другой_ интерфейс, связь которого с комбинаторной логикой менее очевидна; в той же работе объясняется, что аппликативный функтор это strong lax monoidal functor, т.е. вместо S и K его можно снабжать тензорным произведением и тензорной силой, эффект будет тот же. Можно кстати сделать интерфейс через одноточечный базис комбинаторной логики навроде X; но неудобно.

[thedeemon.livejournal.com]

спасибо, помедитирую над этим

[sassa-nf.livejournal.com]

также,

inc = S mul

а посему, h = inc inc

как же так?!

[thedeemon.livejournal.com]

>inc = S mul

С чего бы?

[sassa-nf.livejournal.com]

Удивительно, но факт! ты подставь?

inc = S (S (K S) K)
mul =    S (K S) K

Я тоже как-то не мог понять, и в виде mul a b f x = a (b f) x этого не видно.

Зато раз x можно "сократить", то выходит mul a b x = a (b x) (даже больше: mul = (.)), а inc n f x = f ((n f) x) = mul f (n f) x

Полиморфизм!

[thedeemon.livejournal.com]

А вообще да, действительно.

Prelude> let h = inc inc
Prelude> (h . h . h $ one) (+1) 0
42

Хотя типы ghci выводит разные для inc и s mul.

[sassa-nf.livejournal.com]

думаю, ещё сильно зависит от того, как mul задать. Если задать слишком строго (т.е. не сокращать x в типе), то хотя всё равно реализация mul = (.), но это будет специализация (.) для функций вида (a->b)->(c->d) и не получится использовать mul в inc, т.к. в inc используется версия mul без x (версия (.) для функций вида a->b).

[aruslan.livejournal.com]

спасибо за референс