HigherOrderCO/Bend
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Bend.git synced 2024-10-05 15:57:08 +03:00
Code Issues Packages Projects Releases Wiki Activity

Fix more of the documentation

Browse Source
This commit is contained in:
Nicolas Abril 2024-05-20 19:10:36 +02:00
parent daa85e1bf6
commit 9302a5b26d
7 changed files with 135 additions and 133 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/compiler-options.md
View File

@ -17,7 +17,7 @@
Enables or disables Eta Reduction for defined functions.
Eta reduction simplifies lambda expressions, removing redundant parameters. [See also](https:#wiki.haskell.org/Eta_conversion).
Eta reduction simplifies lambda expressions, removing redundant parameters. [See also](https://wiki.haskell.org/Eta_conversion).
Example:
```py

18
docs/defining-data-types.md
View File

@ -2,27 +2,27 @@
It is possible to easily define complex data types using the `data` keyword.
```rs
// A Boolean is either True or False
```py
# A Boolean is either True or False
data Bool = True | False
```
If a constructor has any arguments, parentheses are necessary around it:
```rs
// An option either contains some value, or None
```py
# An option either contains some value, or None
data Option = (Some val) | None
```
If the data type has a single constructor, it can be destructured using `let`:
```rs
// A Box is a wrapper around a value.
```py
# A Box is a wrapper around a value.
data Boxed = (Box val)
let (Box value) = boxed; value
```
The fields of the constructor that is being destructured with the `match` are bound to the matched variable plus `.` and the field names.
```rs
```py
Option.map = λoption λf
match option {
Some: (Some (f option.val))
@ -33,14 +33,14 @@ Option.map = λoption λf
Rules can also have patterns.
They work like match expressions with explicit bindings:
```rs
```py
(Option.map (Some value) f) = (Some (f value))
(Option.map None f) = None
```
However, they also allow matching on multiple values at once, which is something that regular `match` can't do:
```rs
```py
data Boolean = True | False
(Option.is_both_some (Some lft_val) (Some rgt_val)) = True

72
docs/dups-and-sups.md
View File

@ -1,56 +1,60 @@
# Dups and sups
Term duplication is done automatically when a variable is used more than once. But it's possible to manually duplicate a term using `let`. This type of statement is called `dup` or `duplication`.
```rs
// the number 2 in church encoding using let.
```py
# the number 2 in church encoding using let.
ch2 = λf λx let {f1 f2} = f; (f1 (f2 x))
// the number 3 in church encoding using let.
# the number 3 in church encoding using let.
ch3 = λf λx let {f0 f1} = f; let {f2 f3} = f0; (f1 (f2 (f3 x)))
```
A `sup` is a superposition of two values, it is defined using curly brackets with two terms inside. A superposition is the opposite of a duplication.
```rs
A `sup` is a superposition of two values, it is defined using curly brackets with two terms inside. A superposition is the opposite of a duplication.
```py
sup = {3 7}
```
Sups can be used anywhere a value is expected, if anything interacts with the superposition, the result is the superposition of that interaction on both the possible values:
```rs
```py
mul = λa λb (* a b)
result = (mul 2 5) // returns 10
result_sup = (mul 2 {5 7}) // returns {10 14}
multi_sup = (mul {2 3} {5 7}) // returns {{10 14} {15 21}}
result = (mul 2 5) # returns 10
result_sup = (mul 2 {5 7}) # returns {10 14}
multi_sup = (mul {2 3} {5 7}) # returns {{10 14} {15 21}}
```
To access both values of a superposition, superpositions with labels are needed.
A `dup` generally just duplicates the term it points to:
If we pair a superposition with a duplication, the result is that they behave like constructing and destructing a pair:
```rs
// each dup variable now has a copy of the {1 2} superposition
```py
# each dup variable now has a copy of the {1 2} superposition
let {x1 x2} = {1 2}
```
Both `dups` and `sups` support labels, that is, a field starting with `#` to identify their counterpart. Unlabeled dups and sups are automatically assigned unique labels:
```rs
// here, x1 now contains the value of 1, and x2 the value of 2
let #i{x1 x2} = #i{1 2}
Due to how duplications are compiled, when two dups interact, they destructively interfere with each other.
In this case the result doesn't follow the expected behavior (it's well defined at the HVM level, but doesn't is incorrect at a lambda-calculus level).
That imposes a strong restriction on correct Bend programs: a variable should not duplicate another variable that itself duplicates some variables.
The program below is an example where this can go wrong when using higher-order functions.
```py
def List/map(xs, f):
fold xs:
case List/Nil:
return List/Nil
case List/Cons:
# 'f' is duplicated here
return List/Cons(f(xs.head), List/map(xs.tail, f))
# This line above is converted by the compiler to an explicit duplication of 'f'
# {f1 f2} = f
# return List/Cons(f1(xs.head), List/map(xs.tail, f2))
def main:
# This lambda duplicates `x` and is itself duplicated by the map function.
# This will result in wrong behavior.
# In this specific case, the runtime will catch it and generate an error,
# but at the moment that is not always the case.
return List/map([1, 2, 3], lambda x: (+ x x))
```
Due to how dups are compiled, dup tags between two interacting terms should not contain the same label. For example, an application of the church numeral 2 with itself won't reduce as expected:
```rs
c2 = λf λx let {f1 f2} = f; (f1 (f2 x))
main = (c2 c2)
```
To avoid label collision, HVM-Lang automatically generates new dup labels for each dup in the code. But with cases like the example above, when the interacting dups comes from the same place, the result is an invalid reduction.
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, 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))
main = (c2 c2_)
```
In this case, we can only have one source of duplication, or our results will be incorrect.
Either List/map is linear (doesn't duplicate `f`) or the passed function is linear (doesn't duplicate `x` or any other variable inside it).

12
docs/native-numbers.md
View File

@ -123,15 +123,15 @@ Number.minus_three = λn λf λx
Using everything we learned, we can write a program that calculates the n-th Fibonacci number using native numbers:
```rs
fibonacci = λn // n is the argument
```py
fibonacci = λn # n is the argument
switch n {
// If the number is 0, then return 0
# If the number is 0, then return 0
0: 0
// If the number is 1, then return 1
# If the number is 1, then return 1
1: 1
// Otherwise, return the sum of (fib (n-2 + 1)) and (fib n-2)
// The successor pattern provides a `var`-`successor number` bind
# Otherwise, return the sum of (fib (n-2 + 1)) and (fib n-2)
# The successor pattern provides a `var`-`successor number` bind
_: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
}

62
docs/pattern-matching.md
View File

@ -1,8 +1,8 @@
# Pattern Matching
Switches on many numbers are compiled to sequences of simple switch expressions:
```rust
// These two are equivalent
```py
# These two are equivalent
switch n {
0: A
1: B
@ -23,7 +23,7 @@ Switches on many numbers are compiled to sequences of simple switch expressions:
```
Matches on ADT constructors are compiled to different expressions depending on the chosen encoding:
```rust
```py
data Maybe = (Some val) | None
UnwrapOrZero x = match x {
@ -31,27 +31,25 @@ UnwrapOrZero x = match x {
None: 0
}
// If the current encoding is 'adt-tagged-scott' it becomes:
Some = λval #Maybe λSome #Maybe λNone #Maybe(Some val)
None = #Maybe λSome #Maybe λNone None
UnwrapOrZero x = #Maybe (x #Maybe λx.val x.val 0)
# If the current encoding is 'adt-num-scott' it becomes:
Some = λval λx (x 0 val)
None = λx (x 1)
UnwrapOrZero x = (x λtag switch tag {
0: λx.val x.val
_: λ* 0
})
// Otherwise, if the current encoding is 'adt-scott' it becomes:
# Otherwise, if the current encoding is 'adt-scott' it becomes:
Some = λval λSome λNone (Some val)
None = λSome λNone None
UnwrapOrZero x = (x λx.val x.val 0)
```
Currently, if you want to readback the adt constructors and matches after running a program as constructors and matches and not as lambda terms, you have to use `-Oadt-tagged-scott`.
The tags are used to decode which ADT the lambda term refers to, but having them means that if you want to write your own function to operate on these tagged structures your functions have to either use the `match` syntax or use the tags correctly themselves.
You can read more about tagged lambdas and applications in [Automatic vectorization with tagged lambdas](/doc/automatic-vectorization-with-tagged-lambdas.md).
### Pattern Matching functions
Besides `match`and `switch` terms, hvm-lang also supports equational-style pattern matching functions.
```rust
```py
And True b = b
And False * = False
```
@ -60,8 +58,8 @@ There are advantages and disadvantages to using this syntax.
They offer more advanced pattern matching capabilities and also take care linearizing variables to make sure that recursive definitions work correctly in strict evaluation mode, but take away your control of how the pattern matching is implemented and can be a bit more resource intensive in some cases.
Pattern matching equations are transformed into a tree of `match` and `switch` terms from left to right.
```rust
// These two are equivalent
```py
# These two are equivalent
(Foo 0 false (Cons h1 (Cons h2 t))) = (A h1 h2 t)
(Foo 0 * *) = B
(Foo n false *) = n
@ -87,21 +85,21 @@ Foo = λarg1 λarg2 λarg3 (switch arg1 {
Besides the compilation of complex pattern matching into simple `match` and `switch` expressions, this example also shows how some arguments are pushed inside the match.
When compiling for strict evaluation, by default any variables that are used inside a match get linearized by adding a lambda in each arm and an application passing its value inwards.
To ensure that recursive pattern matching functions don't loop in strict mode, it's necessary to make the match arms combinators, so that they can be converted into separate functions and a lazy reference is used in the match arm.
```rust
// This is what the Foo function actually compiles to.
// With -Olinearize-matches-extra and -Ofloat-combinators (default on strict mode)
```py
# This is what the Foo function actually compiles to.
# With -Olinearize-matches and -Ofloat-combinators (default on strict mode)
(Foo) = λa λb λc (switch a { 0: Foo$C5; _: Foo$C8 } b c)
(Foo$C5) = λd λe (d Foo$C0 Foo$C4 e) // Foo.case_0
(Foo$C0) = λ* B // Foo.case_0.case_true
(Foo$C4) = λg (g Foo$C3 B) // Foo.case_0.case_false
(Foo$C3) = λh λi (i Foo$C1 Foo$C2 h) // Foo.case_0.case_false.case_cons
(Foo$C1) = λj λk λl (A l j k) // Foo.case_0.case_false.case_cons.case_cons
(Foo$C2) = λ* B // Foo.case_0.case_false.case_cons.case_nil
(Foo$C5) = λd λe (d Foo$C0 Foo$C4 e) # Foo.case_0
(Foo$C0) = λ* B # Foo.case_0.case_true
(Foo$C4) = λg (g Foo$C3 B) # Foo.case_0.case_false
(Foo$C3) = λh λi (i Foo$C1 Foo$C2 h) # Foo.case_0.case_false.case_cons
(Foo$C1) = λj λk λl (A l j k) # Foo.case_0.case_false.case_cons.case_cons
(Foo$C2) = λ* B # Foo.case_0.case_false.case_cons.case_nil
(Foo$C8) = λn λo λ* (o Foo$C6 Foo$C7 n) // Foo.case_+
(Foo$C6) = λ* 0 // Foo.case_+.case_true
(Foo$C7) = λr (+ r 1) // Foo.case_+.case_false
(Foo$C8) = λn λo λ* (o Foo$C6 Foo$C7 n) # Foo.case_+
(Foo$C6) = λ* 0 # Foo.case_+.case_true
(Foo$C7) = λr (+ r 1) # Foo.case_+.case_false
```
Pattern matching equations also support matching on non-consecutive numbers:
@ -112,10 +110,10 @@ Parse 'λ' = Token.Lambda
Parse n = (Token.Name n)
```
This is compiled to a cascade of `switch` expressions, from smallest value to largest.
```rust
```py
Parse = λarg0 switch matched = (- arg0 '(') {
0: Token.LParenthesis
// ')' + 1 - '(' is resolved during compile time
# ')' + 1 - '(' is resolved during compile time
_: switch matched = (- matched-1 ( ')'-1-'(' ) {
0: Token.RParenthesis
_: switch matched = (- matched-1 ( 'λ'-1-')' ) {
@ -138,7 +136,7 @@ pred_if True 0 * = 0
Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List/String.nil
```rust
```py
Hi "hi" = 1
Hi _ = 0
@ -146,7 +144,7 @@ Foo [] = 0
Foo [x] = x
Foo _ = 3
// Becomes:
# Becomes:
Hi (String.cons 'h' (String.cons 'i' String.nil)) = 2
Hi _ = 0

36
docs/using-scopeless-lambdas.md
View File

@ -4,22 +4,22 @@ Scopeless lambdas are very powerful lambdas that are a side-effect of HVM's inte
Scopeless lambdas are lambdas that have no scope. The variables bound by them can be used outside the lambda's body. They can be created by prefixing a dollar symbol (`$`) to a lambda's variable name.
```rs
λ$x $x // The identity function as a scopeless lambda
```py
λ$x $x # The identity function as a scopeless lambda
```
Of course, using scopeless lambdas as a replacement for regular lambdas is kind of pointless. Their real power comes from being able to use the bound variable outside the body:
```rs
```py
main = (((λ$x 1) 2), $x)
// $x gets replaced by 2 and the application ((λ$x 1) 2) gets replaced by 1
// Outputs (1, 2)
# $x gets replaced by 2 and the application ((λ$x 1) 2) gets replaced by 1
# Outputs (1, 2)
```
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.
```rs
```py
def = $x
main = (((λ$x 1) 2), def)
@ -31,12 +31,12 @@ The bound variables are local to each term.
We have seen that the variable bound to a scopeless lambda gets set when the lambda is called. But, what happens if we never call `λ$x 1`? What will `$x` get set to then? Here is a program that does that:
```rs
main = // TODO bug in hvm-lang
let _ = λ$x 1 // Discard and erase the scopeless lambda
```py
main =
let _ = λ$x 1 # Discard and erase the scopeless lambda
(2, $x)
// Outputs (2, *)
# Outputs (2, *)
```
The program outputs `2` as the first item of the tuple, as expected. But the second item is `*`! What is `*`?
@ -47,12 +47,12 @@ What happens if we call `λ$x 1` with two different values instead?
Try to answer this with your knowledge of HVM. Will it throw a runtime error? Will it return something unexpected?
```rs
```py
main =
let f = λ$x 1 // Assign the lambda to a variable
((f 2), ((f 3), $x)) // Return a tuple of (f 2) and another tuple.
let f = λ$x 1 # Assign the lambda to a variable
((f 2), ((f 3), $x)) # Return a tuple of (f 2) and another tuple.
// Outputs (1, (1, {#0 3 2}))
# Outputs (1, (1, {#0 3 2}))
```
What? This is even more confusing. The first two values are `1`, as expected. But what about the last term?
@ -65,18 +65,18 @@ Now that we know how scopeless lambdas work, we can make programs using them. An
Call/cc is a function that takes a function that takes a parameter `k`. When `k` is called with an argument, `callcc` returns it.
```rs
// Function that discards its second argument
```py
# Function that discards its second argument
Seq a b = a
// Create a program capable of using `callcc`
# Create a program capable of using `callcc`
CC.lang = λprogram
let callcc = λcallback (λ$garbage($hole) (callback λ$hole(0)));
let result = (program callcc);
(Seq result $garbage)
Main = (CC.lang λcallcc
// This code calls `callcc`, then calls `k` to fill the hole with `42`. This means that the call to callcc returns `42`, and the program returns `52`. (+ (k 42) 1729) is garbage and is erased.
# This code calls `callcc`, then calls `k` to fill the hole with `42`. This means that the call to callcc returns `42`, and the program returns `52`. (+ (k 42) 1729) is garbage and is erased.
(+ 10 (callcc λk(+ (k 42) 1729)))
)
```

66
docs/writing-fusing-functions.md
View File

@ -1,44 +1,44 @@
# Writing fusing functions
## Church encoding
Church Encoding is a way to encode common datatypes as λ-calculus terms. For example, here is a [Church-encoded](https://en.wikipedia.org/wiki/Church_encoding) boolean type in HVM
```rs
```py
true = λt λf t
false = λt λf f
```
Matching on values of this representation is simply calling the boolean value with what the function should return if the boolean is true and if the boolean is false.
```rs
```py
if boolean case_true case_false = (boolean case_true case_false)
main = (if true 42 37)
// Outputs 42
# Outputs 42
// Or alternatively:
// if boolean = boolean
// Each boolean is represented by its own matching function
// so (true 42 37) will do the same thing.
# Or alternatively:
# if boolean = boolean
# Each boolean is represented by its own matching function
# so (true 42 37) will do the same thing.
```
This is how a `Not` function that acts on this encoding can be defined:
```rs
```py
not = λboolean (boolean false true)
main = (not true) // Outputs λtλf f.
main = (not false) // Outputs λtλf t.
main = (not true) # Outputs λtλf f.
main = (not false) # Outputs λtλf t.
```
If the boolean is `true`, then the function will return `false`. If it is `false`, it will return `true`.
## Self-application
What happens if we self-compose the `not` function? It is a well known fact that`(not (not x)) == x`, so we should expect something that behaves like the identity function.
```rs
```py
main = λx (not (not x))
// Output:
// λa (a λ* λb b λc λ* c λ* λd d λe λ* e)
# Output:
# λa (a λ* λb b λc λ* c λ* λd d λe λ* e)
```
The self-application of `not` outputs a large term. Testing will show that the term does indeed behave like an identity function. However, since the self-application of `not` is larger than `not` itself, if we self-compose this function many times, our program will get really slow and eat up a lot of memory, despite all functions being equivalent to the identity function:
```rs
main = λx (not (not x)) // Long
main = λx (not (not (not (not x)))) // Longer
main = λx (not (not (not (not (not (not (not (not x)))))))) // Longer
// etc...
```py
main = λx (not (not x)) # Long
main = λx (not (not (not (not x)))) # Longer
main = λx (not (not (not (not (not (not (not (not x)))))))) # Longer
# etc...
```
The self-application of not a large number of times, such as 65536 or 4294967296, will be large enough to slow down our computer by a significant amount.
@ -46,19 +46,19 @@ Luckily, there's a trick we can do to make the self-application of `not` much sh
### Fusing functions
Let's first take our initial `not` implementation.
```rs
```py
not = λboolean (boolean false true)
```
We begin by replacing `false` and `true` by their values.
```rs
```py
not = λboolean (boolean λtλf(f) λtλf(t))
```
After doing this, it's easy to notice that there's something that both terms have in common. Both of them are lambdas that take in two arguments. We can **lift** the lambda arguments up and make them **shared** between both cases.
```rs
not = λbooleanλtλf (boolean f t)
```py
not = λboolean λt λf (boolean f t)
```
Let's see how the self-application of `not` gets reduced now. Each line will be a step in the reduction.
```rs
```py
main = λx (not (not x))
main = λx (not (λbooleanλtλf (boolean f t) x))
main = λx (not (λtλf (boolean x f t)))
@ -77,19 +77,19 @@ Something else that is important when writing fusing functions is linearizing va
Consider the [scott-encoded](https://crypto.stanford.edu/~blynn/compiler/scott.html) type `Nat`:
```rs
zero = λs λz z // 0 as a scott-encoded number
succ = λpred λs λz (s pred) // Creates a Scott number out of its predecessor
```py
zero = λs λz z # 0 as a scott-encoded number
succ = λpred λs λz (s pred) # Creates a Scott number out of its predecessor
two = (succ (succ zero)) // λs λz (s λs λz (s λs λz z))
two = (succ (succ zero)) # λs λz (s λs λz (s λs λz z))
```
We can write an addition function for this type, that adds two numbers
```rs
```py
add = λa λb
let case_succ = λa_pred (succ (add a_pred b)) // If a = p+1, then return (p+b)+1
let case_zero = b // If the `a = 0`, return `b`
let case_succ = λa_pred (succ (add a_pred b)) # If a = p+1, then return (p+b)+1
let case_zero = b # If the `a = 0`, return `b`
(a case_succ case_zero)
```
@ -124,7 +124,7 @@ To show the power of fusing, here is a program that self-composes `fusing_not` 2
Currently hvm is not able to handle operations between church numbers so we explicitly convert the native number to a church number in this example (which is very slow).
This program uses [native numbers, which are described here](native-numbers.md).
```rs
```py
true = λt λf t
false = λt λf f
@ -132,14 +132,14 @@ not = λboolean (boolean false true)
fusing_not = λboolean λt λf (boolean f t)
// Creates a Church numeral out of a native number
# Creates a Church numeral out of a native number
to_church n = switch n {
0: λf λx x
_: λf λx (f (to_church n-1 f x))
}
main =
((to_church 0xFFFFFF) fusing_not) // try replacing this by regular not. Will it still work?
((to_church 0xFFFFFF) fusing_not) # try replacing this by regular not. Will it still work?
```
Here is the program's output:
```bash