diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 2582d1a..d441664 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *625 tests* (`+cargo test --workspace --all-targets+`); +* Total: *633 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 625 +* Documented all-target tests: 633 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 625 pass, 0 fail +* [x] cargo test –workspace –all-targets — 633 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc index 01ab624..85abe4d 100644 --- a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc +++ b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc @@ -1395,6 +1395,8 @@ Ephapax's soundness statements are *theory* under PROOF-POLICY §1: the typing j === D7 — Recursive types +*Ratified 2026-11-10 (owner):* the recommended option, iso-recursive `TMu` with fold/unfold inserted by desugar. Its first use is rung E9 in the Rust implementation (gate `src/ephapax-cli/tests/recursive_types.rs`), behind `--unstable-core`. In that step a `data` type can refer only to itself: a cycle through another `data` type, and a reference with other type arguments, are named errors. + [cols="3,1,1,4",options="header"] |=== |Option |(a) |(b) |Comment diff --git a/ephapax-linear/src/affine.rs b/ephapax-linear/src/affine.rs index d80e81e..4943519 100644 --- a/ephapax-linear/src/affine.rs +++ b/ephapax-linear/src/affine.rs @@ -179,7 +179,10 @@ impl AffineChecker { self.walk_expr(inner); } - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => { + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } + | ExprKind::Unfold(value) => { self.walk_expr(value); } diff --git a/ephapax-linear/src/linear.rs b/ephapax-linear/src/linear.rs index 331adb6..05803db 100644 --- a/ephapax-linear/src/linear.rs +++ b/ephapax-linear/src/linear.rs @@ -210,7 +210,10 @@ impl LinearChecker { } // --- Sum injections --- - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => { + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } + | ExprKind::Unfold(value) => { self.walk_expr(value); } diff --git a/scripts/probe-battery.sh b/scripts/probe-battery.sh index cf8195e..3a46739 100755 --- a/scripts/probe-battery.sh +++ b/scripts/probe-battery.sh @@ -34,7 +34,9 @@ # Verdicts: ok | ok: | error: | crash:[-stack-overflow] # | timeout | no-module | unavailable:no-wasmtime # Kinds: InvalidWasm AnnotationNotEnforced CodegenError DesugarError -# TypeError ParseError RuntimeError Other, and Trap: (wasm-run) +# TypeError ParseError RuntimeError UnstableCore Other, and +# Trap: (wasm-run). UnstableCore: a form that is behind the +# flag `--unstable-core` (v2 plan rung E9), which the battery does not give. # # Output: a TSV on stdout (or --out FILE), one line per row: # file command exit verdict status baseline target diagnostic @@ -74,7 +76,7 @@ while [ $# -gt 0 ]; do --bin) bin="$2"; shift 2 ;; --out) out="$2"; shift 2 ;; --update) update=1; shift ;; - -h|--help) sed -n '2,59p' "$0"; exit 0 ;; + -h|--help) sed -n '2,62p' "$0"; exit 0 ;; *) echo "probe-battery: unknown argument $1" >&2; exit 3 ;; esac done @@ -154,6 +156,7 @@ classify() { elif grep -q 'Type error' <<<"$text"; then kind=TypeError elif grep -qi 'parse error' <<<"$text"; then kind=ParseError elif grep -q 'Runtime error' <<<"$text"; then kind=RuntimeError + elif grep -q 'behind the flag `--unstable-core`' <<<"$text"; then kind=UnstableCore fi echo "error:$kind" } diff --git a/src/ephapax-analysis/src/escape.rs b/src/ephapax-analysis/src/escape.rs index 0dd0ce0..6b3f68b 100644 --- a/src/ephapax-analysis/src/escape.rs +++ b/src/ephapax-analysis/src/escape.rs @@ -134,7 +134,10 @@ impl EscapeAnalysis { Self::analyze_expr(inner, escaping, in_escaping_context); } - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => { + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } + | ExprKind::Unfold(value) => { Self::analyze_expr(value, escaping, in_escaping_context); } diff --git a/src/ephapax-analysis/src/free_vars.rs b/src/ephapax-analysis/src/free_vars.rs index 2fd1263..3f89e18 100644 --- a/src/ephapax-analysis/src/free_vars.rs +++ b/src/ephapax-analysis/src/free_vars.rs @@ -139,7 +139,10 @@ impl FreeVarAnalysis { Self::collect(right, free, bound); } - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => { + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } + | ExprKind::Unfold(value) => { Self::collect(value, free, bound); } diff --git a/src/ephapax-analysis/src/liveness.rs b/src/ephapax-analysis/src/liveness.rs index a97632c..0649a75 100644 --- a/src/ephapax-analysis/src/liveness.rs +++ b/src/ephapax-analysis/src/liveness.rs @@ -144,7 +144,10 @@ impl LivenessAnalysis { Self::compute(right, live); } - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => { + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } + | ExprKind::Unfold(value) => { Self::compute(value, live); } diff --git a/src/ephapax-cli/src/main.rs b/src/ephapax-cli/src/main.rs index 3bd1feb..3e69124 100644 --- a/src/ephapax-cli/src/main.rs +++ b/src/ephapax-cli/src/main.rs @@ -42,8 +42,9 @@ struct Cli { verbose: bool, /// Accept the forms of the core language that the proofs do not cover - /// yet (v2 plan rung E9): a lambda with an I64, F32 or F64 parameter - /// or result. Applies to `run`, `check` and `compile`. + /// yet (v2 plan rung E9): a recursive `data` type, and a lambda with + /// an I64, F32 or F64 parameter or result. Applies to `run`, `check` + /// and `compile`. #[arg(long, global = true)] unstable_core: bool, } diff --git a/src/ephapax-cli/tests/linearity_holes.rs b/src/ephapax-cli/tests/linearity_holes.rs index d5203ad..59ecda6 100644 --- a/src/ephapax-cli/tests/linearity_holes.rs +++ b/src/ephapax-cli/tests/linearity_holes.rs @@ -419,21 +419,63 @@ fn list_index_from_linear_list_rejected() { assert_cli_rejects("listidx", LISTIDX); } +/// `rec1` has a `data` type that refers to itself. It aborted the compiler +/// with a stack overflow, and then it was a named desugar error. Since +/// rung E9 the core has recursive types: the probe desugars and checks, +/// and the command line refuses it by name without `--unstable-core`. #[test] -fn rec1_is_a_named_desugar_error_not_a_crash() { - match pipeline(REC1) { - Err(PipelineError::Desugar(DesugarError::RecursiveType { name, .. })) => { - assert_eq!(name, "L"); - } - other => panic!("expected DesugarError::RecursiveType, got {other:?}"), - } +fn rec1_is_behind_the_flag_not_a_crash() { + assert!(pipeline(REC1).is_ok(), "{:?}", pipeline(REC1)); let stderr = assert_cli_rejects("rec1", REC1); assert!( - stderr.contains("recursive type `L`"), - "stderr should name the recursive type:\n{stderr}" + stderr.contains("behind the flag `--unstable-core`: the recursive type `L`"), + "stderr should name the flag and the recursive type:\n{stderr}" + ); + + let dir = tempfile::tempdir().expect("tempdir"); + let path = write_probe(dir.path(), "rec1", REC1); + let out = Command::new(ephapax_bin()) + .args(["check", "--unstable-core"]) + .arg(&path) + .output() + .expect("run ephapax check"); + assert!( + out.status.success(), + "with the flag:\n{}", + String::from_utf8_lossy(&out.stderr) ); } +/// Each recursive form that has no lowering is a named desugar error. +#[test] +fn a_recursive_form_with_no_lowering_is_a_named_desugar_error() { + let refused = |src: &str| match pipeline(src) { + Err(PipelineError::Desugar(error)) => error, + other => panic!("expected a desugar error, got {other:?}"), + }; + // 2 `data` types that refer to each other. + assert!(matches!( + refused( + "data Tree = Leaf | Node(Forest)\ndata Forest = FNil | FCons(Tree, Forest)\n\ + fn f(t: Tree): I32 = 0\nfn main(): I32 = 0\n" + ), + DesugarError::MutualRecursion { cycle } if cycle == "Tree -> Forest -> Tree" + )); + // A `data` type that refers to itself with other type arguments. + assert!(matches!( + refused( + "data Grow(a) = Stop | More(Grow((a, a)))\nfn f(t: Grow(I32)): I32 = 0\n\ + fn main(): I32 = 0\n" + ), + DesugarError::NonRegularRecursion { name, .. } if name == "Grow" + )); + // A `type` alias that refers to itself with no `data` type between. + assert!(matches!( + refused("type A = (I32, B)\ntype B = (I32, A)\nfn f(t: A): I32 = 0\nfn main(): I32 = 0\n"), + DesugarError::RecursiveAlias { .. } + )); +} + #[test] fn nested_data_application_is_not_mistaken_for_recursion() { let src = "\ diff --git a/src/ephapax-cli/tests/recursive_types.rs b/src/ephapax-cli/tests/recursive_types.rs new file mode 100644 index 0000000..4e1f531 --- /dev/null +++ b/src/ephapax-cli/tests/recursive_types.rs @@ -0,0 +1,455 @@ +// SPDX-License-Identifier: MPL-2.0 +// Owner: Jonathan D.A. Jewell +// +// recursive_types.rs: v2 plan rung E9, recursive types (decision D7). +// +// A `data` type that refers to itself is an iso-recursive type +// `mu X. T` in the core. The desugarer puts a `fold` at each constructor +// and an `unfold` at each `match`. A value of the type is a pointer to +// its unfolding (a sum cell, a pair), so `fold` and `unfold` do nothing +// at run time. Each program here runs as wasm and in the interpreter, +// with the flag `--unstable-core`, and the 2 must print the expected +// value. + +use std::path::Path; +use std::process::{Command, Output}; + +/// Run the `ephapax` binary with `args`, in the directory `dir`. +fn ephapax(dir: &Path, args: &[&str]) -> Output { + Command::new(env!("CARGO_BIN_EXE_ephapax")) + .current_dir(dir) + .args(args) + .output() + .expect("spawn ephapax") +} + +/// Write each program (name, text, output) into `dir` and run it as wasm +/// and in the interpreter, with the flag `--unstable-core`. +fn each_runs(dir: &Path, programs: &[(&str, String, &str)]) { + for (name, text, want) in programs { + let file = format!("{name}.eph"); + std::fs::write(dir.join(&file), text).expect("write program"); + for mode in [&["run"][..], &["run", "--interp"]] { + let args: Vec<&str> = [mode, &["--unstable-core", file.as_str()]].concat(); + let out = ephapax(dir, &args); + assert!( + out.status.success(), + "{name} under {args:?} failed:\n{}", + String::from_utf8_lossy(&out.stderr) + ); + let stdout = String::from_utf8_lossy(&out.stdout); + assert_eq!(stdout.trim(), *want, "{name} under {args:?}"); + } + } +} + +/// `check` refuses `text` with a message that has `error` in it. +fn check_refuses(name: &str, text: &str, error: &str) { + let tmp = tempfile::tempdir().expect("tempdir"); + let file = format!("{name}.eph"); + std::fs::write(tmp.path().join(&file), text).expect("write program"); + let out = ephapax(tmp.path(), &["check", "--unstable-core", &file]); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success() && stderr.contains(error), + "{name}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ); +} + +/// A list of I32, and the sum of its elements. +const INT_LIST: &str = "data IntList = Nil | Cons(I32, IntList)\n\n\ + fn sum(l: IntList): I32 = match l of | Nil => 0 | Cons(h, t) => h + sum(t) end\n\n"; + +/// The acceptance program of the rung (the sum of an IntList), and the +/// other uses of a `data` type that refers to itself. +#[test] +fn a_recursive_data_type_runs() { + let tmp = tempfile::tempdir().expect("tempdir"); + let with_list = |rest: &str| format!("{INT_LIST}{rest}\n"); + each_runs( + tmp.path(), + &[ + ( + "sum", + with_list("fn main(): I32 = sum(Cons(1, Cons(2, Cons(3, Nil))))"), + "6", + ), + // A function makes the value, 1 cell for each call. + ( + "range", + with_list( + "fn range(n: I32): IntList = if n == 0 then Nil else Cons(n, range(n - 1))\n\n\ + fn main(): I32 = sum(range(20))", + ), + "210", + ), + ( + "append", + with_list( + "fn append(a: IntList, b: IntList): IntList =\n \ + match a of | Nil => b | Cons(h, t) => Cons(h, append(t, b)) end\n\n\ + fn main(): I32 = sum(append(Cons(1, Cons(2, Nil)), Cons(30, Cons(9, Nil))))", + ), + "42", + ), + // With a closure, and with a named function as a value. + ( + "map", + with_list( + "fn map(f: I32 -> I32, l: IntList): IntList =\n \ + match l of | Nil => Nil | Cons(h, t) => Cons(f(h), map(f, t)) end\n\n\ + fn apply(f: IntList -> I32, l: IntList): I32 = f(l)\n\n\ + fn main(): I32 = apply(sum, map(fn(x: I32) -> x * 2, Cons(1, Cons(20, Nil))))", + ), + "42", + ), + // A guard, a literal in a pattern, and an arm for each constructor. + ( + "guard", + with_list( + "fn pos(l: IntList): I32 =\n match l of\n \ + | Cons(h, t) if h > 0 => 1 + pos(t)\n | Cons(h, t) => pos(t)\n \ + | Nil => 0\n end\n\n\ + fn zeros(l: IntList): I32 =\n match l of\n \ + | Cons(0, t) => 1 + zeros(t)\n | Cons(h, t) => zeros(t)\n | Nil => 0\n end\n\n\ + fn empty(l: IntList): Bool = match l of | Nil => true | _ => false end\n\n\ + fn main(): I32 =\n let l = Cons(1, Cons(0, Cons(5, Nil)))\n \ + if empty(l) then 0 else pos(l) * 10 + zeros(l)", + ), + "21", + ), + // In a pair, in a list, and captured by a closure. + ( + "inside", + with_list( + "fn main(): I32 =\n let p = (Cons(20, Nil), Cons(1, Nil))\n \ + let xs = [Cons(10, Nil), Cons(2, Nil)]\n let l = Cons(9, Nil)\n \ + let f = fn(n: I32) -> n + sum(l)\n \ + f(sum(p.0) + sum(p.1) + sum(xs[0]) + sum(xs[1]))", + ), + "42", + ), + // 3 constructors, 2 of them with the type in a field. + ( + "tree", + "data T = A | B(I32, T) | C(T, T)\n\n\ + fn size(t: T): I32 =\n match t of\n | A => 1\n | B(n, r) => n + size(r)\n \ + | C(l, r) => size(l) + size(r)\n end\n\n\ + fn main(): I32 = size(C(B(30, A), C(B(8, A), A)))\n" + .to_string(), + "41", + ), + // The constructor with the field is not the last one. + ( + "first_ctor", + "data Wrap = W(I32, Wrap) | End\n\n\ + fn depth(w: Wrap): I32 = match w of | End => 0 | W(n, r) => n + depth(r) end\n\n\ + fn main(): I32 = depth(W(40, W(2, End)))\n" + .to_string(), + "42", + ), + ( + "nat", + "data Nat = Z | S(Nat)\n\n\ + fn to_i(n: Nat): I32 = match n of | Z => 0 | S(m) => 1 + to_i(m) end\n\n\ + fn add(a: Nat, b: Nat): Nat = match a of | Z => b | S(m) => S(add(m, b)) end\n\n\ + fn main(): I32 = to_i(add(S(S(Z)), S(Z)))\n" + .to_string(), + "3", + ), + // A `type` alias in the cycle is transparent: the recursion is + // that of the `data` type. + ( + "alias", + "type P = (I32, T)\n\ndata T = End | More(P)\n\n\ + fn depth(t: T): I32 = match t of | End => 0 | More(p) => 1 + depth(p.1) end\n\n\ + fn of_pair(p: P): I32 = depth(p.1)\n\n\ + fn main(): I32 = of_pair((1, More((2, More((3, End))))))\n" + .to_string(), + "2", + ), + ], + ); +} + +/// A `data` type with type parameters that refers to itself. The type +/// arguments of a constructor come from its use: `Nil` is a list of I64 +/// in one place and a list of lists in another. +#[test] +fn a_recursive_data_type_with_type_parameters_runs() { + let tmp = tempfile::tempdir().expect("tempdir"); + let with_list = |rest: &str| format!("data List(a) = Nil | Cons(a, List(a))\n\n{rest}\n"); + each_runs( + tmp.path(), + &[ + ( + "bool", + with_list( + "fn all(l: List(Bool)): Bool =\n \ + match l of | Nil => true | Cons(h, t) => h && all(t) end\n\n\ + fn main(): I32 = if all(Cons(true, Cons(true, Nil))) then 42 else 0", + ), + "42", + ), + // An element keeps its width in the cell. + ( + "i64", + with_list( + "fn sum(l: List(I64)): I64 =\n match l of\n \ + | Nil => 5000000000 - 5000000000\n | Cons(h, t) => h + sum(t)\n end\n\n\ + fn main(): I64 = sum(Cons(5000000000, Cons(5000000000, Nil)))", + ), + "10000000000i64", + ), + ( + "f64", + with_list( + "fn sum(l: List(F64)): F64 =\n \ + match l of | Nil => 0.0 | Cons(h, t) => h + sum(t) end\n\n\ + fn main(): F64 = sum(Cons(1.5, Cons(40.5, Nil)))", + ), + "42", + ), + // A list of lists: the type is an argument of itself. + ( + "nested", + with_list( + "fn len(l: List(List(I32))): I32 =\n \ + match l of | Nil => 0 | Cons(h, t) => 1 + len(t) end\n\n\ + fn main(): I32 = len(Cons(Cons(1, Nil), Cons(Nil, Nil)))", + ), + "2", + ), + // A recursive type as the argument of a recursive type. + ( + "rose", + with_list( + "data Rose = R(I32, List(Rose))\n\n\ + fn size(r: Rose): I32 = match r of | R(v, kids) => 1 + sizes(kids) end\n\n\ + fn sizes(l: List(Rose)): I32 =\n \ + match l of | Nil => 0 | Cons(h, t) => size(h) + sizes(t) end\n\n\ + fn main(): I32 = size(R(1, Cons(R(2, Nil), Cons(R(3, Nil), Nil))))", + ), + "3", + ), + // A generic function: 1 copy for each element type. + ( + "generic", + with_list( + "fn rev(l: List(T), acc: List(T)): List(T) =\n \ + match l of | Nil => acc | Cons(h, t) => rev(t, Cons(h, acc)) end\n\n\ + fn head(l: List(I32)): I32 = match l of | Nil => 0 | Cons(h, t) => h end\n\n\ + fn first(l: List(Bool)): Bool =\n \ + match l of | Nil => false | Cons(h, t) => h end\n\n\ + fn main(): I32 =\n \ + if first(rev(Cons(false, Cons(true, Nil)), Nil))\n \ + then head(rev(Cons(1, Cons(42, Nil)), Nil))\n else 0", + ), + "42", + ), + // No annotation gives the type: the uses of the value do. + ( + "from_use", + with_list( + "fn main(): I32 =\n let l = Cons(40, Cons(2, Nil))\n \ + match l of\n | Nil => 0\n \ + | Cons(h, t) => match t of | Nil => h | Cons(g, u) => h + g end\n end", + ), + "42", + ), + ], + ); +} + +/// A module names a recursive `data` type of another module by the rule +/// of each `data` type: an import, and `pub`. +#[test] +fn a_recursive_data_type_crosses_a_module() { + let tmp = tempfile::tempdir().expect("tempdir"); + std::fs::write( + tmp.path().join("lib.eph"), + "module lib\n\npub data IntList = Nil | Cons(I32, IntList)\n\n\ + pub data List(a) = LNil | LCons(a, List(a))\n\n\ + pub fn sum(l: IntList): I32 = match l of | Nil => 0 | Cons(h, t) => h + sum(t) end\n\n\ + pub fn one(n: I32): IntList = Cons(n, Nil)\n", + ) + .expect("write module"); + let app = |name: &str, head: &str, main: &str| { + format!("module {name}\n\n{head}\nfn main(): I32 = {main}\n") + }; + each_runs( + tmp.path(), + &[ + ( + "plain", + app("plain", "import lib\n", "sum(Cons(40, one(2)))"), + "42", + ), + ( + "qualified", + app( + "qualified", + "import lib\n", + "sum(lib.Cons(40, lib.Cons(2, lib.Nil)))", + ), + "42", + ), + ( + "listed", + app( + "listed", + "import lib(IntList, sum)\n\n\ + fn len(l: IntList): I32 = match l of | Nil => 0 | Cons(h, t) => 1 + len(t) end\n", + "sum(Cons(40, Nil)) + len(Cons(1, Cons(2, Nil)))", + ), + "42", + ), + ( + "parameters", + app( + "parameters", + "import lib\n\nfn count(l: List(Bool)): I32 =\n match l of\n \ + | LNil => 0\n | LCons(h, t) => (if h then 1 else 0) + count(t)\n end\n", + "count(LCons(true, LCons(false, LCons(true, LNil))))", + ), + "2", + ), + // A declaration of the module hides the imported type. + ( + "hidden", + app( + "hidden", + "import lib\n\ndata IntList = Mine(I32)\n", + "match Mine(42) of | Mine(n) => n end", + ), + "42", + ), + ], + ); +} + +/// A recursive type with a linear component is linear: a value is used +/// 1 time, each part of it is consumed, and it cannot leave its region. +#[test] +fn a_recursive_type_keeps_the_linear_rules() { + let list = "data SList = SNil | SCons(String@r, SList)\n\n"; + let tmp = tempfile::tempdir().expect("tempdir"); + each_runs( + tmp.path(), + &[( + "consumed", + format!( + "{list}fn total(l: SList): I32 =\n match l of\n | SNil => 0\n \ + | SCons(s, t) => String.len(&s) + (let _ = drop(s) in total(t))\n end\n\n\ + fn main(): I32 =\n region r {{\n \ + total(SCons(String.new@r(\"ab\"), SCons(String.new@r(\"abc\"), SNil)))\n }}\n" + ), + "5", + )], + ); + + // (name, functions, error) + for (name, functions, error) in [ + ( + "used_2_times", + "fn two(l: SList): (SList, SList) = (l, l)\n\nfn main(): I32 = 0\n", + "Linear variable `l` used more than once", + ), + ( + "tail_not_consumed", + "fn first(l: SList): I32 =\n \ + match l of | SNil => 0 | SCons(s, t) => let _ = drop(s) in 1 end\n\n\ + fn main(): I32 = 0\n", + "Linear variable `t` not consumed", + ), + ( + "not_used", + "fn ignore(l: SList): I32 = 0\n\nfn main(): I32 = 0\n", + "Linear variable `l` not consumed", + ), + ( + "leaves_its_region", + "fn main(): I32 =\n let l = region r { SCons(String.new@r(\"ab\"), SNil) }\n 0\n", + "escapes region `r`", + ), + ] { + check_refuses(name, &format!("{list}{functions}"), error); + } + + // A recursive type with no linear component is not linear. + each_runs( + tmp.path(), + &[( + "shared", + format!( + "{INT_LIST}fn main(): I32 =\n let l = Cons(20, Cons(1, Nil))\n sum(l) + sum(l)\n" + ), + "42", + )], + ); +} + +/// The recursive forms that have no lowering yet are refused by name. +#[test] +fn a_recursive_form_with_no_lowering_is_refused_by_name() { + check_refuses( + "each_other", + "data Tree = Leaf | Node(Forest)\n\ndata Forest = FNil | FCons(Tree, Forest)\n\n\ + fn f(t: Tree): I32 = 0\n\nfn main(): I32 = 0\n", + "the `data` types Tree -> Forest -> Tree refer to each other", + ); + check_refuses( + "other_arguments", + "data Grow(a) = Stop | More(Grow((a, a)))\n\n\ + fn f(t: Grow(I32)): I32 = 0\n\nfn main(): I32 = 0\n", + "recursive type `Grow` refers to itself with other type arguments", + ); + check_refuses( + "alias_only", + "type A = (I32, B)\n\ntype B = (I32, A)\n\nfn f(t: A): I32 = 0\n\nfn main(): I32 = 0\n", + "only a `data` type can refer to itself", + ); +} + +/// A recursive `data` type is behind the flag `--unstable-core`: without +/// it, each command refuses the program by name. A declaration with no +/// use is not a use of the flag. +#[test] +fn a_recursive_data_type_is_behind_the_flag() { + let tmp = tempfile::tempdir().expect("tempdir"); + let write = |name: &str, text: &str| { + std::fs::write(tmp.path().join(name), text).expect("write program") + }; + write( + "sum.eph", + &format!("{INT_LIST}fn main(): I32 = sum(Cons(1, Nil))\n"), + ); + // No function has the type in its signature: the body shows it. + write( + "body.eph", + "data IntList = Nil | Cons(I32, IntList)\n\n\ + fn main(): I32 = match Cons(1, Nil) of | Nil => 0 | Cons(h, t) => h end\n", + ); + for file in ["sum.eph", "body.eph"] { + for command in [&["check"][..], &["compile"], &["run"], &["run", "--interp"]] { + let args: Vec<&str> = [command, &[file]].concat(); + let out = ephapax(tmp.path(), &args); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success() + && stderr.contains("behind the flag `--unstable-core`") + && stderr.contains("the recursive type `IntList`"), + "{args:?}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ); + } + } + + write( + "declared.eph", + "data IntList = Nil | Cons(I32, IntList)\n\nfn main(): I32 = 42\n", + ); + let out = ephapax(tmp.path(), &["run", "declared.eph"]); + assert_eq!(String::from_utf8_lossy(&out.stdout).trim(), "42"); +} diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index 8e3a3a8..3dd66f5 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -135,12 +135,22 @@ pub enum DesugarError { #[error("member access on a non-module expression is not supported (only `Module.member` qualified access)")] FieldAccessOnNonModule, - /// A `data` declaration (or `type` alias) refers to itself. The core - /// has no recursive types: the binary-sum encoding expands every - /// named type structurally, so a self-reference would expand forever - /// (probe `rec1` used to abort with a stack overflow). - #[error("recursive type `{name}` is not supported: the core type language has no recursive types (expansion cycle: {cycle})")] - RecursiveType { name: String, cycle: String }, + /// A `type` alias refers to itself, with no `data` type in the cycle. + /// A recursive type is folded at a constructor, and an alias has none. + /// (Probe `rec1` used to abort with a stack overflow.) + #[error("recursive type alias `{name}` is not supported: only a `data` type can refer to itself (expansion cycle: {cycle})")] + RecursiveAlias { name: String, cycle: String }, + + /// 2 or more `data` types refer to each other. A `data` type can + /// refer to itself (v2 plan rung E9); a cycle through another `data` + /// type has no lowering yet. + #[error("the `data` types {cycle} refer to each other, which is not supported yet: a recursive `data` type can refer only to itself (a `type` alias in the cycle is permitted)")] + MutualRecursion { cycle: String }, + + /// A `data` type refers to itself with other type arguments + /// (`data Grow(a) = More(Grow([a]))`): its expansion does not end. + #[error("recursive type `{name}` refers to itself with other type arguments, which is not supported (expansion cycle: {cycle})")] + NonRegularRecursion { name: String, cycle: String }, } // ========================================================================= @@ -325,6 +335,39 @@ impl DataRegistry { // Desugarer // ========================================================================= +/// A named type whose body is being expanded by `desugar_named_type`. +#[derive(Debug, Clone)] +struct Expansion { + /// Key of the module that declares the type. + home: SmolStr, + name: SmolStr, + /// The type arguments of a `data` type, as core types. `None`: a + /// `type` alias. + args: Option>, + /// The type of each type parameter of a `data` type: the type that a + /// type variable stands for in its body, at each depth. + params: HashMap, + /// The body referred to the type itself: the type is recursive. + recursive: bool, +} + +/// The variable of the recursive type of the `data` type `name`. A +/// program cannot write this name, so it is not the name of a type +/// parameter or of an extern type. +fn mu_var(name: &str) -> SmolStr { + format!("#{name}").into() +} + +/// `forall p1. .. forall pn. ty`: the annotation `ty` of a constructor, +/// with the type parameters `params` of its `data` type bound. The type +/// checker gives each bound parameter a type that it finds. +fn quantify(ty: Ty, params: &[SmolStr]) -> Ty { + params.iter().rev().fold(ty, |ty, var| Ty::ForAll { + var: var.clone(), + body: Box::new(ty), + }) +} + /// The desugaring pass. /// /// Call [`Desugarer::desugar_module`] to transform a complete surface module @@ -338,9 +381,9 @@ pub struct Desugarer { /// [`Desugarer::desugar_module`]. module_qualifiers: HashSet, /// Named types currently being expanded by `desugar_named_type`, - /// innermost last, each with the key of the module that declares it. - /// Re-entering one is a recursive type. - expanding: RefCell>, + /// innermost last. A `data` type that is entered again is a recursive + /// type (v2 plan rung E9). + expanding: RefCell>, /// Key of the module whose scope gives a name its meaning: the module /// being desugared, or, while the body of a named type expands, the /// module that declares that type. @@ -891,7 +934,15 @@ impl Desugarer { inner: Box::new(self.desugar_ty(inner)?), mutable: *mutable, }), - SurfaceTy::Var(v) => Ok(Ty::Var(v.clone())), + // In the body of a `data` type, a type parameter of that type + // stands for its type argument. (Only a parameter that was a + // whole field got its argument: `Box((a, a))` kept `a`.) + SurfaceTy::Var(v) => Ok(self + .expanding + .borrow() + .last() + .and_then(|e| e.params.get(v).cloned()) + .unwrap_or_else(|| Ty::Var(v.clone()))), SurfaceTy::List(inner) => Ok(Ty::List(Box::new(self.desugar_ty(inner)?))), SurfaceTy::Tuple(elements) => { let desugared: Vec<_> = elements @@ -978,7 +1029,7 @@ impl Desugarer { got: args.len(), }); } - return self.with_expansion(name, home, |this| this.desugar_ty(aliased)); + return self.expand_alias(name, home, |this| this.desugar_ty(aliased)); } TypeDef::Data { params, ctors } => (params, ctors), }; @@ -991,48 +1042,148 @@ impl Desugarer { }); } - // Build substitution map: type param → concrete type + // The arguments are elaborated before the declaration is entered, + // so a finite nested application (`List(List(I32))`) is valid. let core_args = args .iter() .map(|arg| self.desugar_ty(arg)) .collect::, _>>()?; - let subst: HashMap<&SmolStr, &Ty> = params.iter().zip(core_args.iter()).collect(); // Build right-nested sum from constructor field types - self.with_expansion(name, home, |this| this.build_sum_type(ctors, &subst)) + self.expand_data(name, home, params, core_args, |this| { + this.build_sum_type(ctors) + }) } - /// Run `f` with the named type `name` of the module `home` pushed on - /// the expansion stack, and with the names of `home` in scope. Fails - /// with [`DesugarError::RecursiveType`] if the same declaration is - /// already being expanded, including non-regular recursion with - /// changing arguments. Arguments are elaborated before entering the - /// declaration, so finite nested applications remain valid. Errors - /// propagate after removing this expansion from the stack. - fn with_expansion( + /// The names of the expansions from `start`, then `name`: the cycle + /// that an error shows. + fn cycle(stack: &[Expansion], start: usize, name: &str) -> String { + let mut names: Vec<&str> = stack[start..].iter().map(|e| e.name.as_str()).collect(); + names.push(name); + names.join(" -> ") + } + + /// Run `f`, which expands the body of the alias `name` of the module + /// `home`, with the names of `home` in scope. An alias that refers to + /// itself with no `data` type between is an error: only a `data` type + /// is recursive. With a `data` type between, the alias is expanded + /// again: the recursion is that of the `data` type, which ends it. + fn expand_alias( &self, name: &SmolStr, home: &SmolStr, - f: impl FnOnce(&Self) -> Result, - ) -> Result { - let key = (home.clone(), name.clone()); + f: impl FnOnce(&Self) -> Result, + ) -> Result { { let stack = self.expanding.borrow(); - if stack.contains(&key) { - let mut cycle: Vec = stack.iter().map(|(_, n)| n.to_string()).collect(); - cycle.push(name.to_string()); - return Err(DesugarError::RecursiveType { + let seen = stack + .iter() + .rposition(|e| e.args.is_none() && e.home == *home && e.name == *name); + if let Some(seen) = seen.filter(|&i| stack[i..].iter().all(|e| e.args.is_none())) { + return Err(DesugarError::RecursiveAlias { name: name.to_string(), - cycle: cycle.join(" -> "), + cycle: Self::cycle(&stack, seen, name), }); } } - self.expanding.borrow_mut().push(key); + self.expanding.borrow_mut().push(Expansion { + home: home.clone(), + name: name.clone(), + args: None, + params: HashMap::new(), + recursive: false, + }); let result = self.in_scope(home, f); self.expanding.borrow_mut().pop(); result } + /// The type of the `data` type `name` of the module `home`, with the + /// type parameters `params`, at the type arguments `args`. `f` builds + /// the sum of its constructors, with the names of `home` in scope and + /// each type parameter as its argument. + /// + /// A reference to the type inside its own body, with the same + /// arguments, is the variable of a recursive type, and the result is + /// then `mu var. body` (v2 plan decision D7: iso-recursive). Not + /// supported, each with its own error: a cycle through another `data` + /// type, and a reference with other arguments. + fn expand_data( + &self, + name: &SmolStr, + home: &SmolStr, + params: &[SmolStr], + args: Vec, + f: impl FnOnce(&Self) -> Result, + ) -> Result { + let is_data = |e: &Expansion| e.args.is_some(); + { + let mut stack = self.expanding.borrow_mut(); + let entered = stack + .iter() + .rposition(|e| is_data(e) && e.home == *home && e.name == *name); + if let Some(entered) = entered { + let cycle = Self::cycle(&stack, entered, name); + let name = name.to_string(); + if stack[entered + 1..].iter().any(is_data) { + return Err(DesugarError::MutualRecursion { cycle }); + } + if stack[entered].args.as_ref() != Some(&args) { + return Err(DesugarError::NonRegularRecursion { name, cycle }); + } + stack[entered].recursive = true; + return Ok(Ty::Var(mu_var(&name))); + } + stack.push(Expansion { + home: home.clone(), + name: name.clone(), + params: params.iter().cloned().zip(args.iter().cloned()).collect(), + args: Some(args), + recursive: false, + }); + } + let body = self.in_scope(home, f); + let recursive = self + .expanding + .borrow_mut() + .pop() + .is_some_and(|e| e.recursive); + let body = body?; + Ok(if recursive { + Ty::Mu { + var: mu_var(name), + body: Box::new(body), + } + } else { + body + }) + } + + /// The recursive type of the `data` type of the constructor `info`, + /// or `None` if that `data` type does not refer to itself. The type + /// parameters of the `data` type are type variables in the result. + fn recursive_ty( + &self, + info: &ConstructorInfo, + ) -> Result, Ty)>, DesugarError> { + let params = match self.registry.get_type(&info.home, &info.data_name) { + Some(TypeInfo { + def: TypeDef::Data { params, .. }, + .. + }) => params.clone(), + _ => { + return Err(DesugarError::UnknownType { + name: info.data_name.to_string(), + }) + } + }; + let args: Vec = params.iter().cloned().map(SurfaceTy::Var).collect(); + let ty = self.in_scope(&info.home, |this| { + this.desugar_named_type(&info.data_name, &args) + })?; + Ok(matches!(ty, Ty::Mu { .. }).then_some((params, ty))) + } + /// Build the right-nested binary sum type for a list of constructors. /// /// `[A, B, C]` → `A + (B + C)` @@ -1040,22 +1191,18 @@ impl Desugarer { /// - Nullary: `()` /// - Single field: the field type /// - Multiple fields: product of field types - fn build_sum_type( - &self, - ctors: &[ConstructorDef], - subst: &HashMap<&SmolStr, &Ty>, - ) -> Result { + fn build_sum_type(&self, ctors: &[ConstructorDef]) -> Result { assert!( !ctors.is_empty(), "data type must have at least one constructor" ); if ctors.len() == 1 { - return self.build_payload_type(&ctors[0].fields, subst); + return self.build_payload_type(&ctors[0].fields); } - let left = self.build_payload_type(&ctors[0].fields, subst)?; - let right = self.build_sum_type(&ctors[1..], subst)?; + let left = self.build_payload_type(&ctors[0].fields)?; + let right = self.build_sum_type(&ctors[1..])?; Ok(Ty::Sum { left: Box::new(left), @@ -1068,41 +1215,14 @@ impl Desugarer { /// - No fields → `()` /// - One field → the field type /// - Multiple fields → right-nested product - fn build_payload_type( - &self, - fields: &[SurfaceTy], - subst: &HashMap<&SmolStr, &Ty>, - ) -> Result { - match fields.len() { - 0 => Ok(Ty::Base(BaseTy::Unit)), - 1 => self.subst_and_desugar_ty(&fields[0], subst), - _ => { - let first = self.subst_and_desugar_ty(&fields[0], subst)?; - let rest_fields = &fields[1..]; - let rest = self.build_payload_type(rest_fields, subst)?; - Ok(Ty::Prod { - left: Box::new(first), - right: Box::new(rest), - }) - } - } - } - - /// Apply type parameter substitution then desugar. - fn subst_and_desugar_ty( - &self, - ty: &SurfaceTy, - subst: &HashMap<&SmolStr, &Ty>, - ) -> Result { - match ty { - SurfaceTy::Var(v) => { - if let Some(replacement) = subst.get(v) { - Ok((*replacement).clone()) - } else { - Ok(Ty::Var(v.clone())) - } - } - other => self.desugar_ty(other), + fn build_payload_type(&self, fields: &[SurfaceTy]) -> Result { + match fields { + [] => Ok(Ty::Base(BaseTy::Unit)), + [field] => self.desugar_ty(field), + [first, rest @ ..] => Ok(Ty::Prod { + left: Box::new(self.desugar_ty(first)?), + right: Box::new(self.build_payload_type(rest)?), + }), } } @@ -1136,14 +1256,29 @@ impl Desugarer { // Build the payload expression let payload = self.build_payload_expr(args, span)?; - // Get the full sum type for the "other side" annotations - let empty_subst: HashMap<&SmolStr, &Ty> = HashMap::new(); let ctors = self.ctors_of(&info)?; + // A value of a recursive type is folded (v2 plan rung E9). The + // type parameters of the `data` type are bound in each annotation: + // the type checker finds a type for each one at this constructor, + // and the fold makes the annotations of the injections agree. + let recursive = self.recursive_ty(&info)?; + let params: &[SmolStr] = recursive.as_ref().map_or(&[], |(params, _)| params); + // Wrap in inl/inr chain based on index. The types of the other // constructors are names of the module that declares the type. - self.in_scope(&info.home, |this| { - this.wrap_injection(payload, info.index, &ctors, &empty_subst, span) + let value = self.in_scope(&info.home, |this| { + this.wrap_injection(payload, info.index, &ctors, params, span) + })?; + Ok(match &recursive { + None => value, + Some((params, ty)) => Expr::new( + ExprKind::Fold { + ty: quantify(ty.clone(), params), + value: Box::new(value), + }, + span, + ), }) } @@ -1170,13 +1305,14 @@ impl Desugarer { } } - /// Wrap a payload in the appropriate chain of inl/inr. + /// Wrap a payload in the appropriate chain of inl/inr. Each annotation + /// binds the type parameters `params` ([`quantify`]). fn wrap_injection( &self, payload: Expr, index: usize, ctors: &[ConstructorDef], - subst: &HashMap<&SmolStr, &Ty>, + params: &[SmolStr], span: Span, ) -> Result { let total = ctors.len(); @@ -1189,10 +1325,10 @@ impl Desugarer { if index == 0 { // First constructor: inl(payload) // The "right" type is the sum of remaining constructors - let right_ty = self.build_sum_type(&ctors[1..], subst)?; + let right_ty = self.build_sum_type(&ctors[1..])?; Ok(Expr::new( ExprKind::Inl { - ty: right_ty, + ty: quantify(right_ty, params), value: Box::new(payload), }, span, @@ -1200,22 +1336,22 @@ impl Desugarer { } else if index == total - 1 { // Last constructor: inr(inr(...inr(payload)...)) // Need (total - 1) layers of inr, but we do it recursively - let left_ty = self.build_payload_type(&ctors[0].fields, subst)?; - let inner = self.wrap_injection(payload, index - 1, &ctors[1..], subst, span)?; + let left_ty = self.build_payload_type(&ctors[0].fields)?; + let inner = self.wrap_injection(payload, index - 1, &ctors[1..], params, span)?; Ok(Expr::new( ExprKind::Inr { - ty: left_ty, + ty: quantify(left_ty, params), value: Box::new(inner), }, span, )) } else { // Middle constructor: inr(... inl(payload) ...) - let left_ty = self.build_payload_type(&ctors[0].fields, subst)?; - let inner = self.wrap_injection(payload, index - 1, &ctors[1..], subst, span)?; + let left_ty = self.build_payload_type(&ctors[0].fields)?; + let inner = self.wrap_injection(payload, index - 1, &ctors[1..], params, span)?; Ok(Expr::new( ExprKind::Inr { - ty: left_ty, + ty: quantify(left_ty, params), value: Box::new(inner), }, span, @@ -1322,7 +1458,14 @@ impl Desugarer { _ => None, }) .ok_or(DesugarError::EmptyMatch)?; - let ctors = self.ctors_of(self.ctor(first_ctor)?)?; + let info = self.ctor(first_ctor)?; + let ctors = self.ctors_of(info)?; + // A value of a recursive type is unfolded before its sum is read + // (v2 plan rung E9). + let core_scrutinee = match self.recursive_ty(info)? { + Some(_) => Expr::new(ExprKind::Unfold(Box::new(core_scrutinee)), span), + None => core_scrutinee, + }; // The constructor index of each arm; `None` for an arm that takes // every constructor. A literal or a tuple pattern at the top of @@ -2515,7 +2658,7 @@ mod expansion_regressions { }; assert!(matches!( Desugarer::with_registry(registry).desugar_ty(&recursive), - Err(DesugarError::RecursiveType { .. }) + Err(DesugarError::NonRegularRecursion { .. }) )); } #[test] @@ -2541,7 +2684,7 @@ mod expansion_regressions { registry.register_type_alias("", "A64".into(), named("A0"), false); assert!(matches!( Desugarer::with_registry(registry).desugar_ty(&named("A0")), - Err(DesugarError::RecursiveType { .. }) + Err(DesugarError::RecursiveAlias { .. }) )); } } diff --git a/src/ephapax-driver/src/qualify.rs b/src/ephapax-driver/src/qualify.rs index 6758563..99b26f1 100644 --- a/src/ephapax-driver/src/qualify.rs +++ b/src/ephapax-driver/src/qualify.rs @@ -182,6 +182,8 @@ fn rename_expr(expr: &mut Expr, scope: &Renames) { | ExprKind::Snd(_) | ExprKind::Inl { .. } | ExprKind::Inr { .. } + | ExprKind::Fold { .. } + | ExprKind::Unfold(_) | ExprKind::If { .. } | ExprKind::Region { .. } | ExprKind::Borrow { .. } diff --git a/src/ephapax-interp/src/lib.rs b/src/ephapax-interp/src/lib.rs index b562a21..49322ff 100644 --- a/src/ephapax-interp/src/lib.rs +++ b/src/ephapax-interp/src/lib.rs @@ -430,6 +430,9 @@ impl Interpreter { ExprKind::Snd(inner) => self.eval_snd(inner), ExprKind::Inl { value, .. } => self.eval_inl(value), ExprKind::Inr { value, .. } => self.eval_inr(value), + // A value of a recursive type is the value of its unfolding: + // `fold` and `unfold` change the type only. + ExprKind::Fold { value, .. } | ExprKind::Unfold(value) => self.eval(value), ExprKind::Case { scrutinee, left_var, diff --git a/src/ephapax-ir/src/lib.rs b/src/ephapax-ir/src/lib.rs index 2cfa638..ff655aa 100644 --- a/src/ephapax-ir/src/lib.rs +++ b/src/ephapax-ir/src/lib.rs @@ -491,6 +491,14 @@ pub fn expr_to_sexpr(expr: &Expr) -> SExpr { ty_to_sexpr(ty), expr_to_sexpr(value), ]), + ExprKind::Fold { ty, value } => SExpr::List(vec![ + SExpr::Atom("fold".into()), + ty_to_sexpr(ty), + expr_to_sexpr(value), + ]), + ExprKind::Unfold(inner) => { + SExpr::List(vec![SExpr::Atom("unfold".into()), expr_to_sexpr(inner)]) + } ExprKind::Case { scrutinee, left_var, @@ -720,6 +728,21 @@ pub fn decode_expr(expr: &SExpr) -> Result { ty: decode_ty(&list[1])?, value: Box::new(decode_expr(&list[2])?), }, + "fold" => { + let [_, ty, value] = &list[..] else { + return Err(SExprError::Invalid("(fold ty e)".into())); + }; + ExprKind::Fold { + ty: decode_ty(ty)?, + value: Box::new(decode_expr(value)?), + } + } + "unfold" => { + let [_, inner] = &list[..] else { + return Err(SExprError::Invalid("(unfold e)".into())); + }; + ExprKind::Unfold(Box::new(decode_expr(inner)?)) + } "case" => { if list.len() != 4 { return Err(SExprError::Invalid("(case scr (x e1) (y e2))".into())); @@ -894,6 +917,11 @@ fn ty_to_sexpr(ty: &Ty) -> SExpr { SExpr::Atom(escape_atom(var)), ty_to_sexpr(body), ]), + Ty::Mu { var, body } => SExpr::List(vec![ + SExpr::Atom("mu".into()), + SExpr::Atom(escape_atom(var)), + ty_to_sexpr(body), + ]), Ty::Unif(id) => SExpr::List(vec![ SExpr::Atom("unif".into()), SExpr::Atom(id.to_string()), @@ -965,6 +993,20 @@ fn decode_ty(expr: &SExpr) -> Result { mutable: true, }), "var" => Ok(Ty::Var(SmolStr::new(atom_string(&list[1])?))), + // `(mu X ty)`, and `(forall a ty)`: the annotation of a + // constructor of a recursive `data` type binds the type + // parameters of that type. + "mu" | "forall" => { + let [_, var, body] = &list[..] else { + return Err(SExprError::Invalid("(mu X ty) or (forall a ty)".into())); + }; + let var = SmolStr::new(atom_string(var)?); + let body = Box::new(decode_ty(body)?); + Ok(match tag.as_str() { + "mu" => Ty::Mu { var, body }, + _ => Ty::ForAll { var, body }, + }) + } _ => Err(SExprError::Invalid("unknown type tag".into())), } } @@ -1158,4 +1200,36 @@ mod tests { let no_name = SExpr::List(vec![SExpr::Atom("type-app".into())]); assert!(decode_expr(&no_name).is_err()); } + + /// `fold` keeps its annotation, a recursive type with a bound type + /// parameter, and `unfold` keeps its operand (v2 plan rung E9). + #[test] + fn roundtrip_fold_and_unfold() { + // forall a. mu #List. () + (a * #List) + let list = Ty::ForAll { + var: SmolStr::new("a"), + body: Box::new(Ty::Mu { + var: SmolStr::new("#List"), + body: Box::new(Ty::Sum { + left: Box::new(Ty::Base(BaseTy::Unit)), + right: Box::new(Ty::Prod { + left: Box::new(Ty::Var(SmolStr::new("a"))), + right: Box::new(Ty::Var(SmolStr::new("#List"))), + }), + }), + }), + }; + let nil = ExprKind::Fold { + ty: list, + value: Box::new(Expr::dummy(ExprKind::Lit(Literal::Unit))), + }; + let kind = ExprKind::Unfold(Box::new(Expr::dummy(nil))); + let sexpr = expr_to_sexpr(&Expr::dummy(kind.clone())); + assert_eq!(decode_expr(&sexpr).expect("decode").kind, kind); + + for short in ["fold", "unfold"] { + let short = SExpr::List(vec![SExpr::Atom(short.into())]); + assert!(decode_expr(&short).is_err()); + } + } } diff --git a/src/ephapax-lsp/src/main.rs b/src/ephapax-lsp/src/main.rs index 6976161..594e3b0 100644 --- a/src/ephapax-lsp/src/main.rs +++ b/src/ephapax-lsp/src/main.rs @@ -708,6 +708,7 @@ fn format_ty(ty: &Ty) -> String { ), Ty::Var(name) => name.to_string(), Ty::ForAll { var, body } => format!("forall {}. {}", var, format_ty(body)), + Ty::Mu { var, body } => format!("mu {}. {}", var, format_ty(body)), Ty::Unif(id) => format!("?{}", id), Ty::List(inner) => format!("[{}]", format_ty(inner)), Ty::Tuple(elems) => { @@ -900,6 +901,8 @@ fn find_let_binding_span(expr: &Expr, target: &str) -> Option { | ExprKind::Snd(inner) | ExprKind::Inl { value: inner, .. } | ExprKind::Inr { value: inner, .. } + | ExprKind::Fold { value: inner, .. } + | ExprKind::Unfold(inner) | ExprKind::Drop(inner) | ExprKind::Copy(inner) | ExprKind::Borrow { inner, .. } diff --git a/src/ephapax-repl/src/lib.rs b/src/ephapax-repl/src/lib.rs index d1d679d..a145892 100644 --- a/src/ephapax-repl/src/lib.rs +++ b/src/ephapax-repl/src/lib.rs @@ -448,6 +448,7 @@ fn format_type(ty: &Ty) -> String { Ty::Ref { inner, .. } => format!("Ref({})", format_type(inner)), Ty::Var(v) => v.to_string(), Ty::ForAll { var, body } => format!("forall {}. {}", var, format_type(body)), + Ty::Mu { var, body } => format!("mu {}. {}", var, format_type(body)), Ty::Unif(id) => format!("?{}", id), Ty::Effectful { param, diff --git a/src/ephapax-syntax/src/lib.rs b/src/ephapax-syntax/src/lib.rs index 2afd914..e5259f6 100644 --- a/src/ephapax-syntax/src/lib.rs +++ b/src/ephapax-syntax/src/lib.rs @@ -118,6 +118,14 @@ pub enum Ty { /// Tuple type (T, U, ...) Tuple(Vec), + + /// Iso-recursive type `mu var. body` (v2 plan decision D7, rung E9). + /// `Var(var)` in `body` stands for the whole type. A value of this + /// type is made with `fold` and opened with `unfold`; the type is not + /// equal to its unfolding. The desugarer makes one for a `data` type + /// that refers to itself, and its `var` is not a name that a program + /// can write, so a type variable of the program cannot be captured. + Mu { var: SmolStr, body: Box }, } impl Ty { @@ -142,7 +150,7 @@ impl Ty { Ty::Borrow { inner, .. } => inner.references_region(region), Ty::List(inner) => inner.references_region(region), Ty::Tuple(elements) => elements.iter().any(|t| t.references_region(region)), - Ty::ForAll { body, .. } => body.references_region(region), + Ty::ForAll { body, .. } | Ty::Mu { body, .. } => body.references_region(region), Ty::Effectful { param, ret, .. } => { param.references_region(region) || ret.references_region(region) } @@ -168,6 +176,12 @@ impl Ty { /// /// Type variables (`Var`, `Unif`) are conservatively non-linear. /// Phase 2 will add linearity bounds (`T: Lin`) for generic linear code. + /// + /// A recursive type `mu X. T` is linear when `T` is linear with `X` + /// not linear. This is the least fixed point that the v2 plan gives + /// for the grade of a recursive type: the first step of the iteration + /// reads `X` as not linear, and a second step cannot change a join. + /// So `mu X. () + (String * X)` is linear, as `String` is. pub fn is_linear(&self) -> bool { match self { Ty::String(_) => true, @@ -176,7 +190,7 @@ impl Ty { .. } => true, Ty::Region { inner, .. } => inner.is_linear(), - Ty::ForAll { body, .. } => body.is_linear(), + Ty::ForAll { body, .. } | Ty::Mu { body, .. } => body.is_linear(), Ty::Prod { left, right } | Ty::Sum { left, right } => { left.is_linear() || right.is_linear() } @@ -191,11 +205,15 @@ impl Ty { match self { Ty::Var(v) if v == var => replacement.clone(), Ty::Var(_) | Ty::Base(_) | Ty::Unif(_) => self.clone(), - Ty::ForAll { var: v, body } if v == var => self.clone(), // shadowed + Ty::ForAll { var: v, .. } | Ty::Mu { var: v, .. } if v == var => self.clone(), // shadowed Ty::ForAll { var: v, body } => Ty::ForAll { var: v.clone(), body: Box::new(body.subst_var(var, replacement)), }, + Ty::Mu { var: v, body } => Ty::Mu { + var: v.clone(), + body: Box::new(body.subst_var(var, replacement)), + }, Ty::Fun { param, ret } => Ty::Fun { param: Box::new(param.subst_var(var, replacement)), ret: Box::new(ret.subst_var(var, replacement)), @@ -254,7 +272,8 @@ impl Ty { | Ty::Region { inner, .. } | Ty::Borrow { inner, .. } | Ty::List(inner) - | Ty::ForAll { body: inner, .. } => inner.contains_unif(id), + | Ty::ForAll { body: inner, .. } + | Ty::Mu { body: inner, .. } => inner.contains_unif(id), Ty::Effectful { param, ret, .. } => param.contains_unif(id) || ret.contains_unif(id), Ty::Tuple(elems) => elems.iter().any(|t| t.contains_unif(id)), } @@ -299,6 +318,10 @@ impl Ty { var: var.clone(), body: Box::new(body.resolve(solutions)), }, + Ty::Mu { var, body } => Ty::Mu { + var: var.clone(), + body: Box::new(body.resolve(solutions)), + }, Ty::Effectful { param, ret, @@ -312,6 +335,15 @@ impl Ty { Ty::Tuple(elems) => Ty::Tuple(elems.iter().map(|t| t.resolve(solutions)).collect()), } } + + /// The type of `unfold e` for `e` of this type: `body` with the whole + /// type in the place of `var`. `None` if this is not a recursive type. + pub fn unfolded(&self) -> Option { + match self { + Ty::Mu { var, body } => Some(body.subst_var(var, self)), + _ => None, + } + } } /// Literal values @@ -652,6 +684,15 @@ pub enum ExprKind { /// Tuple field access tuple.N TupleIndex { tuple: Box, index: usize }, + + // ===== Recursive types (v2 plan decision D7, rung E9) ===== + /// `fold[ty](value)`: `value` has the unfolding of the recursive type + /// `ty`, and the result has the type `ty`. + Fold { ty: Ty, value: Box }, + + /// `unfold(e)`: `e` has a recursive type, and the result has its + /// unfolding. + Unfold(Box), } impl Expr { @@ -693,9 +734,11 @@ impl Expr { | ExprKind::Snd(e) | ExprKind::Deref(e) | ExprKind::Drop(e) - | ExprKind::Copy(e) => vec![e], + | ExprKind::Copy(e) + | ExprKind::Unfold(e) => vec![e], ExprKind::Inl { value: e, .. } | ExprKind::Inr { value: e, .. } + | ExprKind::Fold { value: e, .. } | ExprKind::Lambda { body: e, .. } | ExprKind::Region { body: e, .. } | ExprKind::Borrow { inner: e, .. } diff --git a/src/ephapax-typing/src/lib.rs b/src/ephapax-typing/src/lib.rs index f22a180..eed55a8 100644 --- a/src/ephapax-typing/src/lib.rs +++ b/src/ephapax-typing/src/lib.rs @@ -151,6 +151,11 @@ pub enum TypeError { #[error("`{0}` is not a generic function and cannot take type arguments")] NotGeneric(Var), + /// `fold` to a type, or `unfold` of a value of a type, that is not a + /// recursive type (v2 plan rung E9). + #[error("`fold` and `unfold` need a recursive type, found {0:?}")] + NotRecursive(Ty), + /// The number of explicit type arguments is not the number of type /// parameters. #[error("The generic function `{callee}` has {expected} type parameter(s), but the call gives {got} type argument(s)")] @@ -588,6 +593,12 @@ fn subst_tys(ty: &Ty, subst: &HashMap) -> Ty { } } } + // The variable of a recursive type is not a name of the program, + // so no substitution has it. + Ty::Mu { var, body } => Ty::Mu { + var: var.clone(), + body: Box::new(subst_tys(body, subst)), + }, Ty::Effectful { param, ret, @@ -1135,6 +1146,13 @@ impl TypeChecker { self.unify(s, i1, i2) } (Ty::List(i1), Ty::List(i2)) => self.unify(s, i1, i2), + // 2 recursive types are equal when their bodies are, with one + // name for the 2 bound variables. A recursive type is not + // equal to its unfolding (iso-recursive, decision D7). + (Ty::Mu { var: v1, body: b1 }, Ty::Mu { var: v2, body: b2 }) => { + let b2 = b2.subst_var(v2, &Ty::Var(v1.clone())); + self.unify(s, b1, &b2) + } (Ty::Tuple(e1), Ty::Tuple(e2)) if e1.len() == e2.len() => { for (t1, t2) in e1.iter().zip(e2.iter()) { self.unify(s, t1, t2)?; @@ -1236,9 +1254,35 @@ impl TypeChecker { ExprKind::Perform { op, args } => self.check_perform(s, op, args), ExprKind::Handle { body, clauses } => self.check_handle(s, body, clauses), ExprKind::Match { scrutinee, arms } => self.check_match(s, scrutinee, arms), + ExprKind::Fold { ty, value } => self.check_fold(s, ty, value), + ExprKind::Unfold(inner) => self.check_unfold(s, inner), } } + /// `fold[ty](value)`: `ty` is a recursive type `mu X. T`, `value` has + /// the type `T[X := ty]`, and the result has the type `ty`. A type + /// parameter that the annotation binds (`forall a. mu X. T`) gets the + /// type that `value` gives it. + fn check_fold(&mut self, s: Span, ty: &Ty, value: &Expr) -> Result { + let (ty, _) = self.instantiate(ty.clone()); + let Some(unfolded) = ty.unfolded() else { + return Err(self.at(s, TypeError::NotRecursive(ty))); + }; + let value_ty = self.check(value)?; + self.unify(value.span, &unfolded, &value_ty)?; + Ok(self.resolve(&ty)) + } + + /// `unfold(inner)`: `inner` has a recursive type `mu X. T`, and the + /// result has the type `T[X := mu X. T]`. + fn check_unfold(&mut self, s: Span, inner: &Expr) -> Result { + let inner_ty = self.check(inner)?; + let inner_ty = self.resolve(&inner_ty); + inner_ty + .unfolded() + .ok_or_else(|| self.at(s, TypeError::NotRecursive(inner_ty))) + } + fn check_lit(&self, s: Span, lit: &Literal) -> Result { Ok(match lit { Literal::Unit => Ty::Base(BaseTy::Unit), @@ -1719,20 +1763,27 @@ impl TypeChecker { } } + /// `inl[ty](value)`: `ty` is the type of the other side of the sum. A + /// type parameter that the annotation binds (`forall a. T`, from a + /// constructor of a recursive `data` type) gets a type from the use + /// of the value: the `fold` around the injection. fn check_inl(&mut self, _s: Span, ty: &Ty, value: &Expr) -> Result { let value_ty = self.check(value)?; + let (ty, _) = self.instantiate(ty.clone()); Ok(Ty::Sum { left: Box::new(value_ty), - right: Box::new(ty.clone()), + right: Box::new(ty), }) } + /// `inr[ty](value)`: as [`Self::check_inl`], for the other side. fn check_inr(&mut self, _s: Span, ty: &Ty, value: &Expr) -> Result { let value_ty = self.check(value)?; + let (ty, _) = self.instantiate(ty.clone()); Ok(Ty::Sum { - left: Box::new(ty.clone()), + left: Box::new(ty), right: Box::new(value_ty), }) } @@ -2946,6 +2997,7 @@ fn has_unif(ty: &Ty) -> bool { | Ty::Region { inner, .. } | Ty::Borrow { inner, .. } | Ty::ForAll { body: inner, .. } + | Ty::Mu { body: inner, .. } | Ty::List(inner) => has_unif(inner), Ty::Fun { param, ret } | Ty::Effectful { param, ret, .. } => { has_unif(param) || has_unif(ret) diff --git a/src/ephapax-typing/src/mono.rs b/src/ephapax-typing/src/mono.rs index 2737133..6b22836 100644 --- a/src/ephapax-typing/src/mono.rs +++ b/src/ephapax-typing/src/mono.rs @@ -55,7 +55,8 @@ fn substitute_node(expr: &mut Expr, subst: &Subst) { | ExprKind::LetLin { ty: Some(ty), .. } | ExprKind::Lambda { param_ty: ty, .. } | ExprKind::Inl { ty, .. } - | ExprKind::Inr { ty, .. } => *ty = subst_tys(ty, subst), + | ExprKind::Inr { ty, .. } + | ExprKind::Fold { ty, .. } => *ty = subst_tys(ty, subst), ExprKind::TypeApp { type_args, .. } => { for ty in type_args { *ty = subst_tys(ty, subst); @@ -197,6 +198,7 @@ fn ty_name(ty: &Ty) -> String { Ty::Sum { left, right } => format!("({} + {})", ty_name(left), ty_name(right)), Ty::Tuple(elems) => format!("({})", list(elems)), Ty::List(elem) => format!("[{}]", ty_name(elem)), + Ty::Mu { var, body } => format!("(mu {var}. {})", ty_name(body)), other => format!("{other:?}"), } } diff --git a/src/ephapax-wasm/src/lib.rs b/src/ephapax-wasm/src/lib.rs index e3e1140..cd1136e 100644 --- a/src/ephapax-wasm/src/lib.rs +++ b/src/ephapax-wasm/src/lib.rs @@ -257,6 +257,22 @@ fn first_unsupported_in( expr.span.start, expr.span.end ))) } + // A value of a recursive `data` type is made by `fold` and read + // by `unfold` (v2 plan rung E9). Both are behind the flag. + ExprKind::Fold { .. } | ExprKind::Unfold(_) if !unstable_core => { + let ty = match &expr.kind { + ExprKind::Fold { ty, .. } => Some(ty), + ExprKind::Unfold(inner) => types.and_then(|t| t.get(&inner.id)), + _ => None, + }; + Some(CodegenError(format!( + "{UNSTABLE_CORE_PREFIX}: a value of {} (at byte {}..{})", + ty.and_then(recursive_name) + .unwrap_or_else(|| "a recursive `data` type".to_string()), + expr.span.start, + expr.span.end + ))) + } ExprKind::Match { scrutinee, arms } => types .and_then(|t| t.get(&scrutinee.id)) .filter(|ty| arms.iter().any(|arm| pattern_not_lowered(&arm.pattern, ty))) @@ -289,13 +305,18 @@ fn first_unsupported_in( | ExprKind::Snd(e) | ExprKind::Deref(e) | ExprKind::Drop(e) - | ExprKind::Copy(e) => vec![e], + | ExprKind::Copy(e) + | ExprKind::Unfold(e) => vec![e], ExprKind::Let { value, body, .. } | ExprKind::LetLin { value, body, .. } => { vec![value, body] } ExprKind::Lambda { body, .. } | ExprKind::Region { body, .. } => vec![body], ExprKind::App { func, arg } => vec![func, arg], - ExprKind::Inl { value, .. } | ExprKind::Inr { value, .. } => vec![value], + ExprKind::Inl { value, .. } + | ExprKind::Inr { value, .. } + | ExprKind::Fold { value, .. } => { + vec![value] + } ExprKind::Case { scrutinee, left_body, @@ -372,6 +393,16 @@ fn validate_supported_in( Decl::Const { name, value, .. } => (name, value, "constant"), _ => continue, }; + // A function can pass a value of a recursive type on with no + // `fold` and no `unfold`: its signature shows the type. + if let (false, Decl::Fn { params, ret_ty, .. }) = (unstable_core, decl) { + let tys = params.iter().map(|(_, ty)| ty).chain([ret_ty]); + if let Some(ty) = tys.filter_map(recursive_name).next() { + return Err(CodegenError(format!( + "{UNSTABLE_CORE_PREFIX}: {ty} in the signature of function `{name}`" + ))); + } + } if let Some(CodegenError(msg)) = first_unsupported_in(expr, types, unstable_core) { return Err(CodegenError(format!("{msg} in {kind} `{name}`"))); } @@ -379,6 +410,31 @@ fn validate_supported_in( Ok(()) } +/// "the recursive type `IntList`" for the first recursive type in `ty`, +/// by the name of its `data` type. `None` if `ty` has no recursive type. +fn recursive_name(ty: &Ty) -> Option { + match ty { + // The variable of the recursive type of `data IntList` is `#IntList`. + Ty::Mu { var, .. } => Some(format!( + "the recursive type `{}`", + var.trim_start_matches('#') + )), + Ty::Base(_) | Ty::String(_) | Ty::Var(_) | Ty::Unif(_) => None, + Ty::Ref { inner, .. } + | Ty::Region { inner, .. } + | Ty::Borrow { inner, .. } + | Ty::ForAll { body: inner, .. } + | Ty::List(inner) => recursive_name(inner), + Ty::Fun { param, ret } | Ty::Effectful { param, ret, .. } => { + recursive_name(param).or_else(|| recursive_name(ret)) + } + Ty::Prod { left, right } | Ty::Sum { left, right } => { + recursive_name(left).or_else(|| recursive_name(right)) + } + Ty::Tuple(elems) => elems.iter().find_map(recursive_name), + } +} + // --------------------------------------------------------------------------- // Ty → OwnershipKind mapping // --------------------------------------------------------------------------- @@ -2206,6 +2262,12 @@ impl Codegen { // Borrow/deref are identity at the WASM level self.compile_expr(func, inner); } + // A value of a recursive type is the value of its unfolding, + // which is a pointer to a heap cell (a sum, a pair): `fold` + // and `unfold` change the type only (v2 plan rung E9). + ExprKind::Fold { value, .. } | ExprKind::Unfold(value) => { + self.compile_expr(func, value); + } ExprKind::Drop(inner) => { self.compile_expr(func, inner); // Mark the local as consumed if it's a variable @@ -2516,8 +2578,10 @@ impl Codegen { } ExprKind::Fst(inner) | ExprKind::Snd(inner) + | ExprKind::Unfold(inner) | ExprKind::Inl { value: inner, .. } - | ExprKind::Inr { value: inner, .. } => { + | ExprKind::Inr { value: inner, .. } + | ExprKind::Fold { value: inner, .. } => { collect(inner, bound, free, seen); } ExprKind::Case { diff --git a/tests/probes/expectations.tsv b/tests/probes/expectations.tsv index 6bddeb9..670b86f 100644 --- a/tests/probes/expectations.tsv +++ b/tests/probes/expectations.tsv @@ -29,9 +29,9 @@ pairdup wasm-run no-module no-module E0: no module for a rejected program lamcap check error:TypeError error:TypeError E0 tests/linearity_holes.rs: reuse of a linear value is a named TypeError lamcap compile error:TypeError error:TypeError E0: compile runs the same checker lamcap wasm-run no-module no-module E0: no module for a rejected program -rec1 check error:DesugarError error:DesugarError E0: recursive data is a named DesugarError, never a crash -rec1 compile error:DesugarError error:DesugarError E0 -rec1 wasm-run no-module no-module E0 +rec1 check error:UnstableCore error:UnstableCore E9: recursive data is behind the flag --unstable-core; without it, a named error, never a crash (E0) +rec1 compile error:UnstableCore error:UnstableCore E9 +rec1 wasm-run no-module no-module E9: no module for a program that needs the flag i64 check ok ok E5 (already accepted) i64 compile ok ok E5 typed side table: I64 binops lower to i64 i64 wasm-run ok:0 ok:0 E5 (baseline recorded from `ephapax run`, which uses the same engine: the wasmtime CLI was not installed)