Merge pull request #242 from HigherOrderCO/feature/sc-526/improve-der…

…ef-loop-warning-in-strict-evaluation

[sc-526] Improve deref loop warning in strict evaluation

docs/lazy-definitions.md

@@ -1,42 +1,61 @@
 # Making recursive definitions lazy
 
-The HVM-Core is an eager runtime, for both CPU and parallel GPU implementations. Terms that use recursive terms will unroll indefinitely.
+In strict-mode, some types of recursive terms will unroll indefinitely.
 
-This means that for example, the following code will hang, despite being technically correct and working on Haskell:
+This is a simple piece of code that works on many other functional programming languages, including hvm's lazy-mode, but hangs on strict-mode:
 
-```rs
-data Nat = Z | (S p)
+```rust
+Cons = λx λxs λcons λnil (cons x xs)
+Nil  =        λcons λnil nil
 
-Y = λf (λx (f (x x)) λx (f (x x)))
+Map = λf λlist
+  let cons = λx λxs (Cons (f x) (Map f xs))
+  let nil = Nil
+  (list cons nil)
+
+Main = (Map λx (+ x 1) (Cons 1 Nil))
+```
 
-Nat.add = (Y λaddλaλb match a {
-	Z: b
-	(S p): (S (add p b))
-})
+The recursive `Map` definition never gets reduced.
+Using the debug mode `-d` we can see the steps:
 
-main = (Nat.add (S (S (S Z))) (S Z))
+```
+(Map λa (+ a 1) (Cons 1 Nil))
+---------------------------------------
+(Map λa (+ a 1) λb λ* (b 1 Nil))
+---------------------------------------
+(Cons (λa (+ a 1) 1) (Map λa (+ a 1) Nil))
+---------------------------------------
+(Cons (λa (+ a 1) 1) (Nil λb λc (Cons (λa (+ a 1) b) (Map λa (+ a 1) c)) Nil))
+---------------------------------------
+...
 ```
 
-Because of that, its recommended to use a [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
+For similar reasons, if we try using Y combinator it also won't work.
 
-The `Nat.add` definition below can be a supercombinator if linearized.
+```rust
+Y = λf (λx (f (x x)) λx (f (x x)))
 
-```rs
-Nat.add = λaλb match a {
-	Z: b
-	(S p): (S (Nat.add p b))
-}
+Map = (Y λrec λf λlist
+  let cons = λx λxs (Cons (f x) (rec f xs))
+  let nil = Nil
+  (list cons nil f))
 ```
 
-```rs
-// Linearized Nat.add
-Nat.add = λa match a {
-	Z: λb b
-	(S p): λb (S (Nat.add p b))
-}
+By linearizing `f`, the `Map` function "fully reduces" first and then applies `f`.
+
+```rust
+Map = λf λlist
+  let cons = λx λxs λf (Cons (f x) (Map f xs))
+  let nil = λf Nil
+  (list cons nil f)
 ```
 
-This code will work as expected, because `Nat.add` is unrolled lazily only when it is used as an argument to a lambda.
+This code will work as expected, since `cons` and `nil` are lambdas without free variables, they will be automatically floated to new definitions if the [float-combinators](compiler-options#float-combinators) option is active, allowing them to be unrolled lazily by hvm.
+
+It's recommended to use a [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
+
+If you have a set of mutually recursive functions, you only need to make one of the steps lazy. This might be useful when doing micro-optimizations, since it's possible to avoid part of the small performance cost of linearizing lambdas.
 
 ### Automatic optimization
 

src/hvmc_net/mutual_recursion.message

@@ -0,0 +1,23 @@
+Seems like you're trying to run some recursive function(s) on strict-mode.
+The following recursive cycles are not compatible with strict-mode the way these functions were written:
+{cycles}
+
+Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
+If the float-combinators optimization is not on, we recommend activating it.
+
+You have 2 options:
+
+1. Easy Fix: use lazy-mode.
+
+Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
+
+2. Hard Fix: refactor the program to use lazy references.
+
+When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
+If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
+(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
+
+For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+
+See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

src/hvmc_net/mutual_recursion.rs

@@ -17,32 +17,36 @@ pub fn check_cycles(book: &Book, diagnostics: &mut Diagnostics) -> Result<(), Di
   let cycles = graph.cycles();
 
   if !cycles.is_empty() {
-    let msg = format!(
-      "{}\n{}\n{:ERR_INDENT_SIZE$}{}\n{:ERR_INDENT_SIZE$}{}",
-      "Mutual recursion cycle detected in compiled functions:",
-      pretty_print_cycles(&cycles),
-      "",
-      "This program will expand infinitely in strict evaluation mode.",
-      "",
-      "Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information."
-    );
-
+    let msg = format!(include_str!("mutual_recursion.message"), cycles = show_cycles(&cycles));
     diagnostics.add_book_warning(msg.as_str(), WarningType::MutualRecursionCycle);
   }
 
   diagnostics.fatal(())
 }
 
-fn pretty_print_cycles(cycles: &[Vec<Ref>]) -> String {
-  cycles
+fn show_cycles(cycles: &[Vec<Ref>]) -> String {
+  let tail = &format!("\n{:ERR_INDENT_SIZE$}* ...", "");
+  let tail = if cycles.len() > 5 { tail } else { "" };
+
+  let mut cycles = cycles
     .iter()
-    .enumerate()
-    .map(|(i, cycle)| {
-      let cycle_str = cycle.iter().chain(cycle.first()).cloned().collect::<Vec<_>>().join(" -> ");
-      format!("{:ERR_INDENT_SIZE$}Cycle {}: {}", "", 1 + i, cycle_str)
+    .take(5)
+    .map(|cycle| {
+      let cycle_str = cycle
+        .iter()
+        .filter(|nam| !nam.contains("$C"))
+        .chain(cycle.first())
+        .cloned()
+        .collect::<Vec<_>>()
+        .join(" -> ");
+      format!("{:ERR_INDENT_SIZE$}* {}", "", cycle_str)
     })
     .collect::<Vec<String>>()
-    .join("\n")
+    .join("\n");
+
+  cycles.push_str(tail);
+
+  cycles
 }
 
 impl Graph {

tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap

@@ -3,10 +3,30 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/repeated_name_trucation.hvm
 ---
 Warnings:
-Mutual recursion cycle detected in compiled functions:
-  Cycle 1: long_name_that_truncates -> long_name_that_truncates$C0 -> long_name_that_truncates
-  This program will expand infinitely in strict evaluation mode.
-  Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.
+Seems like you're trying to run some recursive function(s) on strict-mode.
+The following recursive cycles are not compatible with strict-mode the way these functions were written:
+  * long_name_that_truncates -> long_name_that_truncates
+
+Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
+If the float-combinators optimization is not on, we recommend activating it.
+
+You have 2 options:
+
+1. Easy Fix: use lazy-mode.
+
+Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
+
+2. Hard Fix: refactor the program to use lazy references.
+
+When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
+If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
+(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
+
+For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+
+See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
+
 
 @long_name_that_truncates = (* @long_name_that_truncates$C0)
 

tests/snapshots/mutual_recursion__a_b_c.hvm.snap

@@ -3,7 +3,26 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/a_b_c.hvm
 ---
 Errors:
-Mutual recursion cycle detected in compiled functions:
-  Cycle 1: A -> B -> C -> A
-  This program will expand infinitely in strict evaluation mode.
-  Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.
+Seems like you're trying to run some recursive function(s) on strict-mode.
+The following recursive cycles are not compatible with strict-mode the way these functions were written:
+  * A -> B -> C -> A
+
+Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
+If the float-combinators optimization is not on, we recommend activating it.
+
+You have 2 options:
+
+1. Easy Fix: use lazy-mode.
+
+Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
+
+2. Hard Fix: refactor the program to use lazy references.
+
+When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
+If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
+(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
+
+For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+
+See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

tests/snapshots/mutual_recursion__multiple.hvm.snap

@@ -3,10 +3,29 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/multiple.hvm
 ---
 Errors:
-Mutual recursion cycle detected in compiled functions:
-  Cycle 1: A -> B -> C -> A
-  Cycle 2: H -> I -> H
-  Cycle 3: M -> M
-  Cycle 4: N -> N
-  This program will expand infinitely in strict evaluation mode.
-  Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.
+Seems like you're trying to run some recursive function(s) on strict-mode.
+The following recursive cycles are not compatible with strict-mode the way these functions were written:
+  * A -> B -> C -> A
+  * H -> I -> H
+  * M -> M
+  * N -> N
+
+Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
+If the float-combinators optimization is not on, we recommend activating it.
+
+You have 2 options:
+
+1. Easy Fix: use lazy-mode.
+
+Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
+
+2. Hard Fix: refactor the program to use lazy references.
+
+When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
+If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
+(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
+
+For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+
+See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

tests/snapshots/mutual_recursion__odd_even.hvm.snap

@@ -3,7 +3,26 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/odd_even.hvm
 ---
 Errors:
-Mutual recursion cycle detected in compiled functions:
-  Cycle 1: isEven -> isOdd -> isEven
-  This program will expand infinitely in strict evaluation mode.
-  Read https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md for more information.
+Seems like you're trying to run some recursive function(s) on strict-mode.
+The following recursive cycles are not compatible with strict-mode the way these functions were written:
+  * isEven -> isOdd -> isEven
+
+Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
+If the float-combinators optimization is not on, we recommend activating it.
+
+You have 2 options:
+
+1. Easy Fix: use lazy-mode.
+
+Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
+
+2. Hard Fix: refactor the program to use lazy references.
+
+When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
+If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
+(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
+
+For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+
+See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.