Companion Proposal: Inductive Enums and Structural Recursion
The enum and pattern-matching proposals lay solid groundwork. I’d like to extend the discussion to recursive data and checked, stack-safe traversal, particularly for execution DAGs and symbolic reasoning. Addressing this alongside the existing proposals would help establish first-class functional programming patterns within Mojo’s systems memory model.
I’ve put together a companion proposal to the enums and pattern matching RFCs that introduces two complementary features:
- Inductive Enums (
inductive enum): Recursive sum types declared naturally withSelf(directly, in payload structs, or inside supported containers likeList[Self]andDict[K, Self]) without manual boxing boilerplate. At runtime, values would be lightweight handles to immutable, reference-counted DAG nodes, making copies cheap O(1) operations and enabling safe subtree sharing. - Structural Functions (
match recursiveandrecur): First-class structural recursion where the compiler checks exhaustive coverage and proves that everyrecurcall strictly descends to a structural sub-element. On finite data, this guarantees termination provided each activation performs finite local work and makes finitely many child requests. The proposed lowering uses explicit heap frames for structural calls and an iterative worklist for structural release, keeping native stack usage O(1) with respect to structural depth. Heap usage can still grow with the traversal; ordinary arm code and non-recursive payload operations, including destructors, retain their usual stack behavior.
Links
- Full Proposal: inductive-types-and-structural-recursion.md
- Companion Diffs in
enums.mdandpattern-matching.md: View Diff - Working Library Prototype on Mojo 1.1: FP Mojo
Why Not Just a Library Heap Box?
Earlier in this thread, it was suggested that recursive enums could compose with a library box like HeapBox[T]. A generic box provides the necessary indirection, but boxing alone does not establish three additional properties:
- Stack-Safe Deallocation: A box whose destructor recursively destroys its children can overflow the native stack on deeply nested data. The failure depth depends on frame size and available stack space; avoiding this requires an iterative release strategy.
- Structural Sharing: Uniquely owned boxes do not provide shared subtree ownership. Starting with one leaf and applying
x = add(x, x)sixty times produces a shared DAG with 61 distinct nodes. Fully expanding the same value into an unshared tree requires 2⁶¹ − 1 nodes. - Checked Descent and Stack Lowering: A generic heap box does not by itself establish checked structural descent or guarantee execution on an explicit frame stack. Those require additional traversal machinery and, for the proposed static checks, compiler support.
A library can implement shared nodes, iterative release, and explicit frame
stacks, as FP Mojo prototype does. Its current API supports up to sixteen clauses per match, copies node payload fields into clause arguments, and checks decreasing height for Next continuations at runtime. That height check does not prove that the target is an actual descendant. The prototype’s documentation also reports about eight seconds at -O3 to build an expression matching and rewriting program. These are properties of this implementation, rather than inherent limits of libraries. Native support could remove these API workarounds and provide static descent checks; its compile-time and runtime costs would need measurement.
The Proposal in One Example
The following is proposed language syntax. The working library prototype uses a different API.
inductive enum Expr:
case num(Int)
case add(Self, Self)
case if_else(Self, Self, Self)
def evaluate(e: Expr) -> Int:
match recursive e:
case .num(value):
return value
case .add(recur left, recur right):
return left + right
case .if_else(recur condition, then_branch, else_branch):
if condition != 0:
return recur then_branch
return recur else_branch
def simplify(e: Expr) -> Expr:
match recursive memo e:
case .add(recur .num(0), recur right):
return right
case recur rebuilt:
return rebuilt
- Eager vs. On-Demand Recursion: Placing
recurin a pattern (e.g.
recur left, recur right) requests child results before the arm body runs.
Inside an arm body,recurevaluates on demand, soevaluatedescends only into the chosen conditional branch. - Non-Destructive Rewriting:
case recur rebuiltgathers child results and rebuilds the node. If every rewritten child is the original child handle, it reuses the original parent without allocating a replacement node. Traversal frames and caches may still allocate. Usingmemoalso avoids repeated work on shared nodes and lets their rewritten results remain shared. Withoutmemo, changed shared nodes can be rebuilt separately along different paths. - Clean Composition: Payloads can use ordinary generic structs for named fields, as suggested earlier. Named case fields would be an equally natural alternative syntax.
Key Design Choices
- Storage Model: Shared immutable nodes with atomic reference counting. Uniquely owned boxes do not provide shared subtree ownership. Region arenas are attractive when nodes share a phase lifetime, but retain dead intermediate nodes until their region can be reclaimed. Multi-pass algorithms can use separate arenas and discard an earlier arena once nothing references it; reference counting instead supports independently lived, persistent subtrees.
- Explicit
recurKeyword: Choosing explicitrecurover unmarked recursion makes calls that use explicit-stack lowering visible, and lets child results be requested directly inside pattern destructuring. - Opt-In Memoization (
match recursive memo): Because arm bodies can have side effects, memoization is explicit. It reuses cached results for shared DAG nodes and preserves their sharing across rewrites. For traversals that process each child slot a bounded number of times, with constant-cost arm work and result copying, expected traversal time is O(V + E), where V counts distinct visited nodes and E counts their child slots, including repeated references. For bounded-arity nodes, this reduces to O(V). The non-memoizedevaluateabove can revisit shared nodes; addingmemowould avoid that repeated work.
The accompanying FP Mojo library provides a working prototype for exploring these storage and traversal choices.