Rational reasoning with node binding

Question

I am trying to wrap my head around Cont and callCC by reducing this function:

s0 = (flip runContT) return $ do (k, n) <- callCC $ \k -> let fx = k (f, x) in return (f, 0) lift $ print n if n < 3 then k (n+1) >> return () else return () 

I managed to achieve this goal:

 s21 = runContT (let fx = 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 ())) 

And at the moment I have no idea what to do with the recursive definition f What is the best way to complete this reduction?

Answer 1

You can proceed as follows.

 s21 = runContT (let fx = 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 fx = 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 fx = 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 ()