cps-defunc-embed.ml

(* 0. recursive impl **************************************************)

let sum l =
  let rec sum = function
    | x :: xs -> sum xs + x
    | [] -> 0
  in
  sum l

(* 1. continuation passing style **************************************)

let sum l =
  let rec sum k = function
    | x :: xs -> sum (fun y -> k (y + x)) xs
    | [] -> k 0
  in
  sum (fun y -> y) l

(* 2. defunctionalization *********************************************)

type k = K0 | K1 of k * int

let sum l =
  let rec sum k = function
    | x :: xs -> sum (K1(k,x)) xs
    | [] -> call 0 k
  and call y = function
    | K0 -> y
    | K1(k, x) -> call (y + x) k
  in
  sum K0 l

(* 3. rewrite 'call' using a denotational semantics for 'k' ***********)

let sum l =
  let rec sum k = function
    | x :: xs -> sum (K1(k,x)) xs
    | [] -> call 0 k
  and call y k = y + denote k
  (* PROOF: call y k == y + denote k
   * --------------------------------
   * 1. call y K0
   *    == y                    [definition of call]
   *    == y + 0                [+ has identity 0]
   *    == y + denote K0        [definition of denote]
   * 2. call y (K1(k,x))
   *    == call (y + x) k       [definition of call]
   *    == (y + x) + denote k   [induction]
   *    == y + (x + denote k)   [+ is associative]
   *    == y + denote (K1(k,x)) [definition of denote]
   *)
  and denote = function
    | K0 -> 0
    | K1(k, x) -> x + denote k
  in
  sum K0 l

(* 4. implement k by a shallow embedding of its semantics *************)

let denote k = k
let k0 = 0
let k1(k,x) = x + denote k

let sum l =
  let rec sum k = function
    | x :: xs -> sum (k1(k,x)) xs
    | [] -> call 0 k
  and call y k = y + denote k
  in
  sum k0 l

(* 5. clean up by inlining ********************************************)

let sum l =
  let rec sum k = function
    | x :: xs -> sum (x + k) xs
    | [] -> 0 + k
  in
  sum 0 l

(* tail recursive :) *)