Doc: Expand total function docs

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,33 @@ 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.
+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
+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))
+end
+```
+
+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:
 
@@ -435,20 +463,23 @@ 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.
-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.
+
+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.
@@ -484,27 +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:
+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.
 
-- 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.
+A meta function:
 
-Additionally:
+- 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.
 
-- 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...).
-- We may well place additional constraints on meta functions in future.
+`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(<args>) := ...`.
 - A meta variable is defined `def meta my_var: MyType := ...`, with type annotations being non-optional.

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)

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.

docs/features/functions/meta_functions.md

@@ -0,0 +1,18 @@
+⬅ [🏠 Home](../../README.md)
+
+⬅ [2 🛠 Features](../README.md)
+
+⬅ [2.5 🔁 Functions](README.md)
+
+# 2.5.3 Meta Functions
+
+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.
+
+`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.
+
+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.

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.

docs/features/functions/total_functions.md

@@ -0,0 +1,64 @@
+⬅ [🏠 Home](../../README.md)
+
+⬅ [2 🛠 Features](../README.md)
+
+⬅ [2.5 🔁 Functions](README.md)
+
+# 2.5.2 Total Functions
+
+## Ackermann's function
+
+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
+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))
+end
+```
+
+```
+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'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.
+- Y. Matiyasevich, *Enumerable Sets are Diophantine*, 1970.
+- C. S. Lee, N. D. Jones, A. M. Ben-Amram, *The Size-Change Principle for Program Termination*, POPL 2001.
+- 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.

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<bool> {
         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<bool> {
         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(())