212B Recitation 5 (2001-02-14) Notes
Joshua Dunfield (joshuad+@cs)

CONTINUATIONS
There's a handout on continuations; I'll follow that pretty closely,
except that I've improved the variable names...

append

(* append : 'a list * 'a list -> 'a list *)
fun append (nil, ys) = ys
  | append (x::xs, ys) = x :: append(xs, ys);

Actually, we can write this in tail-recursive form, using continuations.

fun append' (nil, ys, cont) = cont ys   --Apply the continuation instead of returning ys
  | append' (x::xs, ys, cont) = append' (xs, ys, fn r => cont(x::r))
            --Recurse with a continuation that prepends x to whatever the continuation is passed

fun append2 (xs, ys) = append' (xs, ys, fn r => r)

Example:
    append2 ([1,2], [3,4])
==> append' ([1,2], [3,4], fn r => r)
==> append' ([1], [3,4], fn r1 => (fn r => r) (1::r1))
==> append' ([], [3,4], fn r2 => (fn r1 => (fn r => r) (1::r1)) (2::r2))
==> (fn r2 => (fn r1 => (fn r => r) (1::r1)) (2::r2)) [3, 4]
==> (fn r1 => (fn r => r) (1::r1)) (2::[3, 4])
==> (fn r => r) (1::2::[3,4])
==> 1::2::[3,4]   = [1,2,3,4]

But we haven't really saved anything -- we still have to build up (closures)
and then call the continuation, which does all the necessary cons'ing.

    append ([1,2], [3,4])
==> 1:: append([2], [3,4])
==> 1::2::append([], [3,4])
==> 1::2::[3,4]   = [1,2,3,4]

In both versions, the running time is proportional to the length of xs.
For append, the continuation-based version is much more complicated,
and I would have stuck with the original version.

Here's a problem where continuations make more sense...
 prefix

prefix p xs:    shortest prefix s.t. p is false on the next element;
  if p holds for all xs, return NONE;
Note that if p doesn't hold for the first element, we return nil because
p is false for the "next element" after the empty list.

(* consOpt : 'a * ('a list option) -> 'a list option *)
 fun consOpt (x, NONE) = NONE
    | consOpt (x, SOME xs) = SOME (x::xs)

(* prefix : ('a -> bool) -> 'a list -> ('a list) option *)
fun prefix p nil = NONE
  | prefix p (x::xs) =
      if p(x) then consOpt (x, prefix p xs)
      else SOME nil

   fun pos (x: int) = (x > 0)
     pos: int -> bool

Examples:
   prefix pos [1, 2, ~5, 3] `-> SOME [1, 2]
   prefix pos [1, 2, 3] `-> NONE
   prefix pos [] `-> NONE
   prefix pos [~4] `-> SOME []

  prefix pos [1, 2, ~5, 3] ==> if pos(1) then consOpt (1, prefix pos [2, ~5, 3]) else ...
                  ==> consOpt (1, prefix pos [2, ~5, 3])
                  ==> consOpt (1, consOpt (2, prefix pos [~5, 3]))
                  ==> consOpt (1, consOpt (2, if pos(~5) then ... else SOME nil))
                  ==> consOpt (1, consOpt (2, SOME nil))
                  ==> consOpt (1, SOME(2::nil))
                  ==> SOME(1::(2::nil))
                   =    SOME [1,2]

 prefix pos [1, 2, 3] ==> if pos(1) then consOpt (1, prefix pos [2,3]) else ...
                      ==> consOpt (1, prefix pos [2,3])
                      ==> consOpt (1, consOpt(2, prefix pos [3]))
                      ==> consOpt (1, consOpt(2, consOpt(3, prefix pos [])))
*                     ==> consOpt (1, consOpt(2, consOpt(3, NONE)))
*                     ==> consOpt (1, consOpt(2, NONE))
*                     ==> consOpt (1, NONE)
                      ==> NONE


(* prefix': ('a -> bool) -> ('a list * ('a list -> 'b option)) -> 'b option *)
(* USED WITH 'a list for 'b *)
fun prefix' p (nil, cont) = NONE
  | prefix' p (x::xs, cont) = 
      if p(x) then prefix' p (xs, fn r => cont (x::r))
      else cont nil

(* prefix2: ('a -> bool) -> 'a list -> ('a list) option *)
fun prefix2 p xs = prefix' p (xs, fn r => SOME r)

So let's try prefix2 on [1,2,3].

 prefix2 pos [1, 2, 3] ==> prefix' pos ([1, 2, 3], fn r => SOME r)
    ==> if pos(1) then prefix' pos ([2, 3], fn r2 => (fn r => SOME r) (1::r2)) else ...
    ==> prefix' pos ([2, 3], fn r2 => (fn r => SOME r) (1::r2))
    ==> prefix' pos ([3], fn r3 => (fn r2 => (fn r => SOME r) (1::r2)) (2::r3))
    ==> prefix' pos ([], fn r4 => (fn r3 => ...) (3::r4))
zing!  ==> NONE

...a shorter chain of reductions than for `prefix'.

If we had, say, [1, 2, 3, ~7], then we'd have to call the continuation, and
the reductions would resemble those for append2, above.

(...improvised discussion of success and failure continuations,
and of Assignment 3...)