与结合的方程式推理
我试图通过减少这个函数来绕过Cont和callCC：
s0 = (flip runContT) return $ do
(k, n) <- callCC $ k -> let f x = k (f, x)
in return (f, 0)
lift $ print n
if n < 3
then k (n+1) >> return ()
else return ()
我设法达到了这一点：
s21 = runContT (let f x = ContT $ _ -> cc (f, x) in ContT ($(f,0))) cc where
cc = ((k,n) -> let
iff = if n < 3 then k (n+1) else ContT ($())
in print n >> runContT iff (_ -> return ()))
在这一点上，我不知道如何处理递归定义f什么是完成这种减少的最佳方式？
您可以按照以下步骤操作。
s21 = runContT (let f x = ContT $ _ -> cc (f, x) in ContT ($(f,0))) cc where
cc = ((k,n) -> let
iff = if n < 3 then k (n+1) else ContT ($())
in print n >> runContT iff (_ -> return ())
-- runContT is the opposite of ContT
s22 = (let f x = ContT $ _ -> cc (f, x) in ($(f,0))) cc
where
cc = ((k,n) -> let
iff = if n < 3 then k (n+1) else ContT ($())
in print n >> runContT iff (_ -> return ())
-- reordering
s23 = ($(f,0)) cc
where
f x = ContT $ _ -> cc (f, x)
cc = ((k,n) -> let
iff = if n < 3 then k (n+1) else ContT ($())
in print n >> runContT iff (_ -> return ())
s24 = cc (f,0)
where ...
-- beta
s25 = let iff = if 0 < 3 then f (0+1) else ContT ($())
in print 0 >> runContT iff (_ -> return ())
where ...
-- if, arithmetics
s26 = let iff = f 1
in print 0 >> runContT iff (_ -> return ())
where ...
s27 = print 0 >> runContT (f 1) (_ -> return ())
where ...
s28 = print 0 >> runContT (ContT $ _ -> cc (f, 1)) (_ -> return ())
where ...
s29 = print 0 >> (_ -> cc (f, 1)) (_ -> return ())
where ...
s30 = print 0 >> cc (f, 1)
where ...
-- repeat all the steps s24..s30
s31 = print 0 >> print 1 >> cc (f, 2)
where ...
-- etc.
s32 = print 0 >> print 1 >> print 2 >> cc (f, 3)
where ...
s33 = print 0 >> print 1 >> print 2 >>
let iff = if 3 < 3 then f (3+1) else ContT ($())
in print 3 >> runContT iff (_ -> return ())
where ...
s34 = print 0 >> print 1 >> print 2 >> print 3 >>
let iff = ContT ($())
in runContT iff (_ -> return ()))
where ...
s35 = print 0 >> print 1 >> print 2 >> print 3 >>
runContT (ContT ($())) (_ -> return ())
where ...
s36 = print 0 >> print 1 >> print 2 >> print 3 >>
($()) (_ -> return ())
where ...
s37 = print 0 >> print 1 >> print 2 >> print 3 >>
return ()