Consider the following example in Haskell of a function quux along with the definitions of the continuation monad and callCC.
instance Monad (Cont r) where
return x = cont ($ x)
s >>= f = cont $ \c -> runCont s $ \x -> runCont (f x) c
callCC :: ((a -> Cont r b) -> Cont r a) -> Cont r a
callCC f = cont $ \h -> runCont (f (\a -> cont $ \_ -> h a)) h
quux :: Cont r Int
quux = callCC $ \k -> do
let n = 5
k n
return 25
As I understand this example. The do block can be thought of as
k n >>= \_ -> return 25 ==
cont $ \c -> runCont (k n) $ \x -> runCont ((\_ -> return 25) x) c
And we can see from the definition of k which is \a -> cont $ \_ -> h a that in the above we have \x -> runCont ((\_ -> return 25) x) c being passed into the argument that is ignored with underscore. Ultimately the return 25 is effectively "ignored" because the underscore argument is never used so from lazy evaluation its never evaluated.
So as far as I can tell this implementation of callCC strongly fundamentally depends on lazy evaluation. How would this callCC be done in a strict (non-lazy) functional language?