Skip to content

Commit

Permalink
Update recursion error message and update docs
Browse files Browse the repository at this point in the history
  • Loading branch information
imaqtkatt committed Mar 22, 2024
1 parent f97b7c1 commit ad4f1bb
Show file tree
Hide file tree
Showing 7 changed files with 50 additions and 37 deletions.
6 changes: 4 additions & 2 deletions docs/lazy-definitions.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
# Making recursive definitions lazy

In strict-mode, terms that use recursive terms will unroll indefinitely.
In strict-mode, some types of recursive terms will unroll indefinitely.

This is a simple piece of code that works on many other functional programming languages, but hangs on HVM:
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:

```rust
Cons = λx λxs λcons λnil (cons x xs)
Expand Down Expand Up @@ -55,6 +55,8 @@ This code will work as expected, since `cons` and `nil` are lambdas without free

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

HVM-lang carries out [match linearization](compiler-options#linearize-matches) and [combinator floating](compiler-options#float-combinators) optimizations, enabled through the CLI, which are active by default in strict mode.
Expand Down
9 changes: 5 additions & 4 deletions src/hvmc_net/mutual_recursion.message
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
Seems like you're trying to run some recursive function(s) on strict-mode:
{refs}
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.
Expand All @@ -14,9 +15,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)))
(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))
(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.
24 changes: 18 additions & 6 deletions src/hvmc_net/mutual_recursion.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use crate::diagnostics::{Diagnostics, WarningType};
use crate::diagnostics::{Diagnostics, WarningType, ERR_INDENT_SIZE};
use hvmc::ast::{Book, Tree};
use indexmap::{IndexMap, IndexSet};
use std::fmt::Debug;
Expand All @@ -17,18 +17,30 @@ pub fn check_cycles(book: &Book, diagnostics: &mut Diagnostics) -> Result<(), Di
let cycles = graph.cycles();

if !cycles.is_empty() {
let msg = format!(include_str!("mutual_recursion.message"), refs = show_refs(&cycles));
let msg = format!(include_str!("mutual_recursion.message"), cycles = show_cycles(&cycles));
diagnostics.add_book_warning(msg.as_str(), WarningType::MutualRecursionCycle);
}

diagnostics.fatal(())
}

fn show_refs(cycles: &[Vec<Ref>]) -> String {
use itertools::Itertools;
fn show_cycles(cycles: &[Vec<Ref>]) -> String {
let tail = &format!("\n{:ERR_INDENT_SIZE$}* ...", "");
let tail = if cycles.len() > 5 { tail } else { "" };

let cycles = cycles.concat();
cycles.iter().take(5).join("\n") + if cycles.len() > 5 { "\n..." } else { "" }
let mut cycles = cycles
.iter()
.take(5)
.map(|cycle| {
let cycle_str = cycle.iter().chain(cycle.first()).cloned().collect::<Vec<_>>().join(" -> ");
format!("{:ERR_INDENT_SIZE$}* {}", "", cycle_str)
})
.collect::<Vec<String>>()
.join("\n");

cycles.push_str(tail);

cycles
}

impl Graph {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/repeated_name_trucation.hvm
---
Warnings:
Seems like you're trying to run some recursive function(s) on strict-mode:
long_name_that_truncates
long_name_that_truncates$C0
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$C0 -> 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.
Expand All @@ -20,10 +20,10 @@ 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)))
(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))
(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.

Expand Down
11 changes: 5 additions & 6 deletions tests/snapshots/mutual_recursion__a_b_c.hvm.snap
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,9 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/mutual_recursion/a_b_c.hvm
---
Errors:
Seems like you're trying to run some recursive function(s) on strict-mode:
A
B
C
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.
Expand All @@ -21,9 +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)))
(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))
(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.
17 changes: 8 additions & 9 deletions tests/snapshots/mutual_recursion__multiple.hvm.snap
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,12 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/mutual_recursion/multiple.hvm
---
Errors:
Seems like you're trying to run some recursive function(s) on strict-mode:
A
B
C
H
I
...
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.
Expand All @@ -24,9 +23,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)))
(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))
(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.
10 changes: 5 additions & 5 deletions tests/snapshots/mutual_recursion__odd_even.hvm.snap
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/mutual_recursion/odd_even.hvm
---
Errors:
Seems like you're trying to run some recursive function(s) on strict-mode:
isEven
isOdd
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.
Expand All @@ -20,9 +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)))
(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))
(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.

0 comments on commit ad4f1bb

Please sign in to comment.