How does `get` work in the CPS version of the State monad?

Question

I am trying to understand continuation in general following this tutorial.

However, I am having difficulties to understand following example in section 2.10:

# let get () =
    shift (fun k -> fun state -> k state state) ;;
get : unit => ’a = <fun>

state is of type int I suppose. What I don't get is the type of k. According to my understanding, k captures all computation comes subsequently after get (), and since we are talking about a state monad, k is reasonable to represent a computation that will be continued by taking an int, hence

k : int => 'a

but from the code, it doesn't seem to do that and it takes state for a second time, which actually implies:

k : int => int => 'a

but I don't get where the second one is coming from, and in which sense get is of type unit => 'a instead of unit => int => 'a?

Compared to the actual state monad implementation, the confusion adds more:

newtype StateT s m a = StateT { runStateT :: s -> m (a,s) }

i.e. state transition is represented as a function from state to a tuple of result and state, which matches my first understanding.

Can anyone give a lead?

Secondly, how am I supposed to implement get here using Haskell's Control.Monad.Trans.Cont? I am having problems comforting the type system.

---

UPDATE

It seems I got the second one:

Prelude Control.Monad.Trans.Cont> let get () = shift $ \k -> return $ \i -> k i i

But I still don't get why I need to apply the state twice to the continuation.

Answer 1

You apply k on state twice because the first one corresponds to the result of get () (we want get's effect to be retrieving the current state and returning it as the result) and the second one corresponds to passing the state after the get (which, because get doesn't change the state, is the same as the state before the get) to the next stateful computation.

In other words, since the state monad is State s a ~ s -> (a, s), its CPS version is State s r a ~ s -> (a -> s -> r) -> r, and so for get : State s s, because a ~ s, the continuation will be a function of type s -> s -> r.