= Solution
Suppose that a direct <tree fold> with result type `[Tree a]` implements `proper`, so `proper = fold one two`. Every leaf has result `[]`, hence `one x = []` for every label `x`. Consequently `proper (Two (One x) (One y))` would always equal `two [] []`, independently of either label. Taking labels from `Bool`, the inputs `Two (One False) (One False)` and `Two (One True) (One False)` would therefore have equal results. Their correct results are `[One False, One False]` and `[One True, One False]`, which differ. This is a contradiction.
\b[There is no direct fold with only the proper-subtree list as its recursive summary.] This is the <direct tree-fold information obstruction>: replacing both children by equal summaries prevents the parent operation from recovering their different labels. The claim must not be extended to every expression containing a <tree fold>. A fold retaining the original tree alongside its proper-subtree list, followed by projection, does work; alternatively `tail . subs` uses the richer fold from part (f).
Back to article page
