From f97b7c13792d863a0e14cac5a86c5be7689c45b9 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Fri, 22 Mar 2024 09:35:44 -0300
Subject: [PATCH] Update recursion error message and update docs

---
 docs/lazy-definitions.md                      | 65 ++++++++++++-------
 src/hvmc_net/mutual_recursion.message         |  4 ++
 ...le_o_all__repeated_name_trucation.hvm.snap |  4 ++
 .../mutual_recursion__a_b_c.hvm.snap          |  4 ++
 .../mutual_recursion__multiple.hvm.snap       |  4 ++
 .../mutual_recursion__odd_even.hvm.snap       |  4 ++
 6 files changed, 61 insertions(+), 24 deletions(-)

diff --git a/docs/lazy-definitions.md b/docs/lazy-definitions.md
index e9af3aeab..8ebeec66b 100644
--- a/docs/lazy-definitions.md
+++ b/docs/lazy-definitions.md
@@ -1,42 +1,59 @@
 # 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, terms that use 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, but hangs on HVM:
 
-```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)
 
-Nat.add = (Y λaddλaλb match a {
-	Z: b
-	(S p): (S (add p b))
-})
+Main = (Map λx (+ x 1) (Cons 1 Nil))
+```
 
-main = (Nat.add (S (S (S Z))) (S Z))
+The recursive `Map` definition never gets reduced.
+Using the debug mode `-d` we can see the steps:
+
+```
+(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.
 
 ### Automatic optimization
 
diff --git a/src/hvmc_net/mutual_recursion.message b/src/hvmc_net/mutual_recursion.message
index e4b62c935..ff037e39a 100644
--- a/src/hvmc_net/mutual_recursion.message
+++ b/src/hvmc_net/mutual_recursion.message
@@ -14,5 +14,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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.
diff --git a/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap b/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
index 252c45ea1..7f7eaeef0 100644
--- a/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
@@ -20,7 +20,11 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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.
 
 
diff --git a/tests/snapshots/mutual_recursion__a_b_c.hvm.snap b/tests/snapshots/mutual_recursion__a_b_c.hvm.snap
index 406fe9519..7428ca953 100644
--- a/tests/snapshots/mutual_recursion__a_b_c.hvm.snap
+++ b/tests/snapshots/mutual_recursion__a_b_c.hvm.snap
@@ -21,5 +21,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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.
diff --git a/tests/snapshots/mutual_recursion__multiple.hvm.snap b/tests/snapshots/mutual_recursion__multiple.hvm.snap
index 8f48533aa..e0cd9fa98 100644
--- a/tests/snapshots/mutual_recursion__multiple.hvm.snap
+++ b/tests/snapshots/mutual_recursion__multiple.hvm.snap
@@ -24,5 +24,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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.
diff --git a/tests/snapshots/mutual_recursion__odd_even.hvm.snap b/tests/snapshots/mutual_recursion__odd_even.hvm.snap
index ba0b2bce4..d3eb08a3a 100644
--- a/tests/snapshots/mutual_recursion__odd_even.hvm.snap
+++ b/tests/snapshots/mutual_recursion__odd_even.hvm.snap
@@ -20,5 +20,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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.