documentation edits

This commit is contained in:
Jason Fong 2024-05-18 23:34:20 -04:00
parent 8fda78f1e6
commit 276dcc6280
6 changed files with 8 additions and 8 deletions

View File

@ -8,7 +8,7 @@ bend run <Path to program> [Arguments in expression form]...
It accepts any expression that would also be valid inside a bend function.
Arguments are passed to programs by applying them to the entrypoint function:
Arguments are passed to programs by applying them to the entry point function:
```py
# Imp syntax

View File

@ -114,7 +114,7 @@ Example:
λa λb switch b { 0: a; _: a }
```
When the `linearize-matches-extra` option is used, it linearizes all vars used in the arms.
When the `linearize-matches-extra` option is used, it linearizes all variables used in the arms.
example:
```py
@ -160,7 +160,7 @@ fold = λinit λf λxs (xs λh λt (fold (f init h) f t) init)
# Inline
If enabled, inlines terms that compiles to 0 or 1 inet nodes at lambda level, before pre reduction.
If enabled, inlines terms that compile to 0 or 1 inet nodes at lambda level, before pre-reduction.
Example:
```py

View File

@ -48,7 +48,7 @@ To avoid label collision, HVM-Lang automatically generates new dup labels for ea
This is not *incorrect* behavior or *undefined* behaviour. It is incorrect only if we treat HVM as a λ-calculus reduction engine, which isn't true. However, there are some cases where HVM diverges from λ-calculus, and this is one of them.
To fix the problem, its necessary to re-create the term so that a new label is assigned, or manually assign one:
To fix the problem, it's necessary to re-create the term so that a new label is assigned, or manually assign one:
```rs
c2 = λf λx let {f1 f2} = f; (f1 (f2 x))
c2_ = λf λx let #label {f1 f2} = f; (f1 (f2 x))

View File

@ -53,7 +53,7 @@ minus_zero = -0.0
### Mixing number types
The three number types are fundamentally different.
If you mix two numbers of different types HVM will interpret the binary representation of one of them incorrectly, leading to incorrect results. Which number is interpreted incorrectly depends on the situation and shouldn't be relied on for now.
If you mix two numbers of different types, HVM will interpret the binary representation of one of them incorrectly, leading to incorrect results. Which number is interpreted incorrectly depends on the situation and shouldn't be relied on for now.
At the HVM level, both type and the operation are stored inside the number nodes as tags. One number stores the type, the other the operation.
That means that we lose the type information of one of the numbers, which causes this behavior.

View File

@ -18,7 +18,7 @@ main = (((λ$x 1) 2), $x)
Take some time to think about the program above. It is valid, despite `$x` being used outside the lambda's body.
However, scopeless lambdas don't bind across definitions
However, scopeless lambdas don't bind across definitions.
```rs
def = $x

View File

@ -17,7 +17,7 @@ main = (if true 42 37)
// so (true 42 37) will do the same thing.
```
This is how a `Not` function that acts on this encoding can be defined
This is how a `Not` function that acts on this encoding can be defined.
```rs
not = λboolean (boolean false true)
main = (not true) // Outputs λtλf f.
@ -114,7 +114,7 @@ fusing_add = λa
(a case_succ case_zero)
```
This function is fusing on `a`, which means that `λx (fusing_add two x)` will have a small normal form (but `λx (fusing_add x two)` won't)
This function is fusing on `a`, which means that `λx (fusing_add two x)` will have a small normal form (but `λx (fusing_add x two)` won't).
Broadly speaking, a good rule of thumb in HVM is **push linear lambdas to the top and duplicating lambdas to the bottom**.