Перейти в Haskell: Может ли кто-нибудь объяснить этот, казалось бы, безумный эффект продолжения монады?

Из этот поток (Control.Monad.Cont fun, 2005), Tomasz Zielonka внедрил функцию (прокомментировал ясным и красивым образом Томасом Йегером). Tomasz принимает аргумент (функцию) тела callCC и возвращает его для последующего использования со следующими двумя определениями:

import Control.Monad.Cont
...
getCC :: MonadCont m => m (m a)
getCC = callCC (\c -> let x = c x in return x)

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

Это также упоминается в Haskellwiki. Используя их, вы можете походить на семантику goto в haskell, которая выглядит действительно круто:

import Control.Monad.Cont

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

main :: IO ()
main = (`runContT` return) $ do
    (x, loopBack) <- getCC' 0
    lift (print x)
    when (x < 10) (loopBack (x + 1))
    lift (putStrLn "finish")

Отпечатывает цифры от 0 до 10.

Вот интересный момент. Я использовал это вместе с писателем Монадой, чтобы решить определенную проблему. Мой код выглядит следующим образом:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}

import Control.Monad.Cont
import Control.Monad.Writer

getCC :: MonadCont m => m (m a)
getCC = callCC (\c -> let x = c x in return x)

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

-- a simple monad transformer stack involving MonadCont and MonadWriter
type APP= WriterT [String] (ContT () IO)

runAPP :: APP a -> IO ()
runAPP a= runContT (runWriterT a) process
      where process (_,w)= do
               putStrLn $ unlines w
               return ()

driver :: Int -> APP ()
driver k = do
   tell [ "The quick brown fox ..." ]
   (x,loop) <- getCC' 0
   collect x
   when (x<k) $ loop (x+1) 

collect :: Int -> APP ()
collect n= tell [ (show n) ] 

main :: IO ()
main = do
   runAPP $ driver 4

Когда вы компилируете и запускаете этот код, вывод:

The quick brown fox ...
4

Числа от нуля до трех проглатываются где-то в глубокой темноте этого примера.

Теперь, в "Реальном мире Хаскелл" О'Салливан, Герцен и Стюарт заявляют

"Штабелирующие монадные трансформаторы аналогичны композиционным функциям. Если мы изменим порядок, в котором мы применяем функции, а затем получаем разные результаты, мы не будем удивлены. Так же и с монадными трансформаторами". (Real World Haskell, 2008, P. 442)

Я придумал идею замены трансформаторов выше:

--replace in the above example
type APP= ContT () (WriterT [String] IO)
...
runAPP a = do
    (_,w) <- runWriterT $ runContT a (return . const ())
    putStrLn $ unlines w

Однако это не будет компилироваться, потому что в Control.Monad.Cont отсутствует определение экземпляра для MonadWriter (вот почему я недавно спросил этот вопрос.)

Добавим экземпляр, оставляющий прослушивание и передачу undefined:

instance (MonadWriter w m) => MonadWriter w (ContT r m) where
  tell = lift . tell
  listen = undefined
  pass = undefined

Добавьте эти строки, скомпилируйте и запустите. Все номера печатаются.

Что произошло в предыдущем примере?

Ответ 1

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

В первом примере вы используете type APP= WriterT [String] (ContT () IO), с IO в качестве базовой монады, затем ContT и, наконец, WriterT. Поэтому, когда вы вызываете loop, состояние записи разворачивается до того, что было при вызове getCC', потому что автор находится выше ContT в стеке монады. Когда вы переключаете ContT и WriterT, теперь продолжение только разматывает монаду ContT, потому что она выше, чем писатель.

ContT - не единственный трансформатор монады, который может вызвать такие проблемы. Здесь пример подобной ситуации с ErrorT

func :: Int -> WriterT [String] (ErrorT String IO) Int
func x = do
  liftIO $ print "start loop"
  tell [show x]
  if x < 4 then func (x+1)
    else throwError "aborted..."

*Main> runErrorT $ runWriterT $ func 0
"start loop"
"start loop"
"start loop"
"start loop"
"start loop"
Left "aborted..."

Даже несмотря на то, что монаде писателя были указаны значения, все они отбрасываются, когда выполняется внутренняя монада ErrorT. Но если мы переключим порядок трансформаторов:

switch :: Int -> ErrorT String (WriterT [String] IO) () 
switch x = do
  liftIO $ print "start loop"
  tell [show x]
  if x < 4 then switch (x+1)
    else throwError "aborted..."

*Main> runWriterT $ runErrorT $ switch 0
"start loop"
"start loop"
"start loop"
"start loop"
"start loop"
(Left "aborted...",["0","1","2","3","4"])

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

Определенно проще рассуждать о ContT, когда он находится в верхней части стека, но иногда полезно уметь разматывать монаду с известной точкой. Например, тип транзакции может быть реализован таким образом.

Ответ 2

Я провел некоторое время, прослеживая это в λ-исчислении. Он создал страницы и страницы дериваций, которые я не буду пытаться воспроизвести здесь, но я немного понял, как работает монод. Ваш тип расширяется следующим образом:

type APP a = WriterT [String] (ContT () IO) a
           = ContT () IO (a,[String])
           = ((a,[String]) -> IO()) -> IO()

Вы также можете развернуть Writer return, >>= и tell вместе с Cont return, >>= и callCC. Трассировка это чрезвычайно утомительно, хотя.

Эффект вызова loop в драйвере - отказаться от нормального продолжения и вместо этого снова вернуться от вызова к getCC'. Это оставленное продолжение содержало код, который добавил бы текущий x в список. Поэтому вместо этого мы повторяем цикл, но теперь x - это следующее число, и только когда мы нажимаем последнее число (и, следовательно, не отказываемся от продолжения), мы собираем список из списка ["The quick brown fox"] и ["4"].

Точно так же, как "Real World Haskell" подчеркивает, что монада IO должна оставаться на дне стека, также важно, чтобы продолжение монады оставалось сверху.