Control.Recursion

Type-changing folds and unfolds over ordinary recursive datatypes.

A datatype opts in by defining its own one-layer base type plus three small structural functions: project opens one recursive layer, embed closes one, and map_layer changes only recursive positions. There is deliberately no universal fixed-point carrier: values keep their normal application-facing datatype, and the adapters remain local enough to audit beside its constructors.

The structural laws are embed(project(x)) == x, project(embed(layer)) == layer, and the usual identity and composition laws for map_layer. Mapping must preserve the layer constructor and every non-recursive field, visit each recursive position exactly once, and visit them left to right in declaration order. Those laws make project, embed, and map_layer an honest one-layer view rather than a second interpretation of the datatype.

cata and para terminate on finite values when project returns only strict subterms. ana and hylo terminate when their coalgebra eventually produces layers with no recursive positions. A materialized cata(..., ana(..., seed)) allocates the intermediate recursive value; hylo applies the same unfold and fold one layer at a time without that carrier. They agree for pure algebra and coalgebra pairs, but effects can make their observation order differ, so the library performs no automatic fusion.

Every algebra, coalgebra, and mapper row is open. Effects performed by map_layer and the recursive callback it invokes are observed in the mapper’s promised left-to-right order; no scheme handles, masks, or reorders them.

Functions and Values

cata

cata : forall e0 a b c d. ((a) -> b, ((a) -> c ! {e0}, b) -> d ! {e0}, (d) -> c ! {e0}, a) -> c ! {e0}

Collapse a finite recursive value bottom-up. project exposes one layer, map_layer replaces each recursive child with its folded answer, and algebra consumes the resulting layer.

This parameterized binary tree keeps payload type a separate from the recursive hole r; summing it demonstrates a type-changing fold.

fn main() =
  cata(project, map_layer, sum_layer, Branch(Leaf(1), Branch(Leaf(2), Leaf(3))))

6

ana

ana : forall e0 a b c d. ((a) -> b ! {e0}, ((a) -> c ! {e0}, b) -> d ! {e0}, (d) -> c, a) -> c ! {e0}

Build a finite recursive value top-down. coalgebra expands a seed into one layer of new seeds, map_layer recursively replaces those seeds with values, and embed closes the layer.

fn main() = ana(split_tree_seed, map_layer, embed, ("x", 1))

Branch(Leaf(xL), Leaf(xR))

para

para : forall e0 a b c d. ((a) -> b, ((a) -> (a, c) ! {e0}, b) -> d ! {e0}, (d) -> c ! {e0}, a) -> c ! {e0}

Fold bottom-up while retaining each original child beside its folded answer. The algebra receives (original, answer) at every recursive position, so it can reuse, inspect, or return an untouched subtree.

This string-carrying lambda term returns the original argument whenever an application has the literal identity function on its left.

fn main() =
  para(project, map_layer, simplify, App(Lam("x", Var("x")), App(Var("f"), Var("y"))))

App(Var(f), Var(y))

hylo

hylo : forall e0 a b c d. ((a) -> b ! {e0}, ((a) -> c ! {e0}, b) -> d ! {e0}, (d) -> c ! {e0}, a) -> c ! {e0}

Unfold a seed and fold each produced layer directly, without allocating an intermediate recursive value. For pure callbacks this equals materializing with ana and consuming with cata; effects retain the explicit mapper’s order and are not a general fusion law.

This monomorphic string-carrying lambda base functor builds nested lambdas conceptually and counts their nodes without ever constructing a Term.

fn main() = hylo(nested_lambdas, map_layer, count_layer, 3)

4