Понимание примеров callCC на Haskell
У меня проблемы с пониманием ответов на предыдущий вопрос. Я надеюсь, что объяснение следующего прояснит ситуацию. Следующий пример взят из 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
Но этот пример не компилируется, почему этого нельзя сделать?
Изменить: Рассмотрим пример аналогичный в Схеме. Насколько я знаю, у Схемы не было бы проблем, это правильно? Но почему?
4 ответа
Глядя на ваши примеры в обратном порядке.
Последний пример не проверяет тип из-за бесконечного типа. Глядя на тип 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 должен быть бесконечного типа. Haskell не допускает этого (в общем, по уважительной причине - насколько я могу судить, бесконечный тип здесь будет чем-то вроде этого, предоставьте ему функцию бесконечного порядка в качестве аргумента).
Вы не упоминаете, есть ли что-то, что вас смущает во втором примере, но. Причина, по которой он не печатает "э-э-э...", заключается в том, что ContT действие произведено k ()в отличие от многих ContT Actions не использует следующие вычисления. В этом разница между продолжениями и обычными функциями, которые возвращают ContT действия (отказ от ответственности, любая функция может вернуть ContT действие вроде этого, но в целом). Итак, когда вы следуете k () с печатью, или что-то еще, это не имеет значения, потому что k () просто отбрасывает следующие действия.
Итак, первый пример. Привязка let здесь фактически используется только для того, чтобы возиться с параметрами k, Но тем самым мы избегаем бесконечного типа. По сути, мы делаем некоторую рекурсию в привязке let, которая связана с бесконечным типом, который мы получили раньше. f это немного похоже на версию продолжения с уже сделанной рекурсией.
Тип этой лямбды мы переходим к callCC является Num n => ((n -> ContT r m b, n) -> ContT r m b) -> ContT r m (n -> ContT r m b, n), Это не та же проблема с бесконечным типом, как в вашем последнем примере, потому что мы возились с параметрами. Вы можете выполнить аналогичный трюк без добавления дополнительного параметра, используя привязки let другими способами. Например:
recur :: Monad m => ContT r m (ContT r m ())
recur = callCC $ \k -> let r = k r in r >> return r
Вероятно, это был не очень хорошо объясненный ответ, но основная идея заключается в том, что прямой возврат продолжения создаст проблему бесконечного типа. Используя привязку let для создания некоторой рекурсии внутри лямбды, которую вы передаете callCCВы можете избежать этого.
Как написали другие, последний пример не проверяет тип из-за бесконечного типа.
@augustss предложил другой способ решения этой проблемы:
Вы также можете создать новый тип, чтобы обернуть бесконечный (экви) рекурсивный тип в (изо-) рекурсивный новый тип. - 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 имел в виду.
Пример выполняется в ContT () IO монада, монада, позволяющая продолжения, которые приводят к () и некоторые подняли IO,
type ExM a = ContT () IO a
ContT может быть невероятно запутанной монадой, чтобы работать в ней, но я обнаружил, что уравновешенное рассуждение Хаскелла является мощным инструментом для его распутывания. В оставшейся части этого ответа рассматривается оригинальный пример в несколько этапов, каждый из которых приводится в действие синтаксическими преобразованиями и чистыми переименованиями.
Итак, давайте сначала рассмотрим тип callCC часть - это, в конечном счете, сердце всей этой части кода. Этот кусок отвечает за генерацию странного типа кортежа как его монадического значения.
type ContAndPrev = (Int -> ExM (), Int)
getContAndPrev :: ExM ContAndPrev
getContAndPrev = callCC $ \k -> let f x = k (f, x)
in return (f, 0)
Это можно сделать немного более знакомым, разбив его на (>>=)что именно так будет использоваться в реальном контексте - любой do-блочный десугаринг создаст (>>=) для нас в конце концов.
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, Это секрет понимания Хаскелла callCC---withContAndPrev предоставляется доступ ко всей "остальной части do блок ", который он получает, чтобы выбрать, как использовать.
Давайте проигнорируем фактическую реализацию withContAndPrev и просто посмотрим, сможем ли мы создать поведение, которое мы видели при запуске примера. Это довольно сложно, но то, что мы хотим сделать, это передать в блок способность вызывать себя. Хаскель, будучи таким же ленивым и рекурсивным, мы можем написать это напрямую.
withContAndPrev' :: (ContAndPrev -> ExM ()) -> ExM ()
withContAndPrev' = go 0 where
go n next = next (\i -> go i next, n)
Это все еще что-то вроде рекурсивной головной боли, но может быть легче увидеть, как это работает. Мы берем оставшуюся часть блока do и создаем циклическую конструкцию под названием go, Мы передаем в блок функцию, которая вызывает наш петлитель, 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 что мы в конечном итоге применить значение к. Это рекурсивно трипо, но с ясной точки зрения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 блоки записываются так, что каждая строка получает остаток блока, связанный с ним (>>=) что сразу дает естественное представление о продолжении.
почему необходимо иметь выражение let в callCC для "возврата" продолжения, чтобы его можно было использовать позже
Это точное использование продолжения, то есть захват текущего контекста выполнения и последующее использование этого продолжения захвата для возврата к этому контексту выполнения.
Похоже, вас смущает название функции callCC, который может указывать вам, что он вызывает продолжение, НО фактически он создает продолжение.