Repository navigation
feat(wasm): closures of each value type, and named functions as values (E9, closures) - #437
Merged
Merged
Conversation
…s (E9, closures)
v2 plan rung E9, the closure half. Recursive types wait for decision D7.
A closure function has the wasm type of its parameter and of its result:
(env: i32, param) -> result. Each closure had the one type
(i32, i32) -> i32, and a lambda with an I64, F32 or F64 parameter or
result was refused. Such a lambda is now behind the flag
`--unstable-core` (check, compile, run), as the plan says for E9.
3 defects of the old lowering are repaired. Each one gave a wrong
program with no error from the checker:
- A named function as a value (`apply(inc, 41)`, `let f = add`,
`add(40)`) gave a module that was not valid (no table). The value is
now a closure cell for a closure function that takes the parameters
1 at a time and then calls the function. An extern function also.
- A lambda in a lambda gave a module that was not valid (unknown
function): the list of closure functions was copied before its loop.
- A local with the name of a function of the module was called as that
function (0, where the interpreter gave 42).
Cause of the second defect, also removed: each function body was
compiled 2 times, to count its locals, so each lambda was added to the
module 2 times. A body is now compiled 1 time, and the type section is
written after the bodies, because a closure adds the type of its
signature while its body is compiled.
The driver has `Features { unstable_core }`, `check_program_with`,
`load_program_with`, `load_source_with`, and the load error
`UnstableCore`.
Tests: closures.rs (4 tests, wasm and interpreter). The E5 matrix has
closure parameter, closure result and captured value columns for each
value type: 3396 cases, 0 disagreements. 2 tests that pinned the old
refusal now check the limit that remains and the flag.
628 tests pass; the all-target count is 625.
Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
Contributor
|
Caution Review failedThe pull request is closed.
Warning Some tools did not complete. Review the errors below.
 |
|
Codex Review Summary: ❌ FailedThis 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. |
|
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. |
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
…(E9, D7) (#438) ## Summary v2 plan rung E9, the recursive type half. Decision D7 is ratified (owner, 2026-11-10): iso-recursive types, with fold and unfold from the desugarer. The closure half merged in #437. A `data` type that refers to itself was refused. It is now the core type `mu X. T`, behind the flag `--unstable-core`. ``` data IntList = Nil | Cons(I32, IntList) fn sum(l: IntList): I32 = match l of | Nil => 0 | Cons(h, t) => h + sum(t) end fn main(): I32 = sum(Cons(1, Cons(2, Cons(3, Nil)))) ``` `ephapax run --unstable-core` prints 6, as wasm and in the interpreter. This is the acceptance program of the rung. ## How - **Core** (`ephapax-syntax`): `Ty::Mu { var, body }`, `ExprKind::Fold { ty, value }`, `ExprKind::Unfold(e)`. - **Desugarer**: a `data` type that is entered again during its own expansion becomes `mu #Name. body`. A constructor gets a `fold`, and a `match` gets an `unfold` on its scrutinee. A `data` type that does not refer to itself has the same lowering as before. - **Checker**: `fold[mu X. T](e)` needs `e : T[X := mu X. T]`, and `unfold` gives that type. 2 recursive types are equal when their bodies are, up to the name of the bound variable. A recursive type is not equal to its unfolding. - **Backends**: a value of a recursive type is a pointer to its unfolding (a sum cell, a pair). Fold and unfold do nothing at run time, in wasm and in the interpreter. - **Linearity**: `mu X. T` is linear when `T` is linear with `X` not linear. This is the least fixed point that the plan gives for the grade of a recursive type. ## Type parameters `data List(a) = Nil | Cons(a, List(a))` works at each element type. - The annotation of a constructor of a recursive `data` type binds the type parameters (`forall a. ...`). The checker gives each one a type from the use of the value, and the `fold` makes the annotations of the injections agree. - In the body of a `data` type, a type parameter now stands for its argument at each depth. Before, only a parameter that was a whole field got its argument: `data Box(a) = MkBox((a, a))` kept `a`. ## Refused by name | Form | Error | |---|---| | 2 `data` types that refer to each other | the `data` types Tree -> Forest -> Tree refer to each other | | a type that refers to itself with other type arguments | recursive type `Grow` refers to itself with other type arguments | | a `type` alias that refers to itself | recursive type alias ... only a `data` type can refer to itself | A `type` alias in the cycle of a `data` type is permitted: it is transparent. ## The flag Without `--unstable-core`, `check`, `compile` and `run` refuse a program that uses a recursive type: "behind the flag `--unstable-core`: the recursive type `IntList` ...". A declaration with no use is accepted. The probe `rec1` now has this verdict, so its 2 rows in `tests/probes/expectations.tsv` change from `error:DesugarError` to `error:UnstableCore`, and `scripts/probe-battery.sh` knows that kind. ## Verification - `cargo test --workspace --no-fail-fast`: 636 passed, 0 failed. - `cargo fmt --all --check` and `cargo clippy --workspace --all-targets`: clean. - `scripts/status-gate.sh`: 633 all-target tests (8 more than before). - `scripts/probe-battery.sh`: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI). `scripts/test-probe-battery.sh`: 4 passed. - New file `recursive_types.rs`, 6 tests, each program as wasm and in the interpreter: - `a_recursive_data_type_runs` (10 programs: sum, range, append, map with a closure, guards and literals, values in pairs, lists and closures, 3 constructors, an alias in the cycle); - `a_recursive_data_type_with_type_parameters_runs` (7 programs: Bool, I64, F64, a list of lists, a rose tree, a generic function, a type from its use); - `a_recursive_data_type_crosses_a_module` (5 programs); - `a_recursive_type_keeps_the_linear_rules` (a list of strings: used 2 times, a part not consumed, not used, and a region escape are each refused); - `a_recursive_form_with_no_lowering_is_refused_by_name`; - `a_recursive_data_type_is_behind_the_flag`. - `linearity_holes.rs`: the `rec1` test now checks the flag, and 1 new test checks the 3 named desugar errors. - `ephapax-ir`: a round trip test for `fold`, `unfold`, `mu` and a bound type parameter. ## Not in this pull request - 2 `data` types that refer to each other (refused by name). - A positivity check: `data Self = MkSelf(Self -> I32)` is accepted. - The typed-wasm gate for E9 (it follows E8, which waits for the upstream typed-wasm change). - Promotion out of `--unstable-core` (it waits for proof rung P17). --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
v2 plan rung E9, the closure half. The recursive type half waits for decision D7.
--unstable-coreexists. A lambda with an I64, F32 or F64 parameter or result is behind it.1. Typed closure signatures
A closure is a cell
(table index @ 0, environment @ 4). Its closure function is(env: i32, param) -> result. Each closure had the one type(i32, i32) -> i32, and a lambda with an I64, F32 or F64 parameter or result was refused. Nowcall_indirectuses the type of the callee, and wasm checks it at each call.2. A named function as a value
apply(inc, 41)let f = add in f(40, 2)let f = add(40) in f(2)Each of these programs passed the checker and ran in the interpreter. The value is now a closure cell for a closure function that takes the parameters 1 at a time and then calls the function (
fn(a) -> fn(b) -> add(a, b)). One closure function is made for each name, at its first use. An extern function is a value in the same way.3. Other defects
fn(a: I32) -> fn(b: I32) -> a + bfand a top-level functionf, thenf(x)f(0, interpreter 42)Cause of the first one, also removed: each function body was compiled 2 times to count its locals, so each lambda was added to the module 2 times, and the loop over the closure functions ran on a copy of the list. A body is now compiled 1 time. The type section is written after the bodies, because a closure adds the type of its signature while its body is compiled.
4. The flag
--unstable-coreThe plan puts E9 behind
--unstable-coreuntil proof rung P17 is closed. The flag is a global option of the command line tool, forcheck,compileandrun.--unstable-core: a lambda with an I64, F32 or F64 parameter or result".The driver has
Features { unstable_core },check_program_with,load_program_with,load_source_with, and the load errorUnstableCore. The gate is in the driver.ephapax_wasm::compile_modulelowers each form.Verification
cargo test --workspace --no-fail-fast: 628 passed, 0 failed.cargo fmt --all --checkandcargo clippy --workspace --all-targets: clean.scripts/status-gate.sh: 625 all-target tests (4 more than before).scripts/probe-battery.sh: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI).closures.rs, 4 tests, each program as wasm and in the interpreter:a_named_function_is_a_value,a_lambda_in_a_lambda_runs,a_local_hides_a_function_of_the_same_name,a_wide_lambda_is_behind_the_flag.typed_codegen_matrix.rs) has closure parameter, closure result and captured value columns for each value type: 3396 cases, 0 disagreements between wasm and the interpreter.check_rejects_what_typed_codegen_cannot_lowernow uses the limit that remains (a literal pattern on a wide payload).check_sees_the_limits_of_the_monomorphic_copiesnow checks the flag text, and that the copy runs with the flag.Not in this pull request
Generated by Claude Code