Direct tree-fold information obstruction

ID: direct-tree-fold-information-obstruction

A direct tree fold gives a parent operation only its children's folded summaries. If two different children have equal summaries, the parent cannot distinguish them. For a leaf-labelled binary tree, a function returning proper subtrees maps every leaf to []. A direct fold with precisely that result type would therefore map every two-leaf tree to the same result, despite their possibly different labels. This rules out that direct fold, while permitting a richer folded summary followed by projection.

New to topics? Read the docs here!