Companion Proposal: Inductive Enums and Structural Recursion

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:

  1. Inductive Enums (inductive enum): Recursive sum types declared naturally with Self (directly, in payload structs, or inside supported containers like List[Self] and Dict[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.
  2. Structural Functions (match recursive and recur): First-class structural recursion where the compiler checks exhaustive coverage and proves that every recur call 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


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:

  1. 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.
  2. 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.
  3. 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 recur in a pattern (e.g.
    recur left, recur right) requests child results before the arm body runs.
    Inside an arm body, recur evaluates on demand, so evaluate descends only into the chosen conditional branch.
  • Non-Destructive Rewriting: case recur rebuilt gathers 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. Using memo also avoids repeated work on shared nodes and lets their rewritten results remain shared. Without memo, 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 recur Keyword: Choosing explicit recur over 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-memoized evaluate above can revisit shared nodes; adding memo would avoid that repeated work.

The accompanying FP Mojo library provides a working prototype for exploring these storage and traversal choices.

@owenhilyard - Splited the proposal into another thread.

Hi Anatoly, regarding:

Mojo is a systems programming language in the style of C/C++/Rust. Features like reference counting and heap allocation are therefore implemented by users (e.g. as libraries), rather than being baked into the programming language. The language construct you’re proposing seems to be inspired by FP languages where RC and heap allocation are baked in. Given this difference, can you explain how you see your proposal fitting well into Mojo? Right now, I can’t see it.

Notably, recursive data structures where each node is allocated individually on the heap is often considered an anti-pattern (bad idea) when writing high-performance code. I wouldn’t want Mojo to reinforce that pattern by offering a language construct that relies on it.

Hi Nick,

Great question! You’re right that the current draft commits to a particular storage policy. My intent was to provide a complete abstraction for expressing inductive data and structural computations declaratively, but those capabilities could be separated from the storage implementation.

Introducing inductive types to Mojo doesn’t inherently imply that every node must be an individually heap-allocated, atomically reference-counted object.

In particular, none of the core language-level guarantees in the proposal require reference counting:

  • Exhaustiveness checking across constructors.
  • Compile-time descent verification, ensuring each recur targets a proven structural descendant.
  • recur requests within arm bodies, supported by coroutine-style frame splitting.
  • O(1) native stack usage for structural traversal through explicit frame stacks.

Iterative cleanup is also possible without RC, but requires additional cooperation from the storage implementation. Knowing where children are and establishing acyclicity are necessary foundations; we also need finite child enumeration, valid borrows, and protection against mutation that invalidates descent. Cleanup needs operations for detaching children and releasing storage while respecting payload destructors.

Perhaps a design based on library traits would fit Mojo’s philosophy better. Similar to how the enum proposal uses EnumLike, the language could support match recursive and recur through an interface describing structural children. For example, uniquely owned recursive children could be expressed as:

enum Expr:
    case num(Int)
    case add(OwnedPointer[Self], OwnedPointer[Self])

With suitable structural and ownership contracts, the compiler could check coverage and descent, lower traversal onto an explicit stack, and generate iterative cleanup for compatible storage and payload types.

OwnedPointer still allocates individually. Supporting arenas or index-based layouts would require additional contracts for context, origins, and structural invariants, plus an explicit policy for allocating traversal frames.

For ASTs constructed once and repeatedly traversed, arenas or contiguous storage are often preferable. Independently reclaimable nodes nevertheless have useful applications:

  • MLIR allocates each operation individually, and rewrites mutate its IR in place.
  • Some incremental compilers and symbolic systems use persistent structures whose subtrees are shared across revisions.
  • A conventional arena retains dead nodes until its region can be reclaimed. Separate arenas for successive phases can mitigate this when lifetimes permit; independently lived subtrees may benefit from more granular reclamation.

Decoupling the storage mechanism lets each workload choose the layout that fits it while keeping checked recursion.

For users working on data science applications, especially those coming from Python, the payoff would be checked structural traversal without hand-written traversal stacks, together with compile-time coverage checking.

Would a storage-agnostic version of the proposal fit Mojo better?

@nick

Ultimately, it boils down to what kind of language Mojo wants to be.

While low-level systems capabilities make Mojo a compelling alternative to C, C++, and Rust, capturing Python users, such as data scientists and the mathematically inclined community more broadly, requires pairing performance with high-level, declarative primitives that meet users where they are.

Rust already has algebraic data types and exhaustive pattern matching. But development friction still makes it painful to use for data science practice. The opportunity for Mojo is to extend these capabilities and make them fit naturally into the way math & data science practitioners work.

End users need pre-baked, declarative primitives to express ideas effortlessly, relying on the language and underlying libraries to handle complexity and performance behind the scenes. The hallmark of a successful design is a set of “effortless” APIs that hide this friction, much as JAX and PyMC do in Python.

Finally, inductive types are a cornerstone for ensuring program correctness and enabling automatic mathematical reasoning—both are quite important for math and data science domains. While adopting full dependent type theory (like Lean 4) is both unrealistic and unnecessary, supporting basic inductive types would go a long way for mathematically inclined users.

So let’s articulate why effortless inductive types could be compelling for mathematics and data science users. Some of the clearest immediate beneficiaries would be people building symbolic systems, modeling tools, and scientific libraries. Other users would benefit through the APIs those libraries provide:

  • Let users define objects the way they think about mathematics. Symbolic expressions, mixture distributions, and hierarchical models can be described through a few constructors, making mathematical structure directly visible in the code.

  • Provide structural correctness checks with little additional effort. Typed constructors and exhaustive matching catch incorrect payloads, missing operands, and forgotten cases before users launch expensive computations.

  • Let users concentrate on mathematical rules. Generated constructors, pattern matching, and reusable library folds would let users write what each case means while the language and libraries handle the machinery.

  • Make automated reasoning more accessible. Declarative inductive definitions give verification tools a standard basis for generating induction principles, checking structural termination, and verifying mathematical transformations.

  • Offer Python users a compelling combination of simplicity and rigor. Concise, readable definitions combined with stronger compiler checks and native execution would help exploratory mathematical code grow into dependable scientific software without requiring users to become systems programming specialists.

Most of the heavy lifting should, of course, be handled by libraries. However, it would be great to make recursive inductive types straightforward to declare, with language support for type checking, ownership, and exhaustiveness. That would give libraries a common foundation for delivering the “effortless” experience these users are looking for.

Thank you for the extra detail. I think I’m starting to see how some variation of your proposal could align with Mojo’s design philosophy.

Regarding:

Is the core of your request that you want the ability to declare enums that are “recursive”, i.e. Expr can store instances of Expr? Plus some guarantees that recursion terminates?

Mojo already intends to support recursive types. And when it does, the storage policy will be explicit through types such as OwnedPointer that you used in the example I quoted.

If the other feature you want is proof of termination, then I would suggest putting together a proposal that focuses solely on how this would work, while assuming that Mojo already plans to support recursive type definitions such as the example I’ve quoted. That might make your proposal more digestible and in line with Mojo’s design philosophy.

To maximize the chance that Modular reads your proposal, I would suggest stripping it down to the bare minimum, beginning with a motivation section and then presenting the smallest set of features that achieve your goal. Any optional/“nice to have” ideas can be moved to an appendix. Basically: small proposals are much easier to engage with than large ones.

Finally, I suggest avoiding “loose” statements like:

I personally am not convinced by these kinds of statements. Every programmer wants to express their ideas effortlessly, but we often disagree on how to achieve that. To make an effective argument of this kind, you would need to convince everyone that you know how other people think, or know what other people want, which I’m not sure you be able to pull off. I would instead focus on providing practical examples of how the features your proposing would make certain kinds of Mojo programs easier to write, or faster, or more reliable. And I would cater these examples to Mojo’s near-term target audience: HPC programmers and (if possible) AI kernel developers.

Thank you for your candor! Let me know when you start considering data scientists part of your target audience. Then we can discuss how enhanced type checking relates to formal proof guarantees and why it is important in math-related applications.

Just to clarify: I am not speaking in behalf of Modular. Perhaps Modular is interested in exploring features for data scientists and mathematicians. I just know that the near-term priorities are mostly in the AI and HPC space. Long-term, Mojo aims to serve a wider audience. The roadmap talks a bit about this.

@caroline, Please clarify the position of Modular Inc. on whether it considers data scientists part of its target audience. If they are included in the long-term vision, when and how does Modular plan to integrate feedback from the data science community into the language, standard library, and broader product suite (e.g., during Phase 3)?

On a personal note, signaling to a massive segment of potential enterprise customers that they are not your target audience is a pretty bold business move, courageous even. Meanwhile, I straggle to see why any self-respecting data scientist or an applied mathematician would be interested contributing to the ecosystem that does not consider them target audience.

Hi! Data scientist here. :waving_hand: Just thought I’d chime in and say that Mojo has been an immensely helpful tool for our research lab. We’ve been using it to accelerate (and modernize) our high-performance data processing pipelines. I’d say we are self-respecting and we even contribute some small amount back to the ecosystem. I definitely say there’s some overlap with our needs and what modular is providing, even though we’re not strictly doing work with generative AI.

Hi folks, I think there is likely singificant confusion being introduced by mojo community members here, I’ll try to clarify:

YES, we do want mojo to be used for scientific computing and many other purposes. You can see in our roadmap that we’re building mojo to be a general purpose language, and as Jeff and other folks have pointed out, it is already not bad for these usecases!

That said, we still do need to prioritize our investments, and we don’t always read new proposals the day they’re posted, particularly when it is on a saturday :slight_smile: :slight_smile:

@anatolvitold I can’t access your proposal doc, is the URL right? https://github.com/anatolvitold/modular/blob/proposal/inductive-structural-recursion/Mojo/proposals/inductive-types-and-structural-recursion.md

Hi @clattner,

Glad to hear that! :slight_smile:

I have re-uploaded the proposal. The link should work now.

Hi @anatolvitold,

Thanks for the questions! I hear you on the confusion and frustration.

To echo Chris’s point: Mojo is meant to be a general-purpose programming language. We’re focusing on specific areas right now so we can deliver on the roadmap we’ve committed to, but data scientists and applied mathematicians are still very much part of Mojo’s audience.

At this stage, Mojo serves that audience by keeping the core language small and low-level while making it possible to build great libraries on top of it. Those libraries should look and feel like first-class features of the language. I think that’s what Nick was getting at.

As for design feedback, Mojo will likely have an RFC process eventually, where the community can propose, discuss, refine, and vote on new features. We’re not there yet. Until then, you’re doing the right thing: posting your idea on the forum and opening up the discussion.

Thanks again for your feedback.

Thank you, @Caroline! That means a lot.