Recursive Structural Types

A design for recursive types in datalit and Datafun: an inline rec binder, iso-recursive semantics, and recursion that must pass through a collection rather than a box. Written October 2026 in response to mandocs/drafts/recursive-structural-types.md; not implemented. Checked on paper against the AWFY benchmarks that need recursive data. The back-end consequences are inferred from reading the code, not tested.

Contents

• The problem
• The design in brief
• Syntax
• The guard rule
• What no box costs
• Iso-recursive, with roll and unroll inserted
• The type checker
• Borrowing match
• Runtime and backends
• Against the AWFY benchmarks
• Prior art
• What exists, what is missing
• Phases
• Open questions

The problem

Datalove cannot write a tree. An alias cannot name itself (type L: ?(int, L) is F064), and datalit has no aliases at all, because it is an expression language with no statements. The obvious fixes each break a constraint the draft sets:

• A statement-level alias does not exist in datalit.
• A box type gives datalit text a runtime meaning that the data format has no use for.
• Implicit boxing breaks "values are stored inline, never implicitly boxed" (mandocs/principles.md).

So a recursive type needs a name that lives inside one type expression, and an indirection that is already in the language.

The design in brief

rec Name T binds Name within T and nowhere else. Every use of Name must sit under a heap-backed collection between the use and its binder, which keeps the inline size finite without a new type. The types are iso-recursive: a rec type differs from its one-level unfolding. Rolling and unrolling are no-ops at run time, though, and the checker inserts them, so a literal never mentions them. Internally the binder becomes a de Bruijn index. Type equality then remains the derived PartialEq, and salsa hashing is unaffected.

Syntax

: rec Node { name: string, kids: [Node] } / {
  name = "root",
  kids = [
    { name = "a", kids = [] },
    { name = "b", kids = [{ name = "c", kids = [] }] },
  ],
}

The value is ordinary datalit. Only the type is new. JSON, the canonical recursive data, needs nothing further:

type Json: rec J enum {
  atom Null,
  term Bool bool,
  term Num f64,
  term Str string,
  term Arr [J],
  term Obj %{string = J},
}

• rec starts a type, so it joins the "type alias, type parameter" row of the reserved-word table (botspec Section 2.1). The parser recognizes it by the word alone, as that section requires. recursive would suit the keyword-heavy style just as well.
• type Json: rec J ... is an ordinary alias whose value is a rec type. A self-referencing alias without rec stays F064. A later ergonomic mode could desugar it.
• A rec name that shadows an alias, a type parameter or an outer rec name is an error.
• A binder that is never used, rec L int, is an error, so that each type has one spelling.

The guard rule

Each use of a bound name must have at least one of [_], %{_ = _}, #{_} or {| |} between it and its own binder. Structs, tuples, ?, !, terms, enums and inner rec binders do not count.

: rec L { elt: int, next: [L] }        // ok
: rec L { elt: int, next: ?L }         // error: L is not behind a collection
: rec L L                              // error
: rec A { b: rec B { a: A, bs: [B] } } // error: B is guarded, A is not
: rec L [L]                            // ok: [], [[]], ... are all finite

This is Algol 68's "shielding", with the collections in the role of ref. Algol also requires a struct on every cycle (the "yang" half of its yin-yang rule). That requirement exists to rule out ambiguous coercions, and Datalove has no implicit coercions, so the requirement is left out.

The check runs during hint conversion in time linear in the type. A stack records the collection depth at each binder. A use is legal when the current collection depth is greater than the depth at its own binder.

What no box costs

Recursion with a fixed arity has to go through a list:

: rec List { elt: int, next: [List] }     // at most one, by convention
: rec Tree { v: int, kids: [Tree] }       // exactly two, by convention

The type stops enforcing the arity. Each slot also holds a list handle where an option of a pointer would have been. Most recursive data is rose trees, JSON, or ASTs whose children are lists, and none of that pays. Cons lists and binary search trees do pay.

In the AWFY benchmarks the arity went unenforced in List, Towers and Richards, but expressing the structure was never a problem (Against the AWFY benchmarks).

If the cost matters, the smallest fix is to make the guard a slot of its own. That fix is a box under another name, and should be decided as one. This plan does not include it.

Iso-recursive, with roll and unroll inserted

Let T = rec X body. Unfolding T substitutes T for X in body. T and its unfolding are distinct types with the same layout, because rec is not a box. Rolling and unrolling therefore do nothing at run time, and inserting them silently does not hide any work.

• Roll happens only in checking mode, when a struct, tuple, list or enum literal is checked against an expected rec type. The literal is checked against the unfolding. This covers every datalit file and every hinted Datafun literal.

• Unroll happens at every elimination: field projection, tuple index, indexing, match, for, and destructuring. The head of a rec type is exposed first:

  n          : rec Node { name: string, kids: [Node] }
  n.kids     : [rec Node { name: string, kids: [Node] }]
  n.kids[0]  : rec Node { ... }
  

  A chain of projections lands back on the rec type rather than on a growing unfolding.

• Anything else is a mismatch. A value whose type is the unfolding, such as an unhinted literal bound to a variable, is not accepted where the rec type is expected. Adapt (@) performs the roll: it already means "clone, widen or coerce", and roll is the coercion that costs nothing. Unroll never needs @, because elimination does it.

The type checker

The changes, against crates/datalove-datalit/src/tycheck/types.rs and the Datafun checker:

1. Two variants in the datalit Type: Rec(TypeRec { name, body }) and RecVar(u32), a de Bruijn index where 0 is the innermost binder. Var(InternedText), the generic type parameter, is unaffected.

2. Hint conversion carries a binder stack. It resolves names to indices and runs the guard and unused-binder checks. This is the only place a free RecVar exists.

3. Every expression's type is closed. Unfolding substitutes a closed Rec, so no index ever needs shifting, and no RecVar escapes its binder. A debug assertion at the conversion boundary enforces this.

4. Equality is the derived PartialEq and Hash. De Bruijn indices make alpha-equivalence syntactic. Equi-recursive types would instead need a coinductive equality check (Amadio and Cardelli) at every comparison. Salsa needs Hash to agree with Eq, so they would also need every type graph minimized before it is hashed, and the order-insensitive enums make that minimization harder. This is the main reason to choose iso.

5. The binder name is not part of a type's identity. Otherwise rec A {..A..} and rec B {..B..} would be different types. The name lives in a field whose Eq and Hash ignore it, so diagnostics can print rec Node. The cost: salsa may backdate a memo whose only change is the name, and a diagnostic could then show a stale binder name. The fallback is no stored name and a generated rec Self.

6. An expose helper unfolds a rec at the head of a type. Every elimination site calls it before matching on the type's shape. Auditing those sites is the main work. A site that is missed reports a spurious mismatch, never an unsound acceptance, and tests over a recursive struct, enum and list will find the misses.

7. An unfold costs O(body), one level per elimination, and types never grow along a chain. If profiling finds the clones, interning Rec bodies makes the substituted copy O(1).

8. Generic unification is structural. Rec unifies only with Rec, and inference never unfolds a type. That keeps equi-recursion from coming back through the unifier.

9. Mutual recursion nests. An inner binder may refer to an outer one:

   rec E enum {
     term Lit int,
     term Block [rec S enum { term Let E, term Do E }],
   }
   

   This is the usual iso-recursive limitation. The S obtained by projecting out of E is not syntactically equal to a separately written rec S ... rec E ..., so which type is outermost matters. Wasm GC solves this with rec groups. Data files can likely live without them.

Every operation stays linear in the size of the type, and equality does not change. The new code is one conversion pass, one substitution, one helper, and an audit of the elimination sites.

Borrowing match

match consumes its input (botspec Section 8.8). A recursive struct can be read without moving it, because a field projection is a borrow: f(ref n.kids[0]?). A recursive enum cannot. Reading a Json or an AST means moving the value or cloning every level, so recursive enums can be built but not read in place. This plan therefore includes a borrowing match:

match ref v
case term Arr items        // items is a ref borrow of the payload
    call walk(ref items)
case default
end match

The form follows for item in ref xs, where the marker already means "the names this binds are borrows". match mut v would follow for ... in mut in the same way, binding payloads that may be written but not moved. The checker unrolls v's type before matching, as at every elimination. The ownership analysis treats each binding as a borrow rooted at v, the same rule that covers ref a[i]?.

Borrowing match does not depend on recursive types and is useful without them. Recursive enums are what make it necessary.

Runtime and backends

None of this has been checked against the code beyond reading TyDesc.

• Descriptors become cyclic. A rec type's TyDesc points to itself through the collection's element descriptor. TyDesc children are raw pointers (crates/datalove-rtdt/src/lib.rs), so the cycle can be represented. Building it has to tie the knot: allocate, memoize under the closed Rec type, then fill in. A naive recursion from Type never ends.
• Walkers over types must stop at collections. is_plain and computed_flags are examples. The guard rule makes stopping there correct, since every cycle passes through a collection and a collection is never plain. Whether is_plain already stops at lists is not yet known.
• Generated per-type glue must be memoized. Any backend that emits drop, clone, equality or print code by recursing over a type needs to memoize on Rec, so that the generated functions call each other instead of expanding forever.
• Deep values overflow the stack. Drop, clone, equality and printing recurse over values. They terminate, but a linked list of a million elements built as [List] will overflow the Rust stack, as a Box linked list does in Rust. This failure mode is new, and the lists of children in rose trees will reach it less often than cons lists will. The AWFY benchmarks never recurse more than 15 deep, so they will not catch it. It needs its own test.

Against the AWFY benchmarks

AWFY benchmarks that could not be written because Datalove has no recursive types are listed in the AWFY survey. Checked on paper against the AWFY JavaScript sources:

• Storage is a tree of arrays seven deep, whose leaves hold 1 to 10 empty slots. rec T [?T] is that shape exactly. A leaf is list.repeated(ref : ?Tree / none, n), and nothing reads the tree.

• Json is a rose tree. The parser pushes into [Json], and term literals roll implicitly. A term in a variable already needs @ to widen into an enum (botspec Section 3.6), so rolling through @ is the existing idiom. Its verifyResult is the one place that reads the tree. A consuming match works there, because the result is checked once.

• Towers keeps each pile as a [Disk] of length 0 or 1. With a fresh [] per move, each of the 8191 moves allocates. Swapping the emptied buffers through mem.swap and mut piles[p]! avoids that, provided an emptied list keeps its capacity:

  let t = list.pop(mut piles[p]!)
  call mem.swap(mut piles[p]!, mut t.next)
  call mem.swap(mut d.next, mut piles[q]!)
  call list.push(mut piles[q]!, d)
  

• List returns one of its arguments from tail(x, y, z) and passes each list to two or three recursive calls. With owned values the arguments are ref and each result is cloned. A reimplementation counted 2809 calls, of which 2107 are base cases, and 16,451 cloned nodes, where AWFY allocates 31. That turns a benchmark of calls and pointer chasing into one of allocation. Every result is a suffix of one of the three original lists, so a faithful port returns (which, skip) and walks the originals by ref. With no ref local, the walks are recursive, as in f(ref x[0]?.next).

• Richards packets are owned by one queue at a time. Appending at the end of a queue forwards mut queue[0]!.link down a recursion. Peeking and writing a packet in place is mut record.work_in[0]!. Tasks are shared between the link chain and the task table, so they stay an arena.

• CD walks x.parent.parent in put and remove. A red-black tree without parent links fits rec N { ..., left: [N], right: [N] }, but that is a different algorithm, and its deletion is the hard part.

Two things stand out. First, the guard rule never got in the way. Second, what blocks the remaining benchmarks is sharing, which no owned recursive type provides.

Prior art

References:

• Algol 68 Jargon File: Well-Formedness and Yin-Yang
• WebAssembly 3.0 specification
• Andreas Rossberg, Mutually Iso-Recursive Subtyping, OOPSLA 2023
• The CUE Language Specification, "Structural cycles"
• Amadio and Cardelli, "Subtyping Recursive Types", TOPLAS 1993
• Pierce, Types and Programming Languages, chapters 20 and 21

What exists, what is missing

What exists:

• Structural types as derived-equality trees.
• Aliases that expand to the types they name.
• Bidirectional checking, which always knows the expected type of a hinted literal.
• Collections that own heap storage.
• TyDesc children as raw pointers.

What is missing:

• The rec syntax in both grammars.
• The two Type variants, binder-aware hint conversion, the guard check, expose, and roll through @.
• A borrowing match ref and match mut.
• Knot-tying construction of descriptors, and memoized per-type glue in every backend.
• Some answer to drop, clone, equality and printing of deep values.

Phases

1. Front end. Parse rec in datalit and Datafun, convert hints to de Bruijn form, and check guards and unused binders. Add tests that reject each ill-formed example above.
2. Checking. Roll in checking mode, add expose at every elimination site, and roll through @. Write datalit tests for the rose tree, JSON and list shapes, and Datafun tests that walk them.
3. Borrowing match. match ref and match mut, with ownership rules for the bindings. This phase is independent of the others and can land first.
4. Runtime. Knot-tied descriptors, and a check of the type walkers. Load recursive datalit values with the runtime datalit loader.
5. Backends. Memoized glue in the interpreter, the JIT and C AOT. Run the engine tests on recursive values. Port Storage, Json and Towers to benchvs as the first real programs.
6. Deep values. Measure the depth at which drop and clone overflow, then decide between explicit work stacks and a documented limit.

Open questions

• Is the loss of "at most one" and "exactly two" through [_] acceptable, or will the guard eventually need a slot of its own?
• Does real data need mutual-recursion groups, or is nesting enough?
• In diagnostics, should binder names live in a field that equality ignores (and risk stale names after backdating), or be generated?
• Does an emptied list keep its buffer through list.pop? Towers' allocation-free moves depend on it.
• Should List be ported with cloning, which measures allocation, or with (which, skip) handles, which leaves recursive types little to do?
• Should map keys and set elements be allowed to recurse? The values are finite, so structural order is defined, but every comparison is deep.