cont_effect.ml

type (_, _) cont =
    Cont : (('a -> 'r) -> 'r) -> ('r, 'a) cont

let runCont : ('r, 'a) cont -> ('a -> 'r) -> 'r
= fun (Cont f) k -> f k

effect ECont : (* arg *) ('r, 'a) cont -> (* ans *) 'a

(* mutlti-shot 💩 *)
let continue' k x = continue (Obj.clone_continuation k) x

let rec _do : (unit -> ('r, 'a) cont) -> ('r, 'b) cont
  = fun th ->
  match th () with
  | x -> x
  (**
   * effectは項のholeになっている部分の型変数
   * $ECont_'rはGADTsで引き回されているが確定してない型
   * (1) で 'rを$ECont_'rにする
   * (2) で $ECont_'rを'rにする
   **)
  | effect (ECont f (* : ($ECont_'r, effect) cont *)) k (* : effect -> ('r, 'b) cont *) ->
    Cont(fun c (* : 'b -> 'r *) ->
      Obj.magic (*2*) @@ runCont f (fun a (* : effect *) ->
      Obj.magic (*1*) @@ runCont (continue' k a) c)
    )

let cont f = perform @@ ECont (Cont f)
let return x = Cont((|>) x)
let run cont = runCont cont (fun x -> x)
let abort v = cont @@ fun _ -> v

(* 問題ない例 *)
let () =
  let res = run @@ _do @@ fun () ->
    let x = cont @@ fun k -> k 10 * k 10 in
    let y = 20 in
    let z = 30 in
    return @@ x + y + z
  in
  assert (res = 3600)

(* NGな例; ATMしてるんで (int/string) *)
let () =
  (* なんと型検査を通る *)
  let _ : int = run @@ _do @@ fun () ->
    let x = 10 in
    let _ = abort "ouch" in
    return x
  in
  assert false