Repository navigation
feat(desugar): data types that refer to each other, as nested recursive types - #440
Conversation
…ve types
`data Tree = Leaf | Node(I32, Forest)` and `data Forest = FNil |
FCons(Tree, Forest)` were refused by name. They are now accepted, behind
the flag `--unstable-core` as each recursive type is.
The core has no new former: the types of a cycle become nested `mu`
types (Bekic's construction), in the order of their names. A `data`
type that is entered hides, for its body, each `data` type in progress
that comes after it: in that body, such a type is not a variable, and
it is expanded again. For Forest before Tree:
Forest = mu F. () + ((() + (I32 * F)) * F)
Tree = () + (I32 * Forest) (not folded)
So the unfolding of each type has the other types in it as they are,
and not types that are only equal to them after more unfolds. A field
of a constructor has the type that its declaration names. The checker
and the 2 backends do not change.
Equality of 2 recursive types now gives the 2 bound variables a new
name when their names differ: a body can have a recursive type in it
that binds the name of the other variable.
Limit, with a named error: a dense cycle makes the nested types grow
fast (4 types that each refer to each of the 4 need 3613 bodies, 5 need
8 million). A type of more than 10000 bodies, or of more than 256
nested named types, is refused: "the type ... is too large". A ring of
32 types needs 127 bodies, and a cycle of 5 types as in a syntax tree
needs fewer than 400. The same limit turns a stack overflow for 700
nested `data` types into the named error.
Tests: data_types_that_refer_to_each_other_run (11 programs as wasm and
in the interpreter, with a cycle of 3 types in each of the 6 orders of
its names, and 4 refused programs), the 2 limits, and a case across
modules. 638 tests pass; the all-target count is 635.
Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
|
Caution Review failedThe pull request is closed.
Warning Some tools did not complete. Review the errors below.
 |
|
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Summary
datatypes that refer to each other were refused by name (#438). They are now accepted, behind the flag--unstable-coreas each recursive type is.The core has no new former, and the checker and the 2 backends do not change. Only the type expansion of the desugarer changes.
How
The types of a cycle become nested
mutypes (Bekic's construction), in the order of their names. Adatatype that is entered hides, for its body, eachdatatype in progress that comes after it: in that body, such a type is not a variable, and it is expanded again. ForForestbeforeTree:The reason for this order rule: with iso-recursive types, a type is not equal to its unfolding. So the unfolding of each type must have the other types in it as they are. With the rule it does, for a cycle of each form and each number of types. A field of a constructor then has the type that its declaration names, and no fold or unfold is missing or in excess.
2 more changes follow from the nesting:
datatype is folded when its own expansion refers to it. A type whose type is the recursive type of anotherdatatype (data B = MkB(A)) is not folded.Limit, with a named error
A dense cycle makes the nested types grow fast.
A type of more than 10000 bodies, or of more than 256 nested named types, is refused: "the type
T4is too large ...". Without the limit, the dense cycle of 5 does not end, and a ring of 700 types overflows the stack. The depth limit also applies todatatypes that do not refer to each other: 700 nesteddatatypes overflowed the stack before this change, and are now the named error.A recursive type of n variables (as the
recgroups of WasmGC) removes the size limit. It is a change of the core language, so it is a decision for the owner and not part of this pull request. The plan document records this next to the D7 ratification.Verification
cargo test --workspace --no-fail-fast: 638 passed, 0 failed.cargo fmt --all --checkandcargo clippy --workspace --all-targets: clean.scripts/status-gate.sh: 635 all-target tests (1 more than before).scripts/probe-battery.sh: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI).data_types_that_refer_to_each_other_run, each program as wasm and in the interpreter:Forestas aTree, aTreeas aForest.a_recursive_form_with_no_lowering_is_refused_by_name: the 2 limits (the dense cycle of 5, a ring of 300).a_recursive_data_type_crosses_a_module: 2 types that refer to each other, used from another module.Generated by Claude Code