Как работает " get " в версии CPS Государственной монады?


Я пытаюсь понять продолжение в целом, следуя этому учебнику.

Однако мне трудно понять следующий пример в разделе 2.10:

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

state это типа int я полагаю. Чего я не понимаю, так это типа k. Согласно моему пониманию, k захватывает все вычисления, приходящие впоследствии после get (), и поскольку мы говорим о монаде состояния, k разумно представлять вычисление, которое будет продолжено принимая int, следовательно

k : int => 'a

Но из кода кажется, что это не так, и он берет state во второй раз, что на самом деле означает:

k : int => int => 'a
Но я не понимаю, откуда берется второй, и в каком смысле get относится к типу unit => 'a вместо unit => int => 'a?

По сравнению с фактической реализацией монады состояния, путаница добавляет больше:

newtype StateT s m a = StateT { runStateT :: s -> m (a,s) }
То есть переход состояния представляется в виде функции от состояния к кортежу результата и состояния, которое соответствует моему первому пониманию.

Может ли кто-нибудь дать наводку?

Во-вторых, как я должен реализовать get здесь, используя haskell's Control.Monad.Trans.Cont? У меня возникли проблемы с утешением системы типов.

Обновление

Кажется, я получил второе:

Prelude Control.Monad.Trans.Cont> let get () = shift $ k -> return $ i -> k i i
Но я все еще не понимаю, почему мне нужно дважды применить состояние к продолжению.
1 5

1 ответ:

Вы применяете k к state дважды, потому что первый из них соответствует результату get () (мы хотим, чтобы эффект get получал текущее состояние и возвращал его в результате), а второй соответствует передаче состояния после get (которое, поскольку get не изменяет состояние, является таким же, как состояние до get) к следующему вычислению с сохранением состояния.

Другими словами, поскольку монада состояния является State s a ~ s -> (a, s), ее версия CPS является State s r a ~ s -> (a -> s -> r) -> r, и поэтому для get : State s s, потому что a ~ s, продолжение будет функцией типа s -> s -> r.