Defunctionalized Lists

The last post finished with a list-based implementation of the BFS traversal. Now I am left with the problem of restoring tail-recursiveness by coming up with a properly tail-recursive version of append (as usual, its synonym is @). Let's recall the definition:

let rec append l r = match l with
| []      -> r
| x :: xs -> x :: (append xs r)

Transforming it to continuation-passing style (CPS):

let rec append_cps l r k = match l with
| []      -> k r
| x :: xs -> append_cps xs r (fun v -> k (x :: v))

so that the original append is:

let append l r = append_cps l r (fun k -> k)

Now the continuations used by append_cps fall into a few usage patterns:

• if the left argument is empty, the continuation is invoked as is
• otherwise, a new continuation is built from the old and the head, to prepend it to the value of the continuation
• everything starts with the identity continuation

Hence, the type:

type 'a kont = KNil | Kons of 'a kont * 'a

defunctionalizes the continuations as type constructors instead of as closures (the pattern to follow is, in general, abstract over the free variables of the continuation). Replacing continuations in the CPS version by these data:

let rec append_kont l r k = match l with
| []      -> kapply k r
| x :: xs -> append_kont xs r (Kons (k, x))

where now have l @ r ≡ append_kont l r KNil. We have yet to apply the reified continuation to the closed-over values; that is, we need to specify kapply: we move the closure constructions in the CPS version to the corresponding branch of a match over the reified continuation constructors:

let rec kapply k v = match k with
| KNil        -> v
| Kons (k, x) -> kapply k (x :: v)

Now, the type 'a kont is isomorphic to the type of lists: F(KNil) = [], and F(KCont (k, x)) == x :: F(k). Exploiting this fact, let's rewrite:

let rec append_list l r t = match l with
| []      -> lapply t r
| x :: xs -> append_list xs r (x :: t)

let rec lapply l v = match l with
| []     -> v
| x :: l -> lapply l (x :: v)

so that now l @ r ≡ append_list l r []. Now this is where things get weird. Believe it or not, append_list and lapply are, deep down, the same function. To see this, abstract r:

let rec append_list l t = match l with
| []      -> t
| x :: xs -> append_list xs (x :: t)

so that l @ r ≡ lapply (append_list l []) r. Compare lapply to this append_list, and write:

let append l r = lapply (lapply l []) r

We're now done, as lapply is tail recursive. What's more, its real name is List.rev_append, which we don't have to write since it's built-in to OCaml. Also, rev l is a shorthand for rev_append l []. The traversal, in tail-recursive form is:

let fold_bfs f e t =
  let rec fold e = function
  | []       -> e
  | L x :: q -> fold (f e x) q
  | N t :: q -> fold e (List.rev_append (List.rev q) t)
  in fold e [t]

I will show next that there is still room for improvement.