Accumulator-passing-style for `mirror`

[anfelor]

Please quote the text that is incorrect:

In the definition of BinTree.mirror, there are two recursive calls: [..] This function cannot be straightforwardly rewritten to be tail recursive using accumulator-passing style.

In what way is this incorrect?

I guess it depends on your definition of straightforwardly, but there is certainly a version using accumulators (pseudo-code, sorry):

inductive BinZipper α where
  | root : BinZipper α
  | branchL (up : BinZipper α) (x : α) (r : BinTree α) : BinZipper α   -- for descending into left subtree
  | branchR (l : BinTree α) (x : α) (up : BinZipper α) : BinZipper α   -- for descending into right subtree

mutual
  def BinTree.mirror-app : BinZipper α → BinTree α -> BinTree α
    | .root, t => t  -- going up reached the root and we are done
    | .branchL up x r, l => mirror r (.branchR l x up) -- left subtree mirrored, lets do right subtree next
    | .branchR l x up, r => mirror-app up (.branch r x l) --- right subtree mirrored, lets go up with`.branch r x l`

  def BinTree.mirror : BinTree α -> BinZipper α → BinTree α
    | .leaf, up => mirror-app up .leaf -- done with this subtree, lets go up
    | .branch l x r => mirror l (.branchL up x r) -- descend into left subtree

(you can avoid mutual recursion by using a boolean to decide which function you are in).

How do you get there? I agree that it might out of the scope of the book, but it turns out to be quite simple: You just perform continuation-passing-style and then defunctionalize the closures 1. This technique always works (since CPS always works) and also often yields fast code in languages like Lean as it nicely makes use of reuse analysis to be fully in-place 2.

[david-christiansen]

It certainly does depend on your definition of "straightforwardly"! I think that CPS and defunctionalization are good topics for a second book on functional programming, but not a first one. Similarly, zippers as a first-order reification of a delimited continuation is a wonderful way to see the world, but I think that it's too much for the audience here.

I'll leave the issue open, because if you tripped over "straightforwardly" here, then someone else probably will too, so I should consider a more precise formulation like "using the tools and ideas presented in this book".

Thanks for the links to the papers - they look very interesting.