Понимание Haskell callCC примеры

Question

У меня возникли проблемы с пониманием ответов на предыдущий question. Я надеюсь, что объяснение следующего прояснит ситуацию. Следующий пример взят из fpcomplete

import Control.Monad.Trans.Class 
import Control.Monad.Trans.Cont 

main = flip runContT return $ do 
    lift $ putStrLn "alpha" 
    (k, num) <- callCC $ \k -> let f x = k (f, x) 
           in return (f, 0) 
    lift $ putStrLn "beta" 
    lift $ putStrLn "gamma" 
    if num < 5 
     then k (num + 1) >> return() 
     else lift $ print num 

Выход

alpha 
beta 
gamma 
beta 
gamma 
beta 
gamma 
beta 
gamma 
beta 
gamma 
beta 
gamma 
5 

Я думаю, я понимаю, как работает этот пример, но зачем это нужно иметь let выражение в callCC для «возврата» продолжение, с тем чтобы его можно было использовать позже. Поэтому я попытался прямо вернуться к продолжению, выполнив следующий простой пример и изменив его.

import Control.Monad.Trans.Class 
import Control.Monad.Trans.Cont 

main = flip runContT return $ do 
    lift $ putStrLn "alpha" 
    callCC $ \k -> do 
     k() 
     lift $ putStrLn "uh oh..." 
    lift $ putStrLn "beta" 
    lift $ putStrLn "gamma" 

Печатается

alpha 
beta 
gamma 

И я изменил его к следующему

import Control.Monad.Trans.Class 
import Control.Monad.Trans.Cont 

main = flip runContT return $ do 
    lift $ putStrLn "alpha" 
    f <- callCC $ \k -> do 
     lift $ putStrLn "uh oh..." 
     return k 
    lift $ putStrLn "beta" 
    lift $ putStrLn "gamma" 

Идея заключалась в том, что продолжение будет получить возвращается как f и быть неиспользованными в данном тестовом примере, который я будет ожидать отпечаток

uh oh... 
beta 
gamma 

Но этот пример не компилируется, почему это невозможно?

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

Answer 1

Посмотрите на свои примеры в обратный заказ.

Последний пример не проверяет тип из-за бесконечного типа. Рассматривая тип callCC, это ((a -> ContT r m b) -> ContT r m a) -> ContT r m a. Если мы попытаемся вернуть продолжение, мы возвращаем что-то типа ContT r m (a -> ContT r m b). Это означает, что мы получаем ограничение равенства типов a ~ (a -> ContT r m b), что означает, что a должен быть бесконечным. Хаскелл этого не допускает (в общем, по уважительной причине - насколько я могу сказать, что бесконечный тип здесь был бы чем-то вроде этого, снабдить его бесконечной функцией порядка в качестве аргумента).

Вы не упомянули, есть ли что-то, о чем вы смутили во втором примере, но. Причина, по которой он не печатает «uh oh ...», заключается в том, что действие ContT, произведенное k(), в отличие от многих действий ContT делает не, используйте следующее вычисление.В этом разница между продолжениями и просто нормальными функциями, которые возвращают ContT действия (отказ от ответственности, любая функция может вернуть ContT действие вроде этого, но в целом). Итак, когда вы следуете за k() с помощью печати или чего-либо еще, это не имеет значения, потому что k() просто отбрасывает следующие действия.

Итак, первый пример. Связывание let здесь фактически используется только для того, чтобы обходиться с параметрами до k. Но тем самым мы избегаем бесконечного типа. Фактически, мы выполняем некоторую рекурсию в связывании let, которая связана с бесконечным типом, который мы получили раньше. f немного напоминает версию продолжения с уже выполненной рекурсией.

Тип этой лямбда мы переходим на callCC is Num n => ((n -> ContT r m b, n) -> ContT r m b) -> ContT r m (n -> ContT r m b, n). Это не имеет той же проблемы с бесконечным типом, что и в вашем последнем примере, потому что мы перепутали параметры. Вы можете выполнить подобный трюк без добавления дополнительного параметра, используя другие привязки. Например:

recur :: Monad m => ContT r m (ContT r m()) 
recur = callCC $ \k -> let r = k r in r >> return r 

Это, вероятно, был не очень хорошо объяснил ответ, но основная идея заключается в том, что возвращение продолжения непосредственно создаст бесконечную задачу типа. Используя привязку let для создания некоторой рекурсии внутри лямбды, вы переходите к callCC, вы можете избежать этого.

Answer 2

почему необходимо иметь выражение впустить в callCC «вернуться» продолжение, так что она может быть использована в дальнейшем

То точное использование продолжения, т.е. захвата тока контекст выполнения, а затем использовать это продолжение продолжения, чтобы вернуться к этому контексту выполнения.

кажется, что вы запутались именем функции callCC, которая может быть указывающим вам, что это вызовом продолжения но на самом деле он создает продолжение.

Answer 3

Пример исполняется в монаде ContT() IO, Монаде разрешает продолжение, которое приводит к (), а некоторые подняты IO.

type ExM a = ContT() IO a 

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

Итак, давайте сначала рассмотрим тип части callCC - это, в конечном счете, сердце всей этой части кода. Этот кусок отвечает за создание странного типа кортежа в качестве его монадического значения.

type ContAndPrev = (Int -> ExM(), Int) 

getContAndPrev :: ExM ContAndPrev 
getContAndPrev = callCC $ \k -> let f x = k (f, x) 
           in return (f, 0) 

Это может быть немного больше знакомы секционированиями его с (>>=), что именно то, как он будет использоваться в реальном контекстуальном любом do -блока desugaring создаст (>>=) для нас в конце концов.

withContAndPrev :: (ContAndPrev -> ExM()) -> ExM() 
withContAndPrev go = getContAndPrev >>= go 

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

flip runContT return $ do 
    lift (putStrLn "alpha") 
    withContAndPrev $ \(k, num) -> do 
    lift $ putStrLn "beta" 
    lift $ putStrLn "gamma" 
    if num < 5 
     then k (num + 1) >> return() 
     else lift $ print num 

Обратите внимание, что это чисто синтаксическое преобразование. Код идентичен исходному примеру, но он подчеркивает существование этого отступованного блока под withContAndPrev. Это секрет понимания Haskell callCC --- withContAndPrev предоставляется доступ ко всему «остатку блока do», который он получает, чтобы выбрать, как использовать.

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

withContAndPrev' :: (ContAndPrev -> ExM()) -> ExM() 
withContAndPrev' = go 0 where 
    go n next = next (\i -> go i next, n) 

Это все еще что-то вроде рекурсивной головной боли, но было бы легче увидеть, как это работает. Мы берем оставшуюся часть блока do и создаем петлевую конструкцию под названием go. Мы передаем в блок функцию, которая вызывает наш looper, go, с новым целочисленным аргументом и возвращает предыдущий.

Мы можем немного развернуть этот код, сделав еще несколько синтаксических изменений исходного кода.

maybeCont :: ContAndPrev -> ExM() 
maybeCont k n | n < 5  = k (num + 1) 
       | otherwise = lift (print n) 

bg :: ExM() 
bg = lift $ putStrLn "beta" >> putStrLn "gamma" 

flip runContT return $ do 
    lift (putStrLn "alpha") 
    withContAndPrev' $ \(k, num) -> bg >> maybeCont k num 

И теперь мы можем рассмотреть, как это выглядит, когда betaGam >> maybeCont k num получает передается в withContAndPrev.

let go n next = next (\i -> go i next, n) 
    next  = \(k, num) -> bg >> maybeCont k num 
in 
    go 0 next 
    (\(k, num) -> betaGam >> maybeCont k num) (\i -> go i next, 0) 
    bg >> maybeCont (\i -> go i next) 0 
    bg >> (\(k, num) -> betaGam >> maybeCont k num) (\i -> go i next, 1) 
    bg >> bg >> maybeCont (\i -> go i next) 1 
    bg >> bg >> (\(k, num) -> betaGam >> maybeCont k num) (\i -> go i next, 2) 
    bg >> bg >> bg >> maybeCont (\i -> go i next) 2 
    bg >> bg >> bg >> bg >> maybeCont (\i -> go i next) 3 
    bg >> bg >> bg >> bg >> bg >> maybeCont (\i -> go i next) 4 
    bg >> bg >> bg >> bg >> bg >> bg >> maybeCont (\i -> go i next) 5 
    bg >> bg >> bg >> bg >> bg >> bg >> lift (print 5) 

Таким образом, наша фальшивая реализация воссоздает поведение исходного цикла. Может быть немного более ясно, как наше поддельное поведение достигает этого, связывая рекурсивный узел, используя «остаток блока do», который он получает в качестве аргумента.

Вооруженные этими знаниями, мы можем подробнее рассмотреть callCC. Мы снова получим прибыль, предварительно изучив его в своей предварительной форме. Это очень просто, если странно, в этой форме.

withCC gen block = callCC gen >>= block 
withCC gen block = block (gen block) 

Другими словами, мы используем аргумент callCC, gen, чтобы сформировать возвращаемое значение callCC, но мы переходим в gen само продолжение block, что мы в конечном итоге применяя значение. Он рекурсивно триппирован, но denotationally clear - callCC действительно «вызывает этот блок с текущим продолжением».

withCC (\k -> let f x = k (f, x) 
       in return (f, 0)) next 
next (let f x = next (f, x) in return (f, 0)) 

Фактические детали реализации callCC немного более сложной задачей, так как они требуют, чтобы мы нашли способ определения callCC из семантики (callCC >>=), но это в основном игнорируемые. В конце дня мы получаем прибыль от того, что блоки do записываются так, что каждая строка получает оставшуюся часть связанного с ним блока с (>>=), что обеспечивает естественное представление о продолжении немедленно.

Answer 4

Как уже писали другие, последний пример не описывает тип из-за бесконечного типа.

@augustss предложил другой способ решения этой проблемы:

Вы также можете сделать NewType завернуть бесконечный (нарна) рекурсивный типа в (изо-) рекурсивный Newtype. - augustss 12 декабря '13 в 12:50

Вот мое взятие на него:

import Control.Monad.Trans.Cont 
import Control.Monad.Trans.Class 

data Mu t = In { out :: t (Mu t) } 

newtype C' b a = C' { unC' :: a -> b } 
type C b = Mu (C' b) 

unfold = unC' . out 
fold = In . C' 

setjmp = callCC $ (\c -> return $ fold c) 
jump l = unfold l l 

test :: ContT() IO() 
test = do 
    lift $ putStrLn "Start" 
    l <- setjmp 
    lift $ putStrLn "x" 
    jump l 

main = runContT test return 

Я думаю, что это то, что @augustss имел в виду.