haskellrecursiontreecatamorphism

How to understand foldTree function?

I have been deeply studying foldTree function in Haskell, which is defined as follows:

foldTree :: (a -> [b] -> b) -> Tree a -> b
foldTree f = go where
    go (Node x ts) = f x (map go ts)

I recently came across the following interpretation of the line:

when we call f x vs we assume, that x and vs are already bound to known values.

go (Node x ts) = f x (map go ts)

The mention of a time element (using terms like "already" and "yet") confuses me. To better understand this, I started experimenting with some concepts borrowed from natural deduction and induction proofs. Specifically, I tried to conceptualize the second argument of f as follows:

  1. I assume a type [b] is defined.
  2. Then, I consider the actual definition of f in terms of combining this assumed [b] type with the a type to define the overall expression foldTree f tree, where tree has type Tree a.

How could I refine this line of thinking in terms of assumptions and not using actual function evaluation, assuming it is correct? Alternatively, is there another formal or intuitive perspective I could adopt to better understand this function and its mechanics?

Solution

  • This is consequence of lazy evaluation [Haskell-wiki].

    However, no value is bound to vs yet; the binding of vs is deferred until the recursion over the entire sub-forest is complete.

    Well it binds with an expression, with map go ts, and that is it. When f needs the value(s) of [b] it will force evaluation of that expression tree. This thus means that it will start evaluating map go ts. It is possible that the tree has no children, in which case map will return an empty list.

    If the tree has children, it will evaluate the list as nodes are needed through lazy evaluation, and it will not even per se evaluate go ti with ti the Node of one of the children.

    But because in Haskell functions are pure, the order essentially does not matter. You can just pretend that these items are evaluated.