From b97c37a11dfaa2328497c20bfb1529ecd64a9942 Mon Sep 17 00:00:00 2001 From: Joel Abrahams Date: Thu, 27 Aug 2026 15:58:54 +0200 Subject: [PATCH 1/5] doc: more explanation total functions --- README.md | 102 +++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 97 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index a8427474..5be0185e 100644 --- a/README.md +++ b/README.md @@ -375,6 +375,7 @@ Instead, we place heavy restrictions on total functions, enforcing that they are a. If in the _call tree_ we call a different total function, the argument does not have to be strictly decreasing. b. However, it should still be globally decreasing, meaning that we amend the above: + _"compared to the first parent of the node which is equal to said node, summing over all intermediate nodes" This does mean that we must be able to perform basic arithmetic on the types of the function for this (logic) system to work! **In some sense, basic (integer) arithmetic forms the logical bedrock of our system** @@ -387,6 +388,51 @@ Instead, we place heavy restrictions on total functions, enforcing that they are - `RangeInclusive` : `a..=b` Put another way, we sidestep the issue by ensuring that our system is still sound, but incomplete by acknowledging that we cannot prove termination for arbitrary functions! +**Marking a function `total` does not ask the compiler to decide termination for the function as written.** +It switches the checker into a stricter mode that only accepts the fixed, mechanically checkable subset described by the four rules above. +Write something outside that shape, however obviously it halts to a human reader, and it is rejected. +This is the same trade-off `const fn` makes in Rust or `constexpr` makes in C++. + +It's worth being explicit that this really is a strict subset, not a temporary gap we intend to close later. +**Ackermann's function** is the classic example here. + +```mamba +# some syntax here such as guard arms which are not in the language yet +def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) with + (m, n) if m = 0 => n + 1 + (m, n) if n = 0 => ackermann(m - 1, 1) + (m, n) => ackermann(m - 1, ackermann(m, n - 1)) +end +``` + +`ackermann` (referred to as `A` for brevity sake below) is, in fact, total; +It will halt on all possible inputs. +Its definition looks like an entirely ordinary pair of recursive calls. +But `A` is the textbook example of a total, computable function that is **not primitive recursive**. + +Primitive recursion means the depth of the recursion is bounded in advance by a single value that strictly decreases toward a base case. +A `for` loop over a `SizedIterator` is primitive recursive. +Its iteration count is fixed by the collection's size before the loop even starts. +Structural descent on a single `Measurable` value is primitive recursive too. +Its number of recursive calls is bounded by the starting measure. +This is exactly the expressive class `total` restricts you to. + +Concretely, our `StrictlyDecreases`/`Measurable` scheme cannot accept `A`. + +- The call `A(m, n - 1)` doesn't decrease `m` at all, only `n`. +- The outer call `A(m - 1, A(m, n - 1))` decreases `m`, but its *second* argument is whatever the inner call returns. + This is vastly larger than the original `n`. + No single `Measurable` value of `(m, n)` shrinks on every call, because the "size" of the second argument is regenerated at each step rather than consumed. +- Proving `A` terminates requires induction nested inside induction: + Induct on `m`, and for each `m` separately induct on `n`, reusing the outer hypothesis inside the inner one. + That's a stronger well-founded ordering than a single scalar `measure()` (or even a fixed-arity lexicographic tuple of them) can express. + This is, historically, precisely why Ackermann constructed the function: + To exhibit a total computable function outside the primitive recursive class. + +So a function shaped like Ackermann's can never be marked `total` in Mamba: +No decidable `measure()`-based scheme can accept it while remaining decidable. +Every function we accept as `total` truly halts; not every function that truly halts can be accepted. +Agda, Idris, and Lean draw the same line, for the same reason. Take for instance this naive implementation of the Fibonacci sequence: @@ -448,7 +494,26 @@ end Both of the above return an `Int`, which is part of the library and implements the `Measured` trait. This is a special built-in trait of the language, which as of writing cannot be implemented for custom types. -This is because this forms the logical bedrock of our system of proving that functions are total, but in future we may relax this constraint. + +> **Flag:** `measure()` returning plain `Int` is, as specified above, actually unsound. Well-founded descent +> needs the measure's codomain to have no infinite *descending* chain — true of `Nat`/`PosInt` (bounded below +> by `0`), false of `Int` (`5, 4, 3, ..., -1, -2, ...` never bottoms out). `Measurable for Int` should measure +> into `Nat`, e.g. `self.abs()`, not `self` directly — or `Measurable`'s signature should require the +> `measure()` result to itself implement a "has a least element" trait, not just `Add, Sub, Eq, Comparable`. +> Either way, this needs fixing before `Measurable for Int` is trustworthy, independent of anything else below. + +We think the "cannot be implemented for custom types" restriction can be relaxed, but only for `measure()` +specifically, and only alongside a matching restriction on what a `measure()` body is allowed to contain: no +recursion, no calls to other `meta` functions besides other `measure()` bodies, no loops — just a straight-line +pure expression built from `Add`/`Sub`/`Eq`/`Comparable` operations and reads of `Measurable`-typed sub-fields +(e.g. `self.left.measure() + self.right.measure()` for a tree). There is no fixed-point construct anywhere in +that grammar, so there is no way to write a `measure()` that fails to terminate even in principle — that whole +category of bug is excluded by construction, not merely checked for. Without opening this up, `total` is only +ever useful for built-in numeric types, since a user can never give the checker a way to measure their own +recursive types (trees, custom collections, etc.), which would make the feature far less valuable in practice. + +This is a materially different, and much safer, question than opening up general-purpose `meta` functions to +user-defined recursion — see below. ```mamba # Trait measurable lives at the heart of this system, and by extension Mamba. @@ -496,12 +561,39 @@ These functions have two constraints: Additionally: -- A meta function is not enforced to be total, but it is recommended that it is! - This is because for the compiler to prove a function is meta, it must compile the application first. - Thus we have a circular dependency; - We are already compiling, so this is not an option (unless we have a meta-compiler, but that would require a meta-meta compiler, and so forth...). +- A meta function **must** be total — not merely recommended, required. We resolve the circularity concern + above (proving a function is total normally means compiling and checking it, but we're mid-compile already) + by not proving it at all: a meta function's body is held to the same four restrictions as `total` functions + (see above). This is a syntactic well-formedness rule, not an evaluation — the checker never has to *run* a + meta function to know it terminates, any more than a borrow checker has to run a program to know it doesn't + alias. That sidesteps the meta-compiler regress entirely. - We may well place additional constraints on meta functions in future. +**Should users be able to write general-purpose `meta` functions at all, given the above?** We think the +honest answer for now is: not yet, or only in a closed form. Restrict `meta` to `@builtin`-gated definitions +that ship with the standard library (reviewed by us, small in number) rather than something any Mamba user can +write. The `Measurable`/`measure()` case above is the exception, because we found a restriction (straight-line, +no-recursion-at-all) that's *safe to open up* precisely because it removes recursion from the picture entirely. +General-purpose `meta` has no equivalent escape hatch — its whole value is running arbitrary compile-time +computation — so the best we can offer a user-authored `meta` function is "restricted to structural recursion, +checked," which is weaker than "cannot possibly fail to terminate." Given the README's own framing above (this +is a niche, mostly-stdlib feature to begin with), the risk/benefit favors keeping it closed until there's a +concrete case for opening it. + +Worth stating explicitly: even with the structural-recursion restriction, suppose we (or a future relaxation) +get the checker's syntactic rule wrong and it lets through something that shouldn't have been accepted. The +failure mode is the compiler hangs evaluating a `meta` function during `total`-checking. That is a **strictly +preferable** failure to the one `total` exists to prevent — a hung compile happens on a developer's own +machine or in CI, is attributable to a specific function, is interruptible, and blocks the broken code from +ever being shipped; a hung `total` function at runtime is the exact production failure (denial of service, +a stuck request thread, resource exhaustion) that the whole feature was built to rule out, except now dressed +up with a false badge of having been proven safe. So while the goal is to make compile-time non-termination +impossible by construction (per the structural restriction above), if we ever have to choose between an +imperfect static check that occasionally hangs the compiler and a looser one that occasionally ships a +non-terminating `total` function, we should choose the former without hesitation — and pair it with a +recursion/step budget during meta evaluation (`error: meta evaluation exceeded N steps`), so the failure shows +up as a diagnostic rather than a silent freeze. + **Essentially, the main reason for Mamba having meta functions is to serve as the logical bedrock for provable total functions**. One other benefit is that compiled functions are evaluated at compile time and not runtime, potentially offering significant speed benefits. This is useful when one wants to document how one derived a meta in the form of code, without re-calculating it each time at runtime. From c1a55c28ff63c3cb56367f5e1900e87d1897d2a2 Mon Sep 17 00:00:00 2001 From: Joel Abrahams Date: Fri, 28 Aug 2026 10:26:32 +0200 Subject: [PATCH 2/5] doc: more explanation on termination --- README.md | 66 +++++++++++++++++++++++++++---------------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/README.md b/README.md index 5be0185e..f2d53f25 100644 --- a/README.md +++ b/README.md @@ -421,18 +421,30 @@ Concretely, our `StrictlyDecreases`/`Measurable` scheme cannot accept `A`. - The call `A(m, n - 1)` doesn't decrease `m` at all, only `n`. - The outer call `A(m - 1, A(m, n - 1))` decreases `m`, but its *second* argument is whatever the inner call returns. - This is vastly larger than the original `n`. - No single `Measurable` value of `(m, n)` shrinks on every call, because the "size" of the second argument is regenerated at each step rather than consumed. -- Proving `A` terminates requires induction nested inside induction: - Induct on `m`, and for each `m` separately induct on `n`, reusing the outer hypothesis inside the inner one. - That's a stronger well-founded ordering than a single scalar `measure()` (or even a fixed-arity lexicographic tuple of them) can express. - This is, historically, precisely why Ackermann constructed the function: - To exhibit a total computable function outside the primitive recursive class. - -So a function shaped like Ackermann's can never be marked `total` in Mamba: -No decidable `measure()`-based scheme can accept it while remaining decidable. -Every function we accept as `total` truly halts; not every function that truly halts can be accepted. -Agda, Idris, and Lean draw the same line, for the same reason. + This can be vastly larger than the original `n`. +- Proving `A` terminates does have a real measure behind it, to be precise. + Compare `(m, n)` lexicographically, with `m` as the dominant component. + `A(m, n - 1)` decreases in the second slot. + `A(m - 1, A(m, n - 1))` decreases in the first slot, no matter how large the second slot becomes. + This is a well-founded order, its order type is `ω²`. + So Ackermann's termination is not unprovable. + +What `A` lacks is a *flat* measure, which is what Mamba's scheme requires. +`measure()` returns one comparable value. +`decreases` is one comparison: `self.measure() < other.measure()`. +There is no way to fold `(m, n)` into a single number so that "the pair got lexicographically smaller" becomes "the folded number got smaller". +`n` can grow without any fixed bound in the very same step that `m` shrinks by one. +No finite weighting of `m` and `n` into a single scalar survives that. + +So a function shaped like Ackermann's can never be marked `total` in Mamba today. +Not because no well-founded measure exists for it. +Instead, Mamba's well-founded order is deliberately flat, and Ackermann needs a lexicographic (or ordinal) one. +This doesn't mean every practical termination checker rejects it outright. +ACL2 admits Ackermann-shaped definitions directly, using measures into the ordinals below `ε₀` instead of plain naturals. +Structural checkers built on multi-path call-graph analysis, the size-change principle (Lee, Jones, Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001), can accept the ordinary two-clause Ackermann definition too, by tracking that some combination of argument positions decreases along every call path rather than one designated one. +Agda's termination checker works this way. +Generalising `Measurable` from a flat scalar to a lexicographic tuple, an ordinal, or a multi-argument call-graph analysis is a real, addressable extension. +We don't implement any of that today, but it's worth keeping on the table, and it connects directly to the question of opening `Measurable` up to custom types at all, discussed below. Take for instance this naive implementation of the Fibonacci sequence: @@ -481,39 +493,27 @@ Instead, ordering is reduced to numeric ordering, which is verifiable and depend It is for instance defined for the built-in primitive `Int`. ```mamba -# Measure for int just returns self +# Measure for Int returns abs(self), landing in PosInt, since a measure needs a bounded-below domain def StrictlyDecreases for Int where - def meta measure(self) -> Measurable := self + def meta measure(self) -> Measurable := self.abs() end -# For string, we as an example use the length of the string (Which is also an integer) +# For string, we as an example use the length of the string (also a PosInt) def StrictlyDecreases for Str where def meta measure(self) -> Measurable := self.len() end ``` -Both of the above return an `Int`, which is part of the library and implements the `Measured` trait. +Both of the above return a `PosInt`, which is part of the library and implements the `Measurable` trait. This is a special built-in trait of the language, which as of writing cannot be implemented for custom types. -> **Flag:** `measure()` returning plain `Int` is, as specified above, actually unsound. Well-founded descent -> needs the measure's codomain to have no infinite *descending* chain — true of `Nat`/`PosInt` (bounded below -> by `0`), false of `Int` (`5, 4, 3, ..., -1, -2, ...` never bottoms out). `Measurable for Int` should measure -> into `Nat`, e.g. `self.abs()`, not `self` directly — or `Measurable`'s signature should require the -> `measure()` result to itself implement a "has a least element" trait, not just `Add, Sub, Eq, Comparable`. -> Either way, this needs fixing before `Measurable for Int` is trustworthy, independent of anything else below. - -We think the "cannot be implemented for custom types" restriction can be relaxed, but only for `measure()` -specifically, and only alongside a matching restriction on what a `measure()` body is allowed to contain: no -recursion, no calls to other `meta` functions besides other `measure()` bodies, no loops — just a straight-line -pure expression built from `Add`/`Sub`/`Eq`/`Comparable` operations and reads of `Measurable`-typed sub-fields -(e.g. `self.left.measure() + self.right.measure()` for a tree). There is no fixed-point construct anywhere in -that grammar, so there is no way to write a `measure()` that fails to terminate even in principle — that whole -category of bug is excluded by construction, not merely checked for. Without opening this up, `total` is only -ever useful for built-in numeric types, since a user can never give the checker a way to measure their own -recursive types (trees, custom collections, etc.), which would make the feature far less valuable in practice. +We think this restriction can be relaxed for user types. +The requirement is just that `measure()` be total, deterministic, and pure: defined for every input, always giving the same output for the same input, and free of side effects. +Given that, plus a bounded-below codomain like `PosInt`, the compiler can independently verify at each recursive call site that the measure actually decreases, regardless of which type `measure()` is defined on. +So there's no correctness reason to keep `Measurable` closed to built-in types specifically, only a simplicity one for now. This is a materially different, and much safer, question than opening up general-purpose `meta` functions to -user-defined recursion — see below. +user-defined recursion. See below. ```mamba # Trait measurable lives at the heart of this system, and by extension Mamba. From 0eb8d44f672b6777c07139f90fd6ef5f8f97e635 Mon Sep 17 00:00:00 2001 From: Joel Abrahams Date: Fri, 28 Aug 2026 10:49:45 +0200 Subject: [PATCH 3/5] doc: some more explanation on total functions --- README.md | 93 +++--------- docs/features/README.md | 5 + docs/features/functions/README.md | 17 +++ docs/features/functions/meta_functions.md | 30 ++++ docs/features/functions/pure_functions.md | 19 +++ docs/features/functions/total_functions.md | 157 +++++++++++++++++++++ 6 files changed, 248 insertions(+), 73 deletions(-) create mode 100644 docs/features/functions/README.md create mode 100644 docs/features/functions/meta_functions.md create mode 100644 docs/features/functions/pure_functions.md create mode 100644 docs/features/functions/total_functions.md diff --git a/README.md b/README.md index f2d53f25..5101b6e6 100644 --- a/README.md +++ b/README.md @@ -394,7 +394,8 @@ Write something outside that shape, however obviously it halts to a human reader This is the same trade-off `const fn` makes in Rust or `constexpr` makes in C++. It's worth being explicit that this really is a strict subset, not a temporary gap we intend to close later. -**Ackermann's function** is the classic example here. +Not every function that obviously halts can be marked `total`. +**Ackermann's function** is the classic example: ```mamba # some syntax here such as guard arms which are not in the language yet @@ -405,46 +406,15 @@ def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) with end ``` -`ackermann` (referred to as `A` for brevity sake below) is, in fact, total; -It will halt on all possible inputs. -Its definition looks like an entirely ordinary pair of recursive calls. -But `A` is the textbook example of a total, computable function that is **not primitive recursive**. - -Primitive recursion means the depth of the recursion is bounded in advance by a single value that strictly decreases toward a base case. -A `for` loop over a `SizedIterator` is primitive recursive. -Its iteration count is fixed by the collection's size before the loop even starts. -Structural descent on a single `Measurable` value is primitive recursive too. -Its number of recursive calls is bounded by the starting measure. -This is exactly the expressive class `total` restricts you to. - -Concretely, our `StrictlyDecreases`/`Measurable` scheme cannot accept `A`. - -- The call `A(m, n - 1)` doesn't decrease `m` at all, only `n`. -- The outer call `A(m - 1, A(m, n - 1))` decreases `m`, but its *second* argument is whatever the inner call returns. - This can be vastly larger than the original `n`. -- Proving `A` terminates does have a real measure behind it, to be precise. - Compare `(m, n)` lexicographically, with `m` as the dominant component. - `A(m, n - 1)` decreases in the second slot. - `A(m - 1, A(m, n - 1))` decreases in the first slot, no matter how large the second slot becomes. - This is a well-founded order, its order type is `ω²`. - So Ackermann's termination is not unprovable. - -What `A` lacks is a *flat* measure, which is what Mamba's scheme requires. -`measure()` returns one comparable value. -`decreases` is one comparison: `self.measure() < other.measure()`. -There is no way to fold `(m, n)` into a single number so that "the pair got lexicographically smaller" becomes "the folded number got smaller". -`n` can grow without any fixed bound in the very same step that `m` shrinks by one. -No finite weighting of `m` and `n` into a single scalar survives that. - -So a function shaped like Ackermann's can never be marked `total` in Mamba today. -Not because no well-founded measure exists for it. -Instead, Mamba's well-founded order is deliberately flat, and Ackermann needs a lexicographic (or ordinal) one. -This doesn't mean every practical termination checker rejects it outright. -ACL2 admits Ackermann-shaped definitions directly, using measures into the ordinals below `ε₀` instead of plain naturals. -Structural checkers built on multi-path call-graph analysis, the size-change principle (Lee, Jones, Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001), can accept the ordinary two-clause Ackermann definition too, by tracking that some combination of argument positions decreases along every call path rather than one designated one. -Agda's termination checker works this way. -Generalising `Measurable` from a flat scalar to a lexicographic tuple, an ordinal, or a multi-argument call-graph analysis is a real, addressable extension. -We don't implement any of that today, but it's worth keeping on the table, and it connects directly to the question of opening `Measurable` up to custom types at all, discussed below. +This halts for every input, but Mamba can never mark it `total`. +The trouble is the last case, `ackermann(m - 1, ackermann(m, n - 1))`. +The first argument does get smaller each time. +But the second argument is whatever the inner call returns, which can be a huge number, far bigger than `n` ever was. +Our checker only ever tracks one shrinking number per recursive call. +Here, there just isn't one number that always shrinks. + +There is a way to prove this function halts, but it needs comparing two numbers together rather than one, a more powerful (and more complicated) technique than Mamba currently supports. +See [docs/features/functions/total_functions.md](docs/features/functions/total_functions.md) for the full mathematical story, including why some other languages and provers can accept this exact function today. Take for instance this naive implementation of the Fibonacci sequence: @@ -511,9 +481,10 @@ We think this restriction can be relaxed for user types. The requirement is just that `measure()` be total, deterministic, and pure: defined for every input, always giving the same output for the same input, and free of side effects. Given that, plus a bounded-below codomain like `PosInt`, the compiler can independently verify at each recursive call site that the measure actually decreases, regardless of which type `measure()` is defined on. So there's no correctness reason to keep `Measurable` closed to built-in types specifically, only a simplicity one for now. +See [docs/features/functions/total_functions.md](docs/features/functions/total_functions.md#opening-measurable-to-custom-types) for the full reasoning and its caveats. -This is a materially different, and much safer, question than opening up general-purpose `meta` functions to -user-defined recursion. See below. +This is a materially different, and much safer, question than opening up general-purpose `meta` functions to user-defined recursion. +See below. ```mamba # Trait measurable lives at the heart of this system, and by extension Mamba. @@ -561,38 +532,14 @@ These functions have two constraints: Additionally: -- A meta function **must** be total — not merely recommended, required. We resolve the circularity concern - above (proving a function is total normally means compiling and checking it, but we're mid-compile already) - by not proving it at all: a meta function's body is held to the same four restrictions as `total` functions - (see above). This is a syntactic well-formedness rule, not an evaluation — the checker never has to *run* a - meta function to know it terminates, any more than a borrow checker has to run a program to know it doesn't - alias. That sidesteps the meta-compiler regress entirely. +- A meta function must be total, not just recommended to be. + We can require this without solving the halting problem again, because a meta function's body is held to the same four restrictions as `total` functions. + That's a rule the checker confirms just by looking at the code, without running it. +- We currently keep `meta` closed to the standard library, rather than opening it up to every Mamba user. + General-purpose `meta` doesn't have as clean a safety story as `Measurable` does. - We may well place additional constraints on meta functions in future. -**Should users be able to write general-purpose `meta` functions at all, given the above?** We think the -honest answer for now is: not yet, or only in a closed form. Restrict `meta` to `@builtin`-gated definitions -that ship with the standard library (reviewed by us, small in number) rather than something any Mamba user can -write. The `Measurable`/`measure()` case above is the exception, because we found a restriction (straight-line, -no-recursion-at-all) that's *safe to open up* precisely because it removes recursion from the picture entirely. -General-purpose `meta` has no equivalent escape hatch — its whole value is running arbitrary compile-time -computation — so the best we can offer a user-authored `meta` function is "restricted to structural recursion, -checked," which is weaker than "cannot possibly fail to terminate." Given the README's own framing above (this -is a niche, mostly-stdlib feature to begin with), the risk/benefit favors keeping it closed until there's a -concrete case for opening it. - -Worth stating explicitly: even with the structural-recursion restriction, suppose we (or a future relaxation) -get the checker's syntactic rule wrong and it lets through something that shouldn't have been accepted. The -failure mode is the compiler hangs evaluating a `meta` function during `total`-checking. That is a **strictly -preferable** failure to the one `total` exists to prevent — a hung compile happens on a developer's own -machine or in CI, is attributable to a specific function, is interruptible, and blocks the broken code from -ever being shipped; a hung `total` function at runtime is the exact production failure (denial of service, -a stuck request thread, resource exhaustion) that the whole feature was built to rule out, except now dressed -up with a false badge of having been proven safe. So while the goal is to make compile-time non-termination -impossible by construction (per the structural restriction above), if we ever have to choose between an -imperfect static check that occasionally hangs the compiler and a looser one that occasionally ships a -non-terminating `total` function, we should choose the former without hesitation — and pair it with a -recursion/step budget during meta evaluation (`error: meta evaluation exceeded N steps`), so the failure shows -up as a diagnostic rather than a silent freeze. +See [docs/features/functions/meta_functions.md](docs/features/functions/meta_functions.md) for why we're keeping `meta` closed for now, and what would need to be true before we open it up. **Essentially, the main reason for Mamba having meta functions is to serve as the logical bedrock for provable total functions**. One other benefit is that compiled functions are evaluated at compile time and not runtime, potentially offering significant speed benefits. diff --git a/docs/features/README.md b/docs/features/README.md index 34e6da5d..5f7dc4d2 100644 --- a/docs/features/README.md +++ b/docs/features/README.md @@ -23,3 +23,8 @@ ##### [2.4.2 Error Handling](safety/error_handling.md) ##### [2.4.3 Null Safety](safety/null_safety.md) ##### [2.4.4 Generics](safety/generics.md) + +#### [2.5 🔁 Functions](functions/README.md) +##### [2.5.1 Pure Functions](functions/pure_functions.md) +##### [2.5.2 Total Functions](functions/total_functions.md) +##### [2.5.3 Meta Functions](functions/meta_functions.md) diff --git a/docs/features/functions/README.md b/docs/features/functions/README.md new file mode 100644 index 00000000..ceede2f1 --- /dev/null +++ b/docs/features/functions/README.md @@ -0,0 +1,17 @@ +⬅ [🏠 Home](../../README.md) + +⬅ [2 🛠 Features](../README.md) + +# 2.5 🔁 Functions + +## 📄 Contents + +### [2.5.1 Pure Functions](pure_functions.md) +### [2.5.2 Total Functions](total_functions.md) +### [2.5.3 Meta Functions](meta_functions.md) + +## Introduction + +The [README](../../../README.md) introduces `pure`, `total`, and `meta` functions at the level of intuition. +These pages go further: +The proofs behind the design, the edge cases, and the literature they draw on. diff --git a/docs/features/functions/meta_functions.md b/docs/features/functions/meta_functions.md new file mode 100644 index 00000000..f16d115b --- /dev/null +++ b/docs/features/functions/meta_functions.md @@ -0,0 +1,30 @@ +⬅ [🏠 Home](../../README.md) + +⬅ [2 🛠 Features](../README.md) + +⬅ [2.5 🔁 Functions](README.md) + +# 2.5.3 Meta Functions + +**A meta function must be total, not merely recommended.** +Proving a function is total normally means compiling and checking it, but the compiler is mid-compile already when it needs to check a `meta` function, which sounds circular. +We resolve this by not proving it at all: +A meta function's body is held to the same four restrictions as `total` functions. +This is a syntactic well-formedness rule, not an evaluation. +The checker never has to *run* a meta function to know it terminates, any more than a borrow checker has to run a program to know it doesn't alias. +That sidesteps the meta-compiler regress entirely. + +**Should users be able to write general-purpose `meta` functions at all?** +For now, we think not, or only in a closed form: +Restrict `meta` to `@builtin`-gated definitions that ship with the standard library, reviewed by us, small in number, rather than something any Mamba user can write. +The `Measurable`/`measure()` case discussed in [Total Functions](total_functions.md) is the exception, because we found a restriction, straight-line, no recursion at all, that's safe to open up precisely because it removes recursion from the picture entirely. +General-purpose `meta` has no equivalent escape hatch: +Its whole value is running arbitrary compile-time computation, so the best we can offer a user-authored `meta` function is "restricted to structural recursion, checked", which is weaker than "cannot possibly fail to terminate". +Given that `meta` is already a niche, mostly-stdlib feature, the risk/benefit favours keeping it closed until there's a concrete case for opening it. + +**Worth stating explicitly: even with the structural-recursion restriction, suppose the checker's syntactic rule is ever wrong**, and it lets through something that shouldn't have been accepted. +The failure mode is the compiler hangs evaluating a `meta` function during `total`-checking. +That is a strictly preferable failure to the one `total` exists to prevent. +A hung compile happens on a developer's own machine or in CI, is attributable to a specific function, is interruptible, and blocks the broken code from ever being shipped. +A hung `total` function at runtime is the exact production failure, denial of service, a stuck request thread, resource exhaustion, that the whole feature was built to rule out, except now dressed up with a false badge of having been proven safe. +So while the goal is to make compile-time non-termination impossible by construction, if we ever have to choose between an imperfect static check that occasionally hangs the compiler and a looser one that occasionally ships a non-terminating `total` function, we should choose the former without hesitation, and pair it with a recursion/step budget during meta evaluation (`error: meta evaluation exceeded N steps`), so the failure shows up as a diagnostic rather than a silent freeze. diff --git a/docs/features/functions/pure_functions.md b/docs/features/functions/pure_functions.md new file mode 100644 index 00000000..75297221 --- /dev/null +++ b/docs/features/functions/pure_functions.md @@ -0,0 +1,19 @@ +⬅ [🏠 Home](../../README.md) + +⬅ [2 🛠 Features](../README.md) + +⬅ [2.5 🔁 Functions](README.md) + +# 2.5.1 Pure Functions + +A pure function is referentially transparent. +Wherever a call to it appears, that call could be replaced by its result, and the program would behave identically. +Concretely, for a pure function `f`, if `x = y` then `f(x) = f(y)`. + +It also relies on the rules the README lists: +`fin self`, no calling impure functions, only reading `fin` fields or calling `pure` methods on arguments. +Those rules exist so that nothing reachable from a pure function's arguments can be mutated out from under it, directly or indirectly. + +Purity says nothing about termination on its own. +A pure function can still loop forever. +That's what `total` is for, covered next. diff --git a/docs/features/functions/total_functions.md b/docs/features/functions/total_functions.md new file mode 100644 index 00000000..db0985d9 --- /dev/null +++ b/docs/features/functions/total_functions.md @@ -0,0 +1,157 @@ +⬅ [🏠 Home](../../README.md) + +⬅ [2 🛠 Features](../README.md) + +⬅ [2.5 🔁 Functions](README.md) + +# 2.5.2 Total Functions + +## Ackermann's function, in full + +The README shows this function as an example of something that halts but can never be marked `total`: + +```mamba +# some syntax here such as guard arms which are not in the language yet +def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) with + (m, n) if m = 0 => n + 1 + (m, n) if n = 0 => ackermann(m - 1, 1) + (m, n) => ackermann(m - 1, ackermann(m, n - 1)) +end +``` + +This is the classic Ackermann function: + +``` +A(m, n) = + n + 1 if m = 0 + A(m - 1, 1) if m > 0 and n = 0 + A(m - 1, A(m, n - 1)) if m > 0 and n > 0 +``` + +It halts on every `(m, n)`, and its definition looks like an entirely ordinary pair of recursive calls. +But it is the textbook example of a total, computable function that is **not primitive recursive**. + +Primitive recursion means the depth of the recursion is bounded in advance by a single value that strictly decreases toward a base case. +A `for` loop over a `SizedIterator` is primitive recursive: +Its iteration count is fixed by the collection's size before the loop starts. +Structural descent on a single `Measurable` value is primitive recursive too: +Its number of recursive calls is bounded by the starting measure. +This is exactly the expressive class `total` restricts you to. + +Concretely, our `StrictlyDecreases`/`Measurable` scheme cannot accept `A`: + +- The call `A(m, n - 1)` doesn't decrease `m` at all, only `n`. +- The outer call `A(m - 1, A(m, n - 1))` decreases `m`, but its second argument is whatever the inner call returns. + This can be vastly larger than the original `n`. + +That does not mean `A`'s termination is unprovable. +Compare `(m, n)` lexicographically, with `m` as the dominant component: +`A(m, n - 1)` decreases in the second slot, and `A(m - 1, A(m, n - 1))` decreases in the first slot no matter how large the second slot becomes. +That is a genuine well-founded order. +Its order type is `ω²` (omega squared), an ordinal number describing "pairs of naturals, compared by the first component first". +So Ackermann's termination is a completely ordinary fact, provable by ordinary nested induction. +It is just not provable by the *specific* technique Mamba's `total` checker uses. + +What `A` lacks is a *flat* measure, which is what Mamba's scheme requires. +`measure()` returns one comparable value, and `decreases` is one comparison: +`self.measure() < other.measure()`. +There is no way to fold `(m, n)` into a single number so that "the pair got lexicographically smaller" becomes "the folded number got smaller", because `n` can grow without any fixed bound in the very same step that `m` shrinks by one. +No finite weighting of `m` and `n` into a single scalar survives that. + +So a function shaped like Ackermann's can never be marked `total` in Mamba today, not because no well-founded measure exists for it, but because Mamba's well-founded order is deliberately flat, and Ackermann needs a lexicographic (or ordinal) one. +Other systems that support richer measures accept it directly: + +- ACL2 admits Ackermann-shaped definitions using measures into the ordinals below `ε₀` (epsilon-nought) instead of plain naturals. +- Structural checkers built on multi-path call-graph analysis, the *size-change principle* (Lee, Jones, Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001), accept the ordinary two-clause Ackermann definition too, by tracking that some combination of argument positions decreases along every call path, rather than one designated one. + Agda's termination checker works this way. + +Generalising `Measurable` from a flat scalar to a lexicographic tuple, an ordinal, or a multi-argument call-graph analysis is a real, addressable extension. +We don't implement any of that today, but it's worth keeping on the table, and it connects directly to the next question. + +## Opening `Measurable` to custom types + +`Measurable` is currently a special built-in trait that cannot be implemented for custom types. +The README argues this restriction can be relaxed. +Here is the reasoning behind that in full, since it's worth getting right rather than asserting. + +**Does opening `Measurable` up to custom types open a Pandora's box?** +Not automatically. +Whether it's safe comes down to exactly two properties. +Neither of them is "does the user's `measure()` look honest". + +1. `measure()` must be a total, deterministic, pure function into a well-founded codomain. + Well-founded means the codomain has no infinite descending chain. + `PosInt`/`Nat` qualifies. + `Int` does not: + `5, 4, 3, ..., -1, -2, ...` never bottoms out, so `Measurable for Int` needs to measure into `PosInt` (e.g. `self.abs()`), not return `self` directly. +2. The compiler must independently re-check the decrease at every call site. + It cannot just check that a type implements `Measurable` and stop there. + +The second point is the one that actually matters, and it is easy to get backwards. +`measure()`'s *meaning* is irrelevant to soundness. +A user can write `measure()` as `self.weird_field - 7` for a type with no obvious notion of "size", and the scheme stays perfectly sound, as long as the compiler substitutes the concrete call-site expressions into `measure()` and mechanically checks the resulting inequality on every recursive edge, every time. +What would actually break soundness is trusting the existence of a `Measurable` implementation as a blanket permission, without redoing that check per call site. +That is the real Pandora's box: +Not user-defined measures, but a compiler that stops verifying once a trait box is ticked. + +This is not a novel design. +It is precisely how mainstream deductive systems already let users define arbitrary well-founded relations on arbitrary types: + +- Nordström's account of terminating general recursion in Martin-Löf type theory (Nordström, *Terminating General Recursion*, BIT 28, 1988), and Bove and Capretta's method for modelling general recursion via an inductively defined domain predicate (Bove & Capretta, *Modelling General Recursion in Type Theory*, Nordic Journal of Computing 12, 2005), both let a user supply an arbitrary well-founded relation on an arbitrary type. + Every recursive call still needs its own decrease proof. +- Coq's `Fix`/`well_founded_induction`, Agda's `Induction.WellFounded` module, and Lean 4's `termination_by`/`decreasing_by` all work the same way. + Pick any type. + Pick any well-founded relation on it. + The tool discharges a fresh proof obligation for every recursive call, usually via an automatic arithmetic decision procedure, Lean's `omega` tactic, for instance. +- ACL2 requires every recursive definition to carry a `:measure`, which can be an arbitrary term into the ordinals below `ε₀`, checked automatically by ACL2's own arithmetic and rewriting engine. + Nothing about the measure's shape is restricted beyond "well-founded, and the prover can actually discharge the resulting inequality". + +None of these systems restrict well-founded relations to some closed set of "primitive" types. +They restrict what has to be *proved* about a user-supplied relation, at the point it is used. +That is the model worth copying: +`Measurable` open to any type, `measure()` open to any pure logic, every recursive call in a `total` function re-verified, not merely trait-gated. + +**Re-verifying "does the measure decrease" is itself a decision problem, though.** +This is where the straight-line restriction on `measure()`, no recursion, no loops, matters for a reason beyond "a stray `measure()` can't fail to terminate when evaluated once". +Proving the decrease for *every possible input*, not just one instance, is a decidability question in its own right, and the answer depends on what arithmetic `measure()` is allowed to use. + +- Restricted to `Add`, `Sub`, `Eq`, `Comparable`, which is exactly `Measurable`'s current bound, the resulting inequality lives in Presburger arithmetic: + Linear arithmetic over integers, no multiplication of two non-constant terms. + Presburger arithmetic is decidable (Presburger, 1929), even though the worst case is expensive (Fischer and Rabin proved a double-exponential lower bound in 1974). + This is also the fragment SMT-based verifiers lean on for their own `decreases` clauses (Dafny, F*, Lean's `omega`). +- Add `Mul` between two non-constant `Measurable` values, and this guarantee breaks. + General Diophantine reasoning, arithmetic with unrestricted multiplication, is undecidable. + This is Hilbert's tenth problem, resolved negatively by Matiyasevich in 1970, building on Davis, Putnam, and Robinson's earlier work. + There is no algorithm that decides, in general, whether an arbitrary polynomial equation over the integers has an integer solution, and the same wall shows up here. + +So `Measurable`'s existing trait bound, `Add, Sub, Eq, Comparable`, deliberately excluding `Mul`, is not arbitrary minimalism. +It is exactly the boundary that keeps "does this measure decrease" a decidable question. +Any future relaxation of `Measurable` needs to treat adding `Mul` as a real decidability boundary, not a convenience feature. + +One more requirement, easy to miss. +If `measure()` calls another pure function, the `Str` example in the README calls `.len()`, that function must also be non-recursive. +For the compiler's check to go through, it must be fully unfoldable into the same `Add`/`Sub`/`Eq`/`Comparable` fragment, or treated as an opaque, axiomatically trusted primitive, the way a compiler-provided `len()` can be. +This is a whole-program property, the transitive closure of everything `measure()` reaches, not just a property of `measure()`'s own body. +It is checkable the same way though: +Syntactically, at the definition site, with no evaluation required. + +**Conclusion.** `Measurable` does not need to stay closed to built-in types as a matter of correctness. +The correctness requirement is narrower, and already well understood in the literature above: +A total, deterministic, pure `measure()` into a well-founded, `Mul`-free arithmetic fragment, with every recursive call re-verified individually rather than trusted from the trait's existence. +Closing `Measurable` to built-in types only is a fine *simplicity* choice for an early version of the language. +It should not be sold as a *soundness* one. + +**Further reading**, on the pieces above: + +- M. Presburger, *Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen*, 1929. + The original decidability result for linear integer arithmetic. +- M. J. Fischer, M. O. Rabin, *Super-Exponential Complexity of Presburger Arithmetic*, 1974. + The cost of that decidability, in the worst case. +- Y. Matiyasevich, *Enumerable Sets are Diophantine*, 1970. + The negative resolution of Hilbert's tenth problem, why unrestricted multiplication breaks decidability. +- C. S. Lee, N. D. Jones, A. M. Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001. + A decidable, fully automatic method for proving termination via call-graph decrease analysis, close in spirit to Mamba's own call-tree rule. +- B. Nordström, *Terminating General Recursion*, BIT 28, 1988. +- A. Bove, V. Capretta, *Modelling General Recursion in Type Theory*, Nordic Journal of Computing 12, 2005. +- M. Kaufmann, P. Manolios, J S. Moore, *Computer-Aided Reasoning: An Approach*, 2000. + ACL2's ordinal-based `:measure` mechanism. From 69d7476beb62857773a2bdca26168a7995c89383 Mon Sep 17 00:00:00 2001 From: Joel Abrahams Date: Fri, 28 Aug 2026 13:03:25 +0200 Subject: [PATCH 4/5] fix: void functions in machine code - Python backend with nested loops caused indentationerror - Add _ne_ to built-in Int and Float primitives --- README.md | 2 +- docs/features/functions/total_functions.md | 2 +- src/backend/cranelift/convert/control_flow.rs | 52 +++++++++++++------ src/backend/cranelift/convert/definition.rs | 27 ++++++++-- src/backend/cranelift/convert/mod.rs | 39 +++++++++++--- src/backend/python/ast/mod.rs | 17 ++++-- src/check/resource/primitive/float.py | 2 + src/check/resource/primitive/int.py | 2 + tests/execution.rs | 16 ++++++ .../valid/function/and_unsupported.mamba | 3 ++ .../valid/function/both_branches_return.mamba | 6 +++ .../valid/function/early_return.mamba | 7 +++ .../valid/function/float_comparison.mamba | 4 ++ .../resource/valid/function/forward_ref.mamba | 9 ++++ .../valid/function/mod_unsupported.mamba | 1 + tests/resource/valid/function/neq_float.mamba | 3 ++ tests/resource/valid/function/neq_int.mamba | 3 ++ .../valid/function/nested_for_sum.mamba | 7 +++ .../valid/function/not_unsupported.mamba | 2 + .../valid/function/or_unsupported.mamba | 3 ++ .../valid/function/pow_unsupported.mamba | 1 + .../valid/function/recursion_factorial.mamba | 6 +++ .../valid/function/simple_reassign.mamba | 3 ++ .../valid/function/void_implicit_body.mamba | 7 +++ .../valid/function/while_unsupported.mamba | 5 ++ 25 files changed, 198 insertions(+), 31 deletions(-) create mode 100644 tests/resource/valid/function/and_unsupported.mamba create mode 100644 tests/resource/valid/function/both_branches_return.mamba create mode 100644 tests/resource/valid/function/early_return.mamba create mode 100644 tests/resource/valid/function/float_comparison.mamba create mode 100644 tests/resource/valid/function/forward_ref.mamba create mode 100644 tests/resource/valid/function/mod_unsupported.mamba create mode 100644 tests/resource/valid/function/neq_float.mamba create mode 100644 tests/resource/valid/function/neq_int.mamba create mode 100644 tests/resource/valid/function/nested_for_sum.mamba create mode 100644 tests/resource/valid/function/not_unsupported.mamba create mode 100644 tests/resource/valid/function/or_unsupported.mamba create mode 100644 tests/resource/valid/function/pow_unsupported.mamba create mode 100644 tests/resource/valid/function/recursion_factorial.mamba create mode 100644 tests/resource/valid/function/simple_reassign.mamba create mode 100644 tests/resource/valid/function/void_implicit_body.mamba create mode 100644 tests/resource/valid/function/while_unsupported.mamba diff --git a/README.md b/README.md index 5101b6e6..8976add9 100644 --- a/README.md +++ b/README.md @@ -399,7 +399,7 @@ Not every function that obviously halts can be marked `total`. ```mamba # some syntax here such as guard arms which are not in the language yet -def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) with +def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) where (m, n) if m = 0 => n + 1 (m, n) if n = 0 => ackermann(m - 1, 1) (m, n) => ackermann(m - 1, ackermann(m, n - 1)) diff --git a/docs/features/functions/total_functions.md b/docs/features/functions/total_functions.md index db0985d9..d395155d 100644 --- a/docs/features/functions/total_functions.md +++ b/docs/features/functions/total_functions.md @@ -12,7 +12,7 @@ The README shows this function as an example of something that halts but can nev ```mamba # some syntax here such as guard arms which are not in the language yet -def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) with +def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) where (m, n) if m = 0 => n + 1 (m, n) if n = 0 => ackermann(m - 1, 1) (m, n) => ackermann(m - 1, ackermann(m, n - 1)) diff --git a/src/backend/cranelift/convert/control_flow.rs b/src/backend/cranelift/convert/control_flow.rs index 841da3e0..e8e15564 100644 --- a/src/backend/cranelift/convert/control_flow.rs +++ b/src/backend/cranelift/convert/control_flow.rs @@ -1,5 +1,5 @@ use cranelift_codegen::ir::condcodes::IntCC; -use cranelift_codegen::ir::{types, InstBuilder}; +use cranelift_codegen::ir::{types, InstBuilder, TrapCode}; use crate::backend::cranelift::convert::common::fun_name; use crate::backend::cranelift::convert::FnLower; @@ -18,7 +18,7 @@ impl<'a> FnLower<'a> { /// reassigning an outer variable with `:=`, which isn't a new binding, still works exactly as /// expected; only fresh bindings are undone here, since a `:=` never touches `self.vars`, only /// the value already tracked by whichever `Variable` the name already resolves to). - fn lower_scoped_stmt(&mut self, ast: &ASTTy) -> BackendResult<()> { + fn lower_scoped_stmt(&mut self, ast: &ASTTy) -> BackendResult { let snapshot = self.vars.clone(); let result = self.lower_stmt(ast); self.vars = snapshot; @@ -28,12 +28,20 @@ impl<'a> FnLower<'a> { /// Lower an `IfElse` in statement position: both arms are lowered as statements, and control /// re-joins in a shared `merge_block` afterwards (or falls straight through to it when there /// is no `else`). + /// + /// Returns whether this `if` definitely terminates the enclosing block itself -- only + /// possible when there's an `else` and *both* arms return, since otherwise the false path + /// (falling through with no `else`, or an `else` that doesn't return) always reaches + /// `merge_block` and execution continues from there. When both arms do return, `merge_block` + /// is never actually jumped into -- it's given a `trap` as a placeholder terminator (dead + /// code, never executed) purely so it stays valid IR; Cranelift requires every block in the + /// layout to end in a terminator whether or not it's reachable. pub(super) fn lower_if_else_stmt( &mut self, cond: &ASTTy, then: &ASTTy, el: Option<&ASTTy>, - ) -> BackendResult<()> { + ) -> BackendResult { let cond_value = self.lower_expr(cond)?; let then_block = self.builder.create_block(); let merge_block = self.builder.create_block(); @@ -48,17 +56,27 @@ impl<'a> FnLower<'a> { .brif(cond_value, then_block, &[], else_block, &[]); self.builder.switch_to_block(then_block); - self.lower_scoped_stmt(then)?; - self.builder.ins().jump(merge_block, &[]); - - if let Some(el) = el { - self.builder.switch_to_block(else_block); - self.lower_scoped_stmt(el)?; + let then_returned = self.lower_scoped_stmt(then)?; + if !then_returned { self.builder.ins().jump(merge_block, &[]); } + let both_returned = if let Some(el) = el { + self.builder.switch_to_block(else_block); + let el_returned = self.lower_scoped_stmt(el)?; + if !el_returned { + self.builder.ins().jump(merge_block, &[]); + } + then_returned && el_returned + } else { + false + }; + self.builder.switch_to_block(merge_block); - Ok(()) + if both_returned { + self.builder.ins().trap(TrapCode::unwrap_user(1)); + } + Ok(both_returned) } /// Lower a `For` loop in statement position. @@ -140,11 +158,15 @@ impl<'a> FnLower<'a> { self.vars.insert(var_name, (loop_var, ty)); let result = self.lower_stmt(body); self.vars = snapshot; - result?; - let current = self.builder.use_var(loop_var); - let next = self.builder.ins().iadd(current, step_value); - self.builder.def_var(loop_var, next); - self.builder.ins().jump(header_block, &[]); + // If the body definitely returned (an early `return` inside the loop), `body_block` is + // already filled -- adding the increment/back-edge would panic, and there's no next + // iteration to run anyway, so skip straight to `exit_block` without touching it further. + if !result? { + let current = self.builder.use_var(loop_var); + let next = self.builder.ins().iadd(current, step_value); + self.builder.def_var(loop_var, next); + self.builder.ins().jump(header_block, &[]); + } self.builder.switch_to_block(exit_block); Ok(()) diff --git a/src/backend/cranelift/convert/definition.rs b/src/backend/cranelift/convert/definition.rs index 018ce5ea..2a410c27 100644 --- a/src/backend/cranelift/convert/definition.rs +++ b/src/backend/cranelift/convert/definition.rs @@ -101,6 +101,7 @@ pub(super) fn define_function( funcs: &Funcs, want_asm: bool, ) -> BackendResult> { + let is_void = sig.returns.is_empty(); let mut ctx = ClifContext::new(); ctx.set_disasm(want_asm); ctx.func = Function::with_name_signature(UserFuncName::user(0, func_id.as_u32()), sig); @@ -127,7 +128,21 @@ pub(super) fn define_function( lower.bind_arg(arg, value)?; } + // A void function's body is lowered as a statement, never a value-producing tail -- + // otherwise a body that's just a bare statement (e.g. `def f() := print(x)`, or a + // `do ... end` block with no explicit trailing `return`) would wrongly fall through + // `lower_tail`'s catch-all, which tries to evaluate it as an expression and return its + // value. `print` in particular is only special-cased in `lower_stmt`, so that fallback + // surfaces as a confusing "Undefined function 'print'" rather than actually running it. match body { + // Only add the implicit trailing `return` if the body didn't already end with one + // itself (see `lower_stmt`'s doc comment) -- it would otherwise try to add an + // instruction to an already-filled block and panic. + Some(body) if is_void => { + if !lower.lower_stmt(body)? { + lower.builder.ins().return_(&[]); + } + } Some(body) => lower.lower_tail(body)?, None => { lower.builder.ins().return_(&[]); @@ -175,11 +190,17 @@ pub(super) fn define_main( puts_id, }; + let mut terminated = false; for statement in statements { - lower.lower_stmt(statement)?; + if lower.lower_stmt(statement)? { + terminated = true; + break; + } + } + if !terminated { + let zero = lower.builder.ins().iconst(types::I32, 0); + lower.builder.ins().return_(&[zero]); } - let zero = lower.builder.ins().iconst(types::I32, 0); - lower.builder.ins().return_(&[zero]); lower.builder.seal_all_blocks(); lower.builder.finalize(); diff --git a/src/backend/cranelift/convert/mod.rs b/src/backend/cranelift/convert/mod.rs index 707038e0..99f7bae9 100644 --- a/src/backend/cranelift/convert/mod.rs +++ b/src/backend/cranelift/convert/mod.rs @@ -118,22 +118,45 @@ struct FnLower<'a> { impl<'a> FnLower<'a> { /// Lower `ast` as a statement: for side effects only, its value (if any) is discarded. - fn lower_stmt(&mut self, ast: &ASTTy) -> BackendResult<()> { + /// + /// Returns whether `ast` definitely ended the current block with a `return` (`Ok(true)`) -- + /// once that happens, the block is "filled" and Cranelift panics if anything else tries to + /// add an instruction to it, so every caller that keeps lowering more statements into the + /// same block (a `Block`'s later statements, the synthetic top-level `return` a void + /// function's body doesn't already end with, ...) needs to stop the moment this comes back + /// `true`, exactly the way unreachable code after a `return` would in any straight-line IR. + fn lower_stmt(&mut self, ast: &ASTTy) -> BackendResult { match &ast.node { - NodeTy::VariableDef { .. } => self.lower_variable_def(ast), - NodeTy::Reassign { .. } => self.lower_reassign(ast), + NodeTy::VariableDef { .. } => self.lower_variable_def(ast).map(|()| false), + NodeTy::Reassign { .. } => self.lower_reassign(ast).map(|()| false), NodeTy::IfElse { cond, then, el } => self.lower_if_else_stmt(cond, then, el.as_deref()), - NodeTy::For { expr, col, body } => self.lower_for(expr, col, body), + NodeTy::For { expr, col, body } => self.lower_for(expr, col, body).map(|()| false), NodeTy::Block { statements } => { for statement in statements { - self.lower_stmt(statement)?; + if self.lower_stmt(statement)? { + return Ok(true); + } } - Ok(()) + Ok(false) } NodeTy::FunctionCall { name, .. } if name.name == PRINT => { - self.lower_print(ast).map(|_| ()) + self.lower_print(ast).map(|_| false) + } + NodeTy::FunctionCall { .. } => self.lower_call_stmt(ast).map(|()| false), + // An early `return`/`return ` doesn't have to be a function's literal last + // statement (see `lower_tail`, which handles these same two node shapes for that + // position) -- it can appear anywhere a statement can, e.g. inside an `if` branch + // that isn't the function's own tail. Mirror `lower_tail`'s handling here so that + // shape works too, for both void and value-returning functions. + NodeTy::Return { expr } => { + let value = self.lower_expr(expr)?; + self.builder.ins().return_(&[value]); + Ok(true) + } + NodeTy::ReturnEmpty => { + self.builder.ins().return_(&[]); + Ok(true) } - NodeTy::FunctionCall { .. } => self.lower_call_stmt(ast), other => Err(BackendErr::unimplemented( ast, &format!("{other:?} statement"), diff --git a/src/backend/python/ast/mod.rs b/src/backend/python/ast/mod.rs index 0818bebe..5ba75b73 100644 --- a/src/backend/python/ast/mod.rs +++ b/src/backend/python/ast/mod.rs @@ -490,12 +490,23 @@ fn newline_if_body(core: &PythonCore, ind: usize) -> String { fn newline_delimited(items: &[PythonCore], ind: usize) -> String { let mut s = String::new(); - items - .iter() - .for_each(|item| writeln!(s, "{}{}", indent(ind), to_py(item, ind)).unwrap()); + write_items(&mut s, items, ind); s } +/// Render each of `items` at `ind`, flattening any item that's itself a [`PythonCore::Block`] +/// (recursively, in case of several layers) rather than indenting it as a single opaque item. +/// +/// A `Block` already indents each of its own statements uniformly at `ind` (this is the same function, called again one level down). +fn write_items(s: &mut String, items: &[PythonCore], ind: usize) { + for item in items { + match item { + PythonCore::Block { statements } => write_items(s, statements, ind), + other => writeln!(s, "{}{}", indent(ind), to_py(other, ind)).unwrap(), + } + } +} + fn comma_delimited(items: &[PythonCore], ind: usize) -> String { let mut s = String::new(); items diff --git a/src/check/resource/primitive/float.py b/src/check/resource/primitive/float.py index 9873543a..ae78f634 100644 --- a/src/check/resource/primitive/float.py +++ b/src/check/resource/primitive/float.py @@ -42,3 +42,5 @@ def __lt__(self, other: Union[int, float]) -> bool: pass def __str__(self) -> str: pass def __eq__(self, other: float) -> bool: pass + + def __ne__(self, other: float) -> bool: pass diff --git a/src/check/resource/primitive/int.py b/src/check/resource/primitive/int.py index 3e3f820d..ce632b34 100644 --- a/src/check/resource/primitive/int.py +++ b/src/check/resource/primitive/int.py @@ -48,3 +48,5 @@ def __lt__(self, other: Union[int, float]) -> bool: pass def __str__(self) -> str: pass def __eq__(self, other: int) -> bool: pass + + def __ne__(self, other: int) -> bool: pass diff --git a/tests/execution.rs b/tests/execution.rs index cd935c2c..2eef5b27 100644 --- a/tests/execution.rs +++ b/tests/execution.rs @@ -24,6 +24,16 @@ use tests_util::{resource_path, run_cli, run_via_asm, run_via_bin, run_via_pytho #[test_matrix([run_via_python, run_via_bin], &["function"], "for_loop_shadow.mamba" => "6\n100\n")] #[test_matrix([run_via_python, run_via_bin], &["function"], "def_in_if_shadow.mamba" => "999\n100\n")] #[test_matrix([run_via_python, run_via_bin], &["function"], "def_in_loop_shadow.mamba" => "999\n999\n999\n100\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "neq_int.mamba" => "1\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "neq_float.mamba" => "1\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "float_comparison.mamba" => "1\n0\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "simple_reassign.mamba" => "5\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "forward_ref.mamba" => "4\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "void_implicit_body.mamba" => "4\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "recursion_factorial.mamba" => "120\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "early_return.mamba" => "7\n7\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "both_branches_return.mamba" => "-1\n1\n")] +#[test_matrix([run_via_python, run_via_bin], &["function"], "nested_for_sum.mamba" => "9\n")] fn execution(run: Runner, dirs: &[&str], file: &str) -> String { run(dirs, file).unwrap() } @@ -68,6 +78,12 @@ fn bin_only_execution(run: Runner, dirs: &[&str], file: &str) -> String { #[test_case("print_two_args_unsupported.mamba", "!= 1 argument")] #[test_case("print_interpolated_unsupported.mamba", "interpolated string")] #[test_case("no_initializer_unsupported.mamba", "variable definition")] +#[test_case("and_unsupported.mamba", "And")] +#[test_case("or_unsupported.mamba", "Or")] +#[test_case("not_unsupported.mamba", "Not")] +#[test_case("pow_unsupported.mamba", "Pow")] +#[test_case("mod_unsupported.mamba", "Mod")] +#[test_case("while_unsupported.mamba", "While")] fn bin_backend_rejects_gracefully(file: &str, expected_substring: &str) { let err = run_via_bin(&["function"], file) .expect_err("this fixture is deliberately outside the Cranelift backend's support"); diff --git a/tests/resource/valid/function/and_unsupported.mamba b/tests/resource/valid/function/and_unsupported.mamba new file mode 100644 index 00000000..59930a67 --- /dev/null +++ b/tests/resource/valid/function/and_unsupported.mamba @@ -0,0 +1,3 @@ +def a := True +def b := False +if a and b then print(1) else print(0) diff --git a/tests/resource/valid/function/both_branches_return.mamba b/tests/resource/valid/function/both_branches_return.mamba new file mode 100644 index 00000000..59d5bc8e --- /dev/null +++ b/tests/resource/valid/function/both_branches_return.mamba @@ -0,0 +1,6 @@ +def sign(x: Int) -> Int := do + if x < 0 then return -1 else return 1 +end + +print(sign(-3)) +print(sign(3)) diff --git a/tests/resource/valid/function/early_return.mamba b/tests/resource/valid/function/early_return.mamba new file mode 100644 index 00000000..832c2188 --- /dev/null +++ b/tests/resource/valid/function/early_return.mamba @@ -0,0 +1,7 @@ +def abs_val(x: Int) -> Int := do + if x < 0 then return -x + return x +end + +print(abs_val(-7)) +print(abs_val(7)) diff --git a/tests/resource/valid/function/float_comparison.mamba b/tests/resource/valid/function/float_comparison.mamba new file mode 100644 index 00000000..a75fb731 --- /dev/null +++ b/tests/resource/valid/function/float_comparison.mamba @@ -0,0 +1,4 @@ +def a := 1.5 +def b := 2.5 +if a < b then print(1) else print(0) +if a > b then print(1) else print(0) diff --git a/tests/resource/valid/function/forward_ref.mamba b/tests/resource/valid/function/forward_ref.mamba new file mode 100644 index 00000000..22b9cdc8 --- /dev/null +++ b/tests/resource/valid/function/forward_ref.mamba @@ -0,0 +1,9 @@ +def main_fn() := do + print(helper(3)) +end + +def helper(x: Int) -> Int := do + return x + 1 +end + +main_fn() diff --git a/tests/resource/valid/function/mod_unsupported.mamba b/tests/resource/valid/function/mod_unsupported.mamba new file mode 100644 index 00000000..9a9f0c3c --- /dev/null +++ b/tests/resource/valid/function/mod_unsupported.mamba @@ -0,0 +1 @@ +print(10 mod 3) diff --git a/tests/resource/valid/function/neq_float.mamba b/tests/resource/valid/function/neq_float.mamba new file mode 100644 index 00000000..4bd2a05b --- /dev/null +++ b/tests/resource/valid/function/neq_float.mamba @@ -0,0 +1,3 @@ +def a := 10.0 +def b := 4.0 +if a != b then print(1) else print(0) diff --git a/tests/resource/valid/function/neq_int.mamba b/tests/resource/valid/function/neq_int.mamba new file mode 100644 index 00000000..4194d460 --- /dev/null +++ b/tests/resource/valid/function/neq_int.mamba @@ -0,0 +1,3 @@ +def a := 10 +def b := 4 +if a != b then print(1) else print(0) diff --git a/tests/resource/valid/function/nested_for_sum.mamba b/tests/resource/valid/function/nested_for_sum.mamba new file mode 100644 index 00000000..5d658009 --- /dev/null +++ b/tests/resource/valid/function/nested_for_sum.mamba @@ -0,0 +1,7 @@ +def total := 0 +for i in 0 .. 3 do + for j in 0 .. 3 do + total := total + 1 + end +end +print(total) diff --git a/tests/resource/valid/function/not_unsupported.mamba b/tests/resource/valid/function/not_unsupported.mamba new file mode 100644 index 00000000..149aeda4 --- /dev/null +++ b/tests/resource/valid/function/not_unsupported.mamba @@ -0,0 +1,2 @@ +def a := True +if not a then print(1) else print(0) diff --git a/tests/resource/valid/function/or_unsupported.mamba b/tests/resource/valid/function/or_unsupported.mamba new file mode 100644 index 00000000..14b35664 --- /dev/null +++ b/tests/resource/valid/function/or_unsupported.mamba @@ -0,0 +1,3 @@ +def a := True +def b := False +if a or b then print(1) else print(0) diff --git a/tests/resource/valid/function/pow_unsupported.mamba b/tests/resource/valid/function/pow_unsupported.mamba new file mode 100644 index 00000000..c91c9c7a --- /dev/null +++ b/tests/resource/valid/function/pow_unsupported.mamba @@ -0,0 +1 @@ +print(2 ^ 3) diff --git a/tests/resource/valid/function/recursion_factorial.mamba b/tests/resource/valid/function/recursion_factorial.mamba new file mode 100644 index 00000000..c1d6cb17 --- /dev/null +++ b/tests/resource/valid/function/recursion_factorial.mamba @@ -0,0 +1,6 @@ +def factorial(n: Int) -> Int := do + if n <= 1 then return 1 + return n * factorial(n - 1) +end + +print(factorial(5)) diff --git a/tests/resource/valid/function/simple_reassign.mamba b/tests/resource/valid/function/simple_reassign.mamba new file mode 100644 index 00000000..a2291610 --- /dev/null +++ b/tests/resource/valid/function/simple_reassign.mamba @@ -0,0 +1,3 @@ +def a := 1 +a := 5 +print(a) diff --git a/tests/resource/valid/function/void_implicit_body.mamba b/tests/resource/valid/function/void_implicit_body.mamba new file mode 100644 index 00000000..030f17f2 --- /dev/null +++ b/tests/resource/valid/function/void_implicit_body.mamba @@ -0,0 +1,7 @@ +def helper(x: Int) -> Int := do + return x + 1 +end + +def main_fn() := print(helper(3)) + +main_fn() diff --git a/tests/resource/valid/function/while_unsupported.mamba b/tests/resource/valid/function/while_unsupported.mamba new file mode 100644 index 00000000..a6f17aff --- /dev/null +++ b/tests/resource/valid/function/while_unsupported.mamba @@ -0,0 +1,5 @@ +def i := 0 +while i < 3 do + print(i) + i := i + 1 +end From 40639c15d20da0bb126683d465e792afab8cb94e Mon Sep 17 00:00:00 2001 From: Joel Abrahams Date: Fri, 28 Aug 2026 13:15:37 +0200 Subject: [PATCH 5/5] doc: simplify notes on measurable --- README.md | 42 ++---- docs/features/functions/meta_functions.md | 28 ++-- docs/features/functions/total_functions.md | 155 +++++---------------- 3 files changed, 53 insertions(+), 172 deletions(-) diff --git a/README.md b/README.md index 8976add9..3b12e678 100644 --- a/README.md +++ b/README.md @@ -477,14 +477,9 @@ end Both of the above return a `PosInt`, which is part of the library and implements the `Measurable` trait. This is a special built-in trait of the language, which as of writing cannot be implemented for custom types. -We think this restriction can be relaxed for user types. -The requirement is just that `measure()` be total, deterministic, and pure: defined for every input, always giving the same output for the same input, and free of side effects. -Given that, plus a bounded-below codomain like `PosInt`, the compiler can independently verify at each recursive call site that the measure actually decreases, regardless of which type `measure()` is defined on. -So there's no correctness reason to keep `Measurable` closed to built-in types specifically, only a simplicity one for now. -See [docs/features/functions/total_functions.md](docs/features/functions/total_functions.md#opening-measurable-to-custom-types) for the full reasoning and its caveats. - -This is a materially different, and much safer, question than opening up general-purpose `meta` functions to user-defined recursion. -See below. +Implementing `Measurable` for custom types is future work. +`measure()` only needs to be total, deterministic, and pure, into a bounded-below codomain such as `PosInt`; the compiler verifies the decrease independently at each call site regardless of which type `measure()` is defined on. +See [docs/features/functions/total_functions.md](docs/features/functions/total_functions.md#measurable-and-custom-types) for the reasoning. ```mamba # Trait measurable lives at the heart of this system, and by extension Mamba. @@ -520,30 +515,21 @@ But we can imagine that library writers might find these useful if they wish to ### Meta functions (🇻 x+) -The above also highlights meta functions in the language, which is a necessary evil. -Meta functions are functions which can be evaluated at compile time. -This is somewhat similar to macros in say C++ (or Rust, whose implementation is arguably far superior). -However, the goal of meta functions and traits is to prove properties of variables at compile time. -These functions have two constraints: - -- These may not call non-meta functions (including total and pure functions) or values. -- A meta function is also pure; they have no side-effects. - As this is always implied, we omit the need for the `pure` keyword. +Meta functions are evaluated at compile time, similar to macros in Rust (more so than in C or C++). +Their purpose is to prove properties of the program before code generation, not to generate code. -Additionally: +A meta function: -- A meta function must be total, not just recommended to be. - We can require this without solving the halting problem again, because a meta function's body is held to the same four restrictions as `total` functions. - That's a rule the checker confirms just by looking at the code, without running it. -- We currently keep `meta` closed to the standard library, rather than opening it up to every Mamba user. - General-purpose `meta` doesn't have as clean a safety story as `Measurable` does. -- We may well place additional constraints on meta functions in future. +- May not call non-meta functions or values. +- Is always pure, so the `pure` keyword is omitted. +- Is total: its body is held to the same four restrictions as a `total` function, checked syntactically rather than by running it. -See [docs/features/functions/meta_functions.md](docs/features/functions/meta_functions.md) for why we're keeping `meta` closed for now, and what would need to be true before we open it up. +`meta` is closed to the standard library. +Opening it to user code is future work, though a `measure()` for a custom `Measurable` type (see above) would be a safe first case, since its shape can be checked without running it. +See [docs/features/functions/meta_functions.md](docs/features/functions/meta_functions.md). -**Essentially, the main reason for Mamba having meta functions is to serve as the logical bedrock for provable total functions**. -One other benefit is that compiled functions are evaluated at compile time and not runtime, potentially offering significant speed benefits. -This is useful when one wants to document how one derived a meta in the form of code, without re-calculating it each time at runtime. +Meta functions exist primarily as the logical bedrock for provable `total` functions. +A secondary benefit is performance: a meta computation runs once, at compile time, rather than being recomputed at every call. - A meta function is defined as `def meta my_function() := ...`. - A meta variable is defined `def meta my_var: MyType := ...`, with type annotations being non-optional. diff --git a/docs/features/functions/meta_functions.md b/docs/features/functions/meta_functions.md index f16d115b..152520c8 100644 --- a/docs/features/functions/meta_functions.md +++ b/docs/features/functions/meta_functions.md @@ -6,25 +6,13 @@ # 2.5.3 Meta Functions -**A meta function must be total, not merely recommended.** -Proving a function is total normally means compiling and checking it, but the compiler is mid-compile already when it needs to check a `meta` function, which sounds circular. -We resolve this by not proving it at all: -A meta function's body is held to the same four restrictions as `total` functions. -This is a syntactic well-formedness rule, not an evaluation. -The checker never has to *run* a meta function to know it terminates, any more than a borrow checker has to run a program to know it doesn't alias. -That sidesteps the meta-compiler regress entirely. +A meta function's totality is checked syntactically: +Its body is held to the same restrictions as a `total` function, so the compiler never has to run a meta function to know it terminates, only inspect its shape. +This is what makes evaluating `meta` functions at compile time safe, and avoids a circular dependency on the compiler compiling itself. -**Should users be able to write general-purpose `meta` functions at all?** -For now, we think not, or only in a closed form: -Restrict `meta` to `@builtin`-gated definitions that ship with the standard library, reviewed by us, small in number, rather than something any Mamba user can write. -The `Measurable`/`measure()` case discussed in [Total Functions](total_functions.md) is the exception, because we found a restriction, straight-line, no recursion at all, that's safe to open up precisely because it removes recursion from the picture entirely. -General-purpose `meta` has no equivalent escape hatch: -Its whole value is running arbitrary compile-time computation, so the best we can offer a user-authored `meta` function is "restricted to structural recursion, checked", which is weaker than "cannot possibly fail to terminate". -Given that `meta` is already a niche, mostly-stdlib feature, the risk/benefit favours keeping it closed until there's a concrete case for opening it. +`meta` is closed to the standard library. +Opening it to user code is future work. +A `measure()` for a custom `Measurable` type (see [Total Functions](total_functions.md)) would be a safe first case: restricted to a straight-line, non-recursive form, it cannot fail to terminate by construction. +General-purpose `meta` functions have no equivalent restriction, since their value lies in running arbitrary compile-time computation. -**Worth stating explicitly: even with the structural-recursion restriction, suppose the checker's syntactic rule is ever wrong**, and it lets through something that shouldn't have been accepted. -The failure mode is the compiler hangs evaluating a `meta` function during `total`-checking. -That is a strictly preferable failure to the one `total` exists to prevent. -A hung compile happens on a developer's own machine or in CI, is attributable to a specific function, is interruptible, and blocks the broken code from ever being shipped. -A hung `total` function at runtime is the exact production failure, denial of service, a stuck request thread, resource exhaustion, that the whole feature was built to rule out, except now dressed up with a false badge of having been proven safe. -So while the goal is to make compile-time non-termination impossible by construction, if we ever have to choose between an imperfect static check that occasionally hangs the compiler and a looser one that occasionally ships a non-terminating `total` function, we should choose the former without hesitation, and pair it with a recursion/step budget during meta evaluation (`error: meta evaluation exceeded N steps`), so the failure shows up as a diagnostic rather than a silent freeze. +If the syntactic check on a `meta` function's totality ever has a gap, the failure mode is a hung compile, not a hung program at runtime. diff --git a/docs/features/functions/total_functions.md b/docs/features/functions/total_functions.md index d395155d..4d313f34 100644 --- a/docs/features/functions/total_functions.md +++ b/docs/features/functions/total_functions.md @@ -6,9 +6,9 @@ # 2.5.2 Total Functions -## Ackermann's function, in full +## Ackermann's function -The README shows this function as an example of something that halts but can never be marked `total`: +Ackermann's function halts for every input but cannot be marked `total` in Mamba: ```mamba # some syntax here such as guard arms which are not in the language yet @@ -19,8 +19,6 @@ def ackermann(m: PosInt, n: PosInt) -> PosInt := match (m, n) where end ``` -This is the classic Ackermann function: - ``` A(m, n) = n + 1 if m = 0 @@ -28,130 +26,39 @@ A(m, n) = A(m - 1, A(m, n - 1)) if m > 0 and n > 0 ``` -It halts on every `(m, n)`, and its definition looks like an entirely ordinary pair of recursive calls. -But it is the textbook example of a total, computable function that is **not primitive recursive**. - -Primitive recursion means the depth of the recursion is bounded in advance by a single value that strictly decreases toward a base case. -A `for` loop over a `SizedIterator` is primitive recursive: -Its iteration count is fixed by the collection's size before the loop starts. -Structural descent on a single `Measurable` value is primitive recursive too: -Its number of recursive calls is bounded by the starting measure. -This is exactly the expressive class `total` restricts you to. - -Concretely, our `StrictlyDecreases`/`Measurable` scheme cannot accept `A`: - -- The call `A(m, n - 1)` doesn't decrease `m` at all, only `n`. -- The outer call `A(m - 1, A(m, n - 1))` decreases `m`, but its second argument is whatever the inner call returns. - This can be vastly larger than the original `n`. - -That does not mean `A`'s termination is unprovable. -Compare `(m, n)` lexicographically, with `m` as the dominant component: -`A(m, n - 1)` decreases in the second slot, and `A(m - 1, A(m, n - 1))` decreases in the first slot no matter how large the second slot becomes. -That is a genuine well-founded order. -Its order type is `ω²` (omega squared), an ordinal number describing "pairs of naturals, compared by the first component first". -So Ackermann's termination is a completely ordinary fact, provable by ordinary nested induction. -It is just not provable by the *specific* technique Mamba's `total` checker uses. - -What `A` lacks is a *flat* measure, which is what Mamba's scheme requires. -`measure()` returns one comparable value, and `decreases` is one comparison: -`self.measure() < other.measure()`. -There is no way to fold `(m, n)` into a single number so that "the pair got lexicographically smaller" becomes "the folded number got smaller", because `n` can grow without any fixed bound in the very same step that `m` shrinks by one. -No finite weighting of `m` and `n` into a single scalar survives that. - -So a function shaped like Ackermann's can never be marked `total` in Mamba today, not because no well-founded measure exists for it, but because Mamba's well-founded order is deliberately flat, and Ackermann needs a lexicographic (or ordinal) one. -Other systems that support richer measures accept it directly: - -- ACL2 admits Ackermann-shaped definitions using measures into the ordinals below `ε₀` (epsilon-nought) instead of plain naturals. -- Structural checkers built on multi-path call-graph analysis, the *size-change principle* (Lee, Jones, Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001), accept the ordinary two-clause Ackermann definition too, by tracking that some combination of argument positions decreases along every call path, rather than one designated one. - Agda's termination checker works this way. - -Generalising `Measurable` from a flat scalar to a lexicographic tuple, an ordinal, or a multi-argument call-graph analysis is a real, addressable extension. -We don't implement any of that today, but it's worth keeping on the table, and it connects directly to the next question. - -## Opening `Measurable` to custom types - -`Measurable` is currently a special built-in trait that cannot be implemented for custom types. -The README argues this restriction can be relaxed. -Here is the reasoning behind that in full, since it's worth getting right rather than asserting. - -**Does opening `Measurable` up to custom types open a Pandora's box?** -Not automatically. -Whether it's safe comes down to exactly two properties. -Neither of them is "does the user's `measure()` look honest". - -1. `measure()` must be a total, deterministic, pure function into a well-founded codomain. - Well-founded means the codomain has no infinite descending chain. - `PosInt`/`Nat` qualifies. - `Int` does not: - `5, 4, 3, ..., -1, -2, ...` never bottoms out, so `Measurable for Int` needs to measure into `PosInt` (e.g. `self.abs()`), not return `self` directly. -2. The compiler must independently re-check the decrease at every call site. - It cannot just check that a type implements `Measurable` and stop there. - -The second point is the one that actually matters, and it is easy to get backwards. -`measure()`'s *meaning* is irrelevant to soundness. -A user can write `measure()` as `self.weird_field - 7` for a type with no obvious notion of "size", and the scheme stays perfectly sound, as long as the compiler substitutes the concrete call-site expressions into `measure()` and mechanically checks the resulting inequality on every recursive edge, every time. -What would actually break soundness is trusting the existence of a `Measurable` implementation as a blanket permission, without redoing that check per call site. -That is the real Pandora's box: -Not user-defined measures, but a compiler that stops verifying once a trait box is ticked. - -This is not a novel design. -It is precisely how mainstream deductive systems already let users define arbitrary well-founded relations on arbitrary types: - -- Nordström's account of terminating general recursion in Martin-Löf type theory (Nordström, *Terminating General Recursion*, BIT 28, 1988), and Bove and Capretta's method for modelling general recursion via an inductively defined domain predicate (Bove & Capretta, *Modelling General Recursion in Type Theory*, Nordic Journal of Computing 12, 2005), both let a user supply an arbitrary well-founded relation on an arbitrary type. - Every recursive call still needs its own decrease proof. -- Coq's `Fix`/`well_founded_induction`, Agda's `Induction.WellFounded` module, and Lean 4's `termination_by`/`decreasing_by` all work the same way. - Pick any type. - Pick any well-founded relation on it. - The tool discharges a fresh proof obligation for every recursive call, usually via an automatic arithmetic decision procedure, Lean's `omega` tactic, for instance. -- ACL2 requires every recursive definition to carry a `:measure`, which can be an arbitrary term into the ordinals below `ε₀`, checked automatically by ACL2's own arithmetic and rewriting engine. - Nothing about the measure's shape is restricted beyond "well-founded, and the prover can actually discharge the resulting inequality". - -None of these systems restrict well-founded relations to some closed set of "primitive" types. -They restrict what has to be *proved* about a user-supplied relation, at the point it is used. -That is the model worth copying: -`Measurable` open to any type, `measure()` open to any pure logic, every recursive call in a `total` function re-verified, not merely trait-gated. - -**Re-verifying "does the measure decrease" is itself a decision problem, though.** -This is where the straight-line restriction on `measure()`, no recursion, no loops, matters for a reason beyond "a stray `measure()` can't fail to terminate when evaluated once". -Proving the decrease for *every possible input*, not just one instance, is a decidability question in its own right, and the answer depends on what arithmetic `measure()` is allowed to use. - -- Restricted to `Add`, `Sub`, `Eq`, `Comparable`, which is exactly `Measurable`'s current bound, the resulting inequality lives in Presburger arithmetic: - Linear arithmetic over integers, no multiplication of two non-constant terms. - Presburger arithmetic is decidable (Presburger, 1929), even though the worst case is expensive (Fischer and Rabin proved a double-exponential lower bound in 1974). - This is also the fragment SMT-based verifiers lean on for their own `decreases` clauses (Dafny, F*, Lean's `omega`). -- Add `Mul` between two non-constant `Measurable` values, and this guarantee breaks. - General Diophantine reasoning, arithmetic with unrestricted multiplication, is undecidable. - This is Hilbert's tenth problem, resolved negatively by Matiyasevich in 1970, building on Davis, Putnam, and Robinson's earlier work. - There is no algorithm that decides, in general, whether an arbitrary polynomial equation over the integers has an integer solution, and the same wall shows up here. - -So `Measurable`'s existing trait bound, `Add, Sub, Eq, Comparable`, deliberately excluding `Mul`, is not arbitrary minimalism. -It is exactly the boundary that keeps "does this measure decrease" a decidable question. -Any future relaxation of `Measurable` needs to treat adding `Mul` as a real decidability boundary, not a convenience feature. - -One more requirement, easy to miss. -If `measure()` calls another pure function, the `Str` example in the README calls `.len()`, that function must also be non-recursive. -For the compiler's check to go through, it must be fully unfoldable into the same `Add`/`Sub`/`Eq`/`Comparable` fragment, or treated as an opaque, axiomatically trusted primitive, the way a compiler-provided `len()` can be. -This is a whole-program property, the transitive closure of everything `measure()` reaches, not just a property of `measure()`'s own body. -It is checkable the same way though: -Syntactically, at the definition site, with no evaluation required. - -**Conclusion.** `Measurable` does not need to stay closed to built-in types as a matter of correctness. -The correctness requirement is narrower, and already well understood in the literature above: -A total, deterministic, pure `measure()` into a well-founded, `Mul`-free arithmetic fragment, with every recursive call re-verified individually rather than trusted from the trait's existence. -Closing `Measurable` to built-in types only is a fine *simplicity* choice for an early version of the language. -It should not be sold as a *soundness* one. - -**Further reading**, on the pieces above: +It's the standard example of a total, computable function that is not primitive recursive: its recursion depth isn't bounded in advance by a single value that strictly decreases toward a base case, which is exactly the class `total` accepts. +A `for` loop over a `SizedIterator` is primitive recursive this way (its iteration count is fixed by the collection's size), and so is structural descent on a single `Measurable` value. + +- `A(m, n - 1)` decreases only `n`. +- `A(m - 1, A(m, n - 1))` decreases `m`, but its second argument is whatever the inner call returns, which can be far larger than the original `n`. + +Ackermann's termination is provable, just not by a flat measure. +Comparing `(m, n)` lexicographically, with `m` dominant, works: the outer call always decreases `m`, regardless of how large its second argument becomes. +`measure()` returns a single scalar, though, and `decreases` is a single comparison (`self.measure() < other.measure()`), so there's no way to fold a lexicographic pair into it. + +Other systems accept this shape directly: ACL2 by measuring into the ordinals below `ε₀`, and structural checkers built on the size-change principle (Lee, Jones, Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001), including Agda's, by tracking that some combination of argument positions decreases along every call path rather than one designated one. +Generalising `Measurable` from a flat scalar to a lexicographic tuple, an ordinal, or a multi-argument call-graph analysis is future work. + +## `Measurable` and custom types + +`Measurable` cannot currently be implemented for custom types. +Doing so safely needs two things: `measure()` must be total, deterministic, and pure, into a well-founded (bounded-below) codomain such as `PosInt`; and the compiler must re-verify the decrease at each call site rather than trusting a type's `Measurable` implementation on its own. +Given both, `measure()`'s specific logic doesn't matter for soundness, only that it's such a mapping. + +This is the same model Coq, Agda, Lean, and ACL2 already use for user-defined well-founded recursion: +Any type, any well-founded relation, with a fresh termination proof discharged at each use rather than trusted from a declaration. + +Re-verifying the decrease at every call site is only decidable because `Measurable` is restricted to `Add`, `Sub`, `Eq`, `Comparable` (Presburger arithmetic), which is decidable. +Adding `Mul` between two non-constant values would reintroduce undecidability, so any future relaxation of `Measurable` has to treat multiplication as a hard boundary, not a convenience. +A `measure()` that calls another pure function must also be non-recursive, so the whole call chain can be unfolded and checked at the definition site. + +Opening `Measurable` to custom types is future work. + +**Further reading:** - M. Presburger, *Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen*, 1929. - The original decidability result for linear integer arithmetic. -- M. J. Fischer, M. O. Rabin, *Super-Exponential Complexity of Presburger Arithmetic*, 1974. - The cost of that decidability, in the worst case. - Y. Matiyasevich, *Enumerable Sets are Diophantine*, 1970. - The negative resolution of Hilbert's tenth problem, why unrestricted multiplication breaks decidability. - C. S. Lee, N. D. Jones, A. M. Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001. - A decidable, fully automatic method for proving termination via call-graph decrease analysis, close in spirit to Mamba's own call-tree rule. - B. Nordström, *Terminating General Recursion*, BIT 28, 1988. - A. Bove, V. Capretta, *Modelling General Recursion in Type Theory*, Nordic Journal of Computing 12, 2005. - M. Kaufmann, P. Manolios, J S. Moore, *Computer-Aided Reasoning: An Approach*, 2000. - ACL2's ordinal-based `:measure` mechanism.