Как и почему делает Haskell Продолжение следует работа монады?

Первое, что нужно понять о монаде продолжения, это то, что, по сути, она вообще ничего не делает .Это так!

Основная идея продолжения в целом состоит в том, что оно представляет остальную часть вычисления . Скажем, у нас есть такое выражение: foo (bar x y) z . Теперь извлеките только заключенную в скобки часть, bar x y - это часть общего выражения, но это не просто функция, которую мы можем применить. Вместо этого нам нужно применить функцию к . Итак, мы можем говорить об «остальной части вычислений» в этом случае как о \ a -> foo a z , что мы можем применить к bar x y , чтобы восстановить полную форму.

Бывает, что эта концепция «остальной части вычислений» полезна, но с ней неудобно работать, поскольку это что-то за пределами рассматриваемого подвыражения. Чтобы все работало лучше, мы можем вывернуть все наизнанку: извлечь интересующее нас подвыражение, а затем обернуть его в функцию, которая принимает аргумент, представляющий остальную часть вычисления: \ k -> k (bar xy) .

Эта модифицированная версия дает нам большую гибкость - она ​​не только извлекает подвыражение из своего контекста, но и позволяет нам манипулировать этим внешним контекстом внутри самого подвыражения . Мы можем рассматривать это как своего рода приостановленное вычисление , дающее нам явный контроль над тем, что произойдет дальше.Итак, как мы можем это обобщить? Что ж, подвыражение практически не изменилось, поэтому давайте просто заменим его параметром функции наизнанку, дав нам \ xk -> kx - другими словами, не более чем функция заявление, обратное . Мы могли бы так же легко написать flip ($) или добавить немного экзотического иностранного языка и определить его как оператор |> .

Теперь было бы просто, хотя и утомительно и ужасно запутать, перевести каждую часть выражения в эту форму. К счастью, есть способ получше. Как программисты Haskell, когда мы думаем о построении вычислений в фоновом контексте , следующее, что мы думаем, это , скажем, это монада? И в этом случае ответ да , да, это так.

Чтобы превратить это в монаду, мы начнем с двух основных строительных блоков:

• Для монады m значение типа ma представляет доступ к значению введите a в контексте монады.
• Ядро наших «приостановленных вычислений» - это приложение с перевернутой функцией.

Что значит иметь доступ к чему-то типа a в этом контексте? Это просто означает, что для некоторого значения x :: a мы применили flip ($) к x , получив функцию, которая принимает функцию который принимает аргумент типа a и применяет эту функцию к x .Допустим, у нас есть приостановленное вычисление, содержащее значение типа Bool . Какой тип это дает нам?

> :t flip ($) True
flip ($) True :: (Bool -> b) -> b

Итак, для приостановленных вычислений тип ma работает до (a -> b) -> b ... что, возможно, является препятствием , так как мы уже знали подпись для Cont , но пока пошлите меня.

Здесь интересно отметить, что своего рода «обращение» также применимо к типу монады: Cont b a представляет функцию, которая принимает функцию a -> b и оценивает ее как b . Поскольку продолжение представляет «будущее» вычисления, то тип a в сигнатуре представляет в некотором смысле «прошлое».

Итак, заменив (a -> b) -> b на Cont b a , каков монадический тип для нашего основного строительного блока приложения обратной функции? a -> (a -> b) -> b переводится как a -> Cont ba ... подпись того же типа, что и return и, фактически , это именно то, что есть.

С этого момента все в значительной степени напрямую зависит от типов: по сути, нет разумного способа реализовать >> = , кроме фактической реализации. Но что на самом деле делает ?

Здесь мы возвращаемся к тому, что я сказал изначально: монада продолжения на самом деле не делает много чего. Что-то типа Cont r a тривиально эквивалентно чему-то просто типа a , просто путем предоставления id в качестве аргумента для приостановленного вычисления. Это может вызвать вопрос: если Cont r a является монадой, но преобразование столь тривиально, то не должно ли a само по себе также быть монадой? Конечно, это не работает как есть, поскольку нет конструктора типа, который можно было бы определить как экземпляр Monad , но, скажем, мы добавляем тривиальную оболочку, например data Id a = Id a .Это действительно монада, а именно тождественная монада.

Что делает >> = для монады идентичности? Сигнатура типа Id a -> (a -> Id b) -> Id b , что эквивалентно a -> (a -> b) -> b , что снова просто функциональное приложение. Установив, что Cont ra тривиально эквивалентно Id a , мы можем сделать вывод, что и в этом случае (>> =) - это просто приложение функции .

Конечно, Contra - это сумасшедший перевернутый мир, в котором у всех есть козлиные бородки, так что на самом деле происходит перемешивание вещей запутанным образом, чтобы связать два приостановленных вычисления вместе в новое приостановленное вычисление, но по сути, там на самом деле не происходит ничего необычного! Применение функций к аргументам, ххх, еще один день в жизни функционального программиста.

EDIT: Статья перемещена по ссылке ниже.

Я написал учебник, непосредственно посвященный этой теме, который, я надеюсь, вы найдете полезным. (Оно, безусловно, помогло закрепить мое понимание!) Оно слишком длинное, чтобы удобно уместиться в теме Stack Overflow, поэтому я переместил его в Haskell Wiki.

Пожалуйста, посмотрите: MonadCont под капотом

Вот фибоначчи:

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

Представьте, что у вас есть машина без стека вызовов - он допускает только хвостовую рекурсию. Как выполнить fib на этой машине? Вы можете легко переписать функцию, чтобы она работала в линейном режиме, а не в экспоненциальном времени, но это требует небольшого понимания и не является механическим.

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

Мы заставим fib (n-1) принимать дополнительный параметр, который будет функцией, определяющей, что следует делать после вычисления ее результата, назовем ее x . Конечно, он будет добавлять к нему fib (n-2) . Итак: для вычисления fib n вы вычисляете fib (n-1) после этого, если вы вызываете результат x , вы вычисляете fib (n -2) , после этого, если вы вызываете результат y , вы возвращаете x + y .

Другими словами, вы должны указать:

Как выполнить следующее вычисление: « fib 'nc = вычислить fib n и применить c к результату "?

Ответ заключается в том, что вы делаете следующее:" вычислите fib (n-1) и примените d к результату ", где dx означает «вычислить fib (n-2) и применить e к результату», где ey означает c (x + y) . В коде:

fib' 0 c = c 0
fib' 1 c = c 1
fib' n c = fib' (n-1) d
           where d x = fib' (n-2) e
                 where e y = c (x+y)

Аналогично, мы можем использовать лямбды:

fib' 0 = \c -> c 0
fib' 1 = \c -> c 1
fib' n = \c -> fib' (n-1) $ \x ->
               fib' (n-2) $ \y ->
               c (x+y)

Чтобы получить фактическую идентичность использования Фибоначчи: fib 'n id . Вы можете подумать, что строка fib (n-1) $ ... передает свой результат x следующему.

Последние три строки пахнут блоком do , и на самом деле

fib' 0 = return 0
fib' 1 = return 1
fib' n = do x <- fib' (n-1)
            y <- fib' (n-2)
            return (x+y)

то же самое, вплоть до новых типов, по определению монады Cont . Обратите внимание на различия. В начале есть \ c -> , вместо x <- ... там ... $ \ x -> и c вместо верните .

Попробуйте записать факториал n = n * факториал (n-1) в хвостовом рекурсивном стиле с помощью CPS.

Как работает >> = ? m >> = k эквивалентно

do a <- m
   t <- k a
   return t

Выполняя обратный перевод в том же стиле, что и в fib ', вы получаете

\c -> m $ \a ->
      k a $ \t ->
      c t

упрощение \ t -> ct до c

m >>= k = \c -> m $ \a -> k a c

Добавляя новые типы, вы получаете

m >>= k  = Cont $ \c -> runCont m $ \a -> runCont (k a) c

, который находится вверху этой страницы.Это сложно, но если вы знаете, как переводить между нотацией do и прямым использованием, вам не нужно знать точное определение >> = ! Монада продолжения становится намного понятнее, если вы посмотрите на do-блоки.

Монады и продолжения

Если вы посмотрите на это использование монады списка ...

do x <- [10, 20]
   y <- [3,5]
   return (x+y)

[10,20] >>= \x ->
  [3,5] >>= \y ->
    return (x+y)

([10,20] >>=) $ \x ->
  ([3,5] >>=) $ \y ->
    return (x+y)

это выглядит как продолжение! Фактически, (>> =) , когда вы применяете один аргумент, имеет тип (a -> m b) -> m b , то есть Cont (m b) a . См. Объяснение в sigfpe Мать всех монад . Я бы счел это хорошим продолжением учебника по монаде, хотя, вероятно, это не так.

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