Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to convert CPS-style gcd computation to use the Continuation Monad

Let us consider the following implementation of the Continuation monad, for CPS-style computations yielding and integer:

module Cont : sig
  type 'a t = ('a -> int) -> int
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val callCC: (('a -> 'b t) -> 'a t) -> 'a t
end = struct
  type 'a t = ('a -> int) -> int

  let return x =
    fun cont -> cont x

  let bind m f =
    fun cont -> m (fun x -> (f x) cont)

  let callCC k =
    fun cont -> k (fun x -> (fun _ -> cont x)) cont
end

How can we rewrite the CPS-style implementation of gcd computation (see How to memoize recursive functions?) and especially the memoization to take advantage of the Cont monad?

After defining

let gcd_cont k (a,b) =
  let (q, r) = (a / b, a mod b) in
  if r = 0 then Cont.return b else k (b,r)

I tried to use the type solver to give me cue about the type that the memoization function should have:

# let gcd memo ((a,b):int * int) =
  Cont.callCC (memo gcd_cont (a,b)) (fun x -> x)
;;
    val gcd :
  (((int * int -> int Cont.t) -> int * int -> int Cont.t) ->
   int * int -> (int -> 'a Cont.t) -> int Cont.t) ->
  int * int -> int = <fun>

However I could not turn this hint into an actual implementation. Is someone able to do this? The logic behind using “callCC” in the memoization function is that if a value is found in the cache, then this is is an early exit condition.

like image 648
Adèle Blanc-Sec Avatar asked Sep 19 '15 12:09

Adèle Blanc-Sec


1 Answers

I feel like the issue is that in his answer to How to memoize recursive functions?, Michael called CPS style what is not CPS style. In CPS style, the extra continuation argument k is used whenever one wants to return a value - the value is then applied to k instead.

This is not really what we want here, and not what implements:

let gcd_cont k (a,b) =
  let (q, r) = (a / b, a mod b) in
  if r = 0 then b else k (b,r)

Here, k is not used for returning (b is returned directly), it is used instead of performing a recursive call. This unwinds the recursion: within gcd_cont, one can think of k as gcd_cont itself, just like if let rec was used. Later on, gcd_cont can be turned into a truly recursive function using a fixpoint combinator, that basically "feeds it to itself":

let rec fix f x = f (fix f) x
let gcd = fix gcd_cont

(this is equivalent to the call function that Michael defines)

The difference with defining gcd directly using a let rec is that the version with unwinded recursion allows one to "instrument" the recursive calls, as the recursion itself is performed by the fixpoint combinator. This is what we want for memoization: we only want to perform recursion if the result is not in the cache. Thus the definition of a memo combinator.

If the function is defined with a let rec, the recursion is closed at the same time as defining the function, so one cannot instrument the recursive call-sites to insert memoization.

As a side note, the two answers basically implement the same thing: the only difference is the way they implement recursion in the fixpoint combinator: Michael's fixpoint combinator uses let rec, Jackson's one uses a reference, i.e. "Landin's knot" — an alternative way of implementing recursion, if you have references in your language.

Sooo, to conclude, I'd say implementing that in the continuation monad is not really possible / does not really make sense, as the thing was not CPS in the first place.

like image 100
Armael Avatar answered Oct 15 '22 23:10

Armael