imperative_cps.ml

effect Imperative : (('a -> 'b) -> 'b) -> 'a;;

let runImperative : (unit -> 'ans) -> 'ans =
  fun f -> match f () with
  | x -> x
  | effect (Imperative fx) k ->
    (* fx : ('a -> '_weak_b) -> '_weak_b *)
    (* continue k : 'a -> 'ans *)
    (* Mutlcire OCaml cannot unify '_weak_b and 'ans *)
    (Obj.magic fx) @@ continue k

let imperative e = perform @@ Imperative e
let (<@>) f ek = f @@ imperative ek

let rec map_k f xs k =
  match xs with
  | [] -> k []
  | x :: xs' ->
    f x @@ fun x' ->
    map_k f xs' @@ fun xs'' ->
    k (x' :: xs'')

let () = runImperative @@ fun () ->
  let ls = map_k (fun x k -> k (x + 3)) [2; 3; 5] in
  List.iter (Printf.printf "%d\n") <@> ls

There exists an invalid case due to Obj.magic.

let () =
  let m = runImperative @@ fun () ->
    let ls = fun k -> "5" in
    let () = List.iter (Printf.printf "%d\n") <@> ls in
    0
  in
  assert (m = 0)

The problem above is from the misunderstanding that fx would have weak polymorphic type variable.
Actually fx have some concrete type variable so sometimes Obj.magic crashes runtime.
One solution is that the effect is to be monomorphically typed.

module Imp(T : sig type res end) = struct
  include T

  effect Imperative : (('a -> res) -> res) -> 'a;;

  let runImperative : (unit -> 'ans) -> 'ans =
    fun f -> match f () with
  | x -> x
  | effect (Imperative fx) k ->
    fx @@ continue k

  let imperative e = perform @@ Imperative e
  let (<@>) f ek = f @@ imperative ek
end

let rec map_k f xs k =
  match xs with
  | [] -> k []
  | x :: xs' ->
    f x @@ fun x' ->
    map_k f xs' @@ fun xs'' ->
    k (x' :: xs'')

let () =
  let module I = Imp(struct type res = unit end) in
  let open I in
  runImperative @@ fun () ->
  let ls = map_k (fun x k -> k (x + 3)) [2; 3; 5] in
  List.iter (Printf.printf "%d\n") <@> ls

(* the code below is ILL-typed and safely rejected.
let () =
  let module I = Imp(struct type res = unit end) in
  let open I in
  let m = runImperative @@ fun () ->
    let ls = fun k -> "5" in
    let () = List.iter (Printf.printf "%d\n") <@> ls in
    0
  in
  assert (m = 0)
*)