These transforms have some interesting properties. One is that---assuming we never reduce inside a lambda term, but only when redexes are present in the outermost level---the formulas generated by these transforms will always only have a single candidate redex to be reduced at any stage. In other words, the generated expressions dictate in what order the components from the original expressions will be evaluated. As it happens, the first transform above forces a *call-by-name* reduction order: assuming `M N` to be a redex, redexes inside `N` will be evaluated only after `N` has been substituted into `M`. And the second transform forces a *call-by-value* reduction order. These reduction orders will be forced no matter what the native reduction order of the interpreter is, just so long as we're only allowed to reduce redexes not underneath lambdas.
-Plotkin did important early work with CPS transforms (around 1975), and they are now a staple of academic computer science.
+Plotkin did important early work with CPS transforms, and they are now a staple of academic computer science. (See the end of his 1975 paper [Call-by-name, call-by-value, and the lambda-calculus](http://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf).)
Here's another interesting fact about these transforms. Compare the translations for variables and applications in the call-by-value transform:
let callcc body = fun outk -> body (fun v localk -> outk v) outk
-<!-- GOTCHAS?? -->
+ <!-- GOTCHAS?? -->
3. `callcc` was originally introduced in Scheme. There it's written `call/cc` and is an abbreviation of `call-with-current-continuation`. Instead of the somewhat bulky form:
- (call/cc (lambda (k) ...))
+ (call/cc (lambda (k) ...))
-I prefer instead to use the lighter, and equivalent, shorthand:
+ I prefer instead to use the lighter, and equivalent, shorthand:
- (let/cc k ...)
+ (let/cc k ...)
Callcc examples
This also works and as you can see, delivers the expected answer `101`.
-At the moment, I'm not able to get the third example working with the monadic library. I thought that this should do it, but it doesn't type-check:
+The third example is more difficult to make work with the monadic library, because its types are tricky. I was able to get this to work, which uses OCaml's "polymorphic variants." These are generally more relaxed about typing. There may be a version that works with regular OCaml types, but I haven't yet been able to identify it. Here's what does work:
- # C.(run0 (callcc (fun k -> unit (1,k)) >>= fun (p1,p2) -> p2 (2,unit) >>= fun p2' -> unit (p1,p2')));;
+ # C.(run0 (callcc (fun k -> unit (1,`Box k)) >>= fun (p1,`Box p2) -> p2 (2,`Box unit) >>= fun p2' -> unit (p1,p2')));;
+ - : int * (int * [ `Box of 'b -> ('a, 'b) C.m ] as 'b) as 'a =
+ (2, (2, `Box <fun>))
-If we figure this out later (or anyone else does), we'll come back and report. <!-- FIXME -->
+<!-- FIXME -->
Example 1:
- ; (+ 100 (+ 10 (abort 1))) ~~> 1
+ ; (+ 1000 (+ 100 (abort 11))) ~~> 11
- app2 (op2 plus) (var hundred)
- (app2 (op2 plus) (var ten) (abort (var one)))
+ app2 (op2 plus) (var thousand)
+ (app2 (op2 plus) (var hundred) (abort (var eleven)))
# Continuation_monad.(run0(
- abort 1 >>= fun i ->
- unit (10+i) >>= fun j ->
- unit (100+j)));;
- - : int = 1
+ abort 11 >>= fun i ->
+ unit (100+i) >>= fun j ->
+ unit (1000+j)));;
+ - : int = 11
When no `reset` is specified, there's understood to be an implicit one surrounding the entire computation (but unlike in the case of `callcc`, you still can't capture up to *and including* the end of the computation). So it makes no difference if we say instead:
# Continuation_monad.(run0(
reset (
- abort 1 >>= fun i ->
- unit (10+i) >>= fun j ->
- unit (100+j))));;
- - : int = 1
+ abort 11 >>= fun i ->
+ unit (100+i) >>= fun j ->
+ unit (1000+j))));;
+ - : int = 11
Example 2:
- ; (+ 100 (reset (+ 10 (abort 1)))) ~~> 101
+ ; (+ 1000 (reset (+ 100 (abort 11)))) ~~> 1011
- app2 (op2 plus) (var hundred)
- (reset (app2 (op2 plus) (var ten) (abort (var one))))
+ app2 (op2 plus) (var thousand)
+ (reset (app2 (op2 plus) (var hundred) (abort (var eleven))))
# Continuation_monad.(run0(
reset (
- abort 1 >>= fun i ->
- unit (10+i)
+ abort 11 >>= fun i ->
+ unit (100+i)
) >>= fun j ->
- unit (100+j)));;
- - : int = 101
+ unit (1000+j)));;
+ - : int = 1011
Example 3:
(shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
Continuation_monad.(let v = reset (
- let u = shift (fun k -> k [1] >>= fun x -> unit (10 :: x))
+ let u = shift (fun k -> k [1] >>= fun x -> unit (10 :: x))
in u >>= fun x -> unit (100 :: x)
) in let w = v >>= fun x -> unit (1000 :: x)
- in run0 w)
+ in run0 w);;
- : int list = [1000; 10; 100; 1]
(app (reset (app2 (op2 plus) (var ten)
(shift (\k. (var k))))) (var one))
- (* not sure if this example can be typed as-is in OCaml. We may need a sum-type *)
+ (* not sure if this example can be typed as-is in OCaml... this is the best I an do at the moment... *)
+
+ # type 'x either = Left of (int -> ('x,'x either) Continuation_monad.m) | Right of int;;
+ # Continuation_monad.(let v = reset (
+ shift (fun k -> unit (Left k)) >>= fun i -> unit (Right (10+i))
+ ) in let w = v >>= fun (Left k) ->
+ k 1 >>= fun (Right i) ->
+ unit (100+i)
+ in run0 w);;
+ - : int = 111
+
+<!--
+# type either = Left of (int -> either) | Right of int;;
+# let getleft e = match e with Left lft -> lft | Right _ -> failwith "not a Left";;
+# let getright e = match e with Right rt -> rt | Left _ -> failwith "not a Right";;
+# 100 + getright (let v = reset (fun p () -> Right (10 + shift p (fun k -> Left k))) in getleft v 1);;
+-->
Example 7:
(shift (\k. app (var k) (app (var k) (var one))))))
Continuation_monad.(let v = reset (
- let u = shift (fun k -> k 1 >>= fun x -> k x)
+ let u = shift (fun k -> k 1 >>= fun x -> k x)
in u >>= fun x -> unit (10 + x)
) in let w = v >>= fun x -> unit (100 + x)
in run0 w)