foldTree step-by-step evaluation-CodePudding

Assuming these definitions of foldTree, a Tree and a function f:

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

tree :: Tree String
tree = Node
      "Alpha"
      [ Node "Beta" [Node "Epsilon" [], Node "Zeta" [], Node "Eta" []]
      , Node "Gamma" [Node "Theta" []]
      , Node "Delta" [Node "Iota" [], Node "Kappa" [], Node "Lambda" []]
      ]

f x xs = [x] <> (map ('\t' :) (concat xs))

I will try to evaluate foldTree f tree:

  foldTree f tree
= go (Node "Alpha" [ Node "Beta" [Node "Epsilon" [], Node "Zeta" [], Node "Eta" []], Node "Gamma" [Node "Theta" []], Node "Delta" [Node "Iota" [], Node "Kappa" [], Node "Lambda" []]]
= f "Alpha" (map go [...])
...

At this point, my question is: how does equational reasoning work with closures ? The definition of go has f; however, that is certainly not between its parameters. Is there some trick that allows the insertion of that definition?

CodePudding user response：

Simply, a definition is allowed to refer to any name which is in scope.

"Closures" is a concept much more relevant in the presence of mutation. In Haskell where there's none, a concept of "scope" is enough.

go's definition is nested inside that of foldTree, so has access to its parameter f. In other words, inside go's definition, f is in scope.

The definition can be re-written as

{-
foldTree f t = go t
    where
         go (Node x ts) = f x (map go ts)
-}
foldTree f t =
   let { go (Node x ts) = f x (map go ts) } 
   in go t

and any call foldTree f1 t1 is evaluated as

> foldTree f1 t1 
=>
  let { f=f1; t=t1 }
  in
    let { go (Node x ts) = f x (map go ts) } 
    in go t
=>
  ....

and these are simple nested lets, so the inner one has access to every name defined by the outer one.

To easier see what's going on, try evaluating it first with a simpler example data, like Node "Alpha" [], Node "Alpha" [Node "Beta" []], etc.

For example, with

f0 x xs = [x] <> (map ('\t' :) (concat xs))

the evaluation for Node "Alpha" [] proceeds as

> foldTree f0 (Node "Alpha" []) 
=>
  let { f=f0; t=Node "Alpha" [] }
  in
    let { go (Node x ts) = f x (map go ts) } 
    in go t
=>
  let { f x xs = [x] <> (map ('\t' :) (concat xs))
      ; go (Node x ts) = f x (map go ts) 
      } 
  in go (Node "Alpha" [])
=>
  let { f x xs = [x] <> (map ('\t' :) (concat xs))
      ; go (Node x ts) = f x (map go ts) 
      ; (Node x1 ts1) = (Node "Alpha" [])
      } 
  in f x1 (map go ts1)
=>
  let { f x xs = [x] <> (map ('\t' :) (concat xs))
      ; go (Node x ts) = f x (map go ts) 
      ; x1 = "Alpha"
      ; ts1 = []
      ; xs1 = map go ts1
      } 
  in [x1] <> (map ('\t' :) (concat xs1))
=>
  ["Alpha"] <> (map ('\t' :) (concat []))
=>
  ["Alpha"] <> (map ('\t' :) [])
=>
  ["Alpha"] <> []
=>
  ["Alpha"]