Продолжения

За последние 2 дня жизнь меня буквально макает носом в какие то Continuations.
В целом, я более-менее понимал в чем суть, но некоторые вопросы я не смог ответить, а именно:
1) Что такое Продолжение
2) Чем это отличается от callback и Future в JS?
3) В чем профиты?
4) Как это завязано на Монады?
5) Как это завязано на теоркат и логику (завязано ли?)?

Это вопросы, на которые я пытаюсь ответить.
Впервые лично я столкнулся с продолжениями в книге Харпера “Основания языков программирования”. Книжка мне не очень зашла если честно. Сама концепция была предложена еще в Алголе-60, а потом широко популяризирована благодаря SICP.
Первый раз я пожалел, что не особо понимаю Лисп (Собственно, только там они явнее всего опрееляются). Как следует из английской Википедии, идея продолжений неожиданно появляется в самых различных сферах.

1) Что такое Продолжение

Собсна, определение из (2):

call-with-current-continuation (обычно сокращенно обозначается как call/cc) — функция одного аргумента, который мы будем называть получатель (receiver). Получатель также должен быть функцией одного аргумента, называемого продолжение.

call/cc формирует продолжение, определяя контекст выражения (call/cc receiver) и обрамляя его в функцию выхода escaper, описанную в предыдущем разделе. Затем полученное продолжение передается в качестве аргумента получателю.

Широко известная в узких кругах функция, просто возвращающая свой аргумент:

id :: a -> a
id x = x

Ее же вариант на Хаскелле, являющийся продолжением:

idCPS :: p -> (p -> q) -> q
idCPS x k = k x

Попробуем написать что-то более полезное, и применим его:

f::Int -> (Int -> r) -> r
f x k = k (x * x)
f 2 print :: IO()
f 3 (+1) :: Int

2) Чем это отличается от callback и Future в JS?

Нужно разобраться, что происходит. С точки зрения джаваскрипта разница такая.

Вот — просто функция с коллбеком, которая распоряжается им как хочет, и, что самое главное, возвращает управление в точку вызова.

function f(x, callback){
callback(x);
var y = x*x;
callback(y);
return y;
}

Вот это более идиоматическая тема, коллбек вызывается в конце, нет return-а (Правда, он и не нужен, тут я немножко в замешательстве, что считать возвратом управления)

function f(x, callback){
var y = x*x;
callback(y);
}

3) Профиты

С точки зрения джаваскрипта есть как минимум один. До того, как появились async/await никак нельзя было просто подождать функцию. По видимому для выстраивания цепочек асинхронных вызовов использовались именно продолжения.

В небезызвестном языке C# слова async/await выражают не что иное, как Продолжения. Они говорят: “Пометь остаток метода как продолжение, а потом немедленно вернись в вызвавший тебя метод. Задание вызовет продолжение, когда закончится”

С точки зрения компиляции здесь преимущество в том, что все CPS — функции находятся в хвостовой рекурсивной форме. Как известно, существуют способы оптимизации хвостовой рекурсии, благодаря которым невозможно переполнение стека вызовов.
Например, есть язык программирования CHICKEN Scheme(3), который преобразовывает всю программу в одну цепочку CPS функций, которые транслируются в ничего не возвращающие сишные функции. Используется особый стек вызовов и куча, которые образуют 2 ступени сборки мусора. При каждом вызове продолжения проверяетя, не переполнен стек живыми данными. Если стек переполнен, то его содержимое отгружается в кучу.
Для желающих углубиться в сабж , есть книга (4), с примерами на ламповой ML-ке.

4) Монада Cont

Собственно, как гласит народная мудрость, если что то выглядит как монада, бегает как монада, ест как монада, то это монада. Оптимизированная версия имеется в модуле Control.Monad.Cont, подробное описание приведено в (5). Определение типов может быть выглядеть странно, особенно для Аппликатива, но ничего сверхестественного в нем нет.

newtype Cont r a = Cont { runCont :: (a -> r) -> r }
instance Functor (Cont c) where
fmap f (Cont c) = Cont $ \k -> c (\x -> k (f x))
instance Applicative (Cont c) where
Cont cf <*> Cont cx = Cont \k−>cf(\fn−>cx(\x−>k(fnx)))purex=Cont\k−>cf(\fn−>cx(\x−>k(fnx)))purex=Cont \k -> cf (\fn -> cx (\x -> k (fn x))) pure x = Cont \k -> k x
instance Monad (Cont r) where
return a = Cont (a)f>>=g=Conta)f>>=g=Cont a) f >>= g = Cont \k -> runCont f (\a -> runCont (g a) k)
f :: Int -> Cont r Int
f x = Cont $ \c -> c (x * 2)
g :: Int -> Cont r Int
g x = Cont $ \c -> c (x + 10)
h :: Int -> Cont r Int
h x = if x == 5 then f x else g x
--Наша цепочка вычислений. Мы могли бы например связать их в другом месте
compos :: Cont r Int
compos = return 5 >>= g >>= f
--Обратите внимание, эта функция никогда не оборачивается в Cont
finale :: Show a => a -> String
finale x = “Done: “ ++ show(x)
--Поставил скобочку для наглядности
main = print $ (runCont compos) finale

5) Логика, теория категорий, язык

Продолжения это пример того как работает лемма Йонеды (6). Потом расскажу что там как. Также есть статья про то, как это работает в языке (7). Проще всего в логике. Как известно, у конструктивной логики, в отличие от традиционной, есть 2 особенности. Во-первых, закон исключенного третьего (P || !P == 1) не является базовой аксиомой. Во-вторых, теоремы пруфаются конкретными примерами. Чтобы доказать, что “Существует такой х, который обладает свойством F(x)”, ты должен сконструировать, принести и выставить на всеобщее обозрение хотя бы один такой х.
Напомню также вкратце одну из любимых тем функциональных программистов — изоморфизм Карри-Говарда. На самом деле, это просто настоящая конфетка и годная тема для доказательства теорем (Coq, Agda). Он ставит в соответствие термам(в нашем случае — декларациям функций) доказательство высказывания, а в соответствие типу терма(типу функции) — то высказывание, которое мы доказываем. Таким образом, чтобы что то “доказать”” с помощью Хаскеля нам нужно придумать соответствующий тип и подходящую функцию.
И, наконец, закон Пирса : (((P -> Q) -> Q) -> P). Выглядит довольно знакомо. Выглядит в точности, как тип простейшей функции с продолжением. Это очень удобное средства “встраивания” классической логики в конструктивистсткую. Если в какой-то формальной системе закон пирса выполняется, то выполняется и закон исключенного третьего. В (8) приведено доказательство. Получается, Продолжения могут выступать в качестве доказательства “преобразования двойного отрицания”(9): Если у нас есть на руках классическое доказательство высказывания Р, то мы можем получить бесплатное конструктивное доказательство (!!Р)

(1) Здесь что то будет
(2) http://fprog.ru/lib/ferguson-dwight-call-cc-patterns/
(3) http://wiki.call-cc.org/chicken-compilation-process
(4) https://www.amazon.com/gp/product/052103311X/ref=as_li_ss_tl?ie=UTF8&tag=ucmbread-20&linkCode=as2&camp=1789&creative=390957&creativeASIN=052103311X
(5) https://wiki.haskell.org/MonadCont_under_the_hood
(6) https://golem.ph.utexas.edu/category/2008/01/the_continuation_passing_trans.html
(7) http://www.cs.bham.ac.uk/~hxt/cw04/barker.pdf
(8) http://math.stackexchange.com/questions/447098/why-peirces-law-implies-law-of-excluded-middle
(9) https://en.wikipedia.org/wiki/Double-negation_translation

One clap, two clap, three clap, forty?

By clapping more or less, you can signal to us which stories really stand out.