diff options
24 files changed, 548 insertions, 405 deletions
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index 9b557ca..1b7fd60 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -15,12 +15,11 @@ nav: - Index: index.md - Introduction: - introduction/installation.md - - introduction/lambda-calculus.md - introduction/setup.md + - introduction/lambda-calculus.md - introduction/syntax.md - Coding: - coding/REPL.md - - TDD: coding/test-driven-development.md - coding/mixfix.md - coding/prefix.md - coding/recursion.md @@ -32,13 +31,12 @@ nav: - coding/meta-programming.md - UFCS: coding/uniform-function-call-syntax.md - coding/style.md - - coding/typing.md + - TDD: coding/test-driven-development.md - coding/compilation.md - - coding/performance.md - - coding/examples.md - Technical: - - technical/arithmetic.md + - technical/performance.md - technical/reduction.md + - Examples: coding/examples.md - Landing page: https://bruijn.marvinborner.de - GitHub: https://github.com/marvinborner/bruijn diff --git a/docs/wiki_src/coding/IO.md b/docs/wiki_src/coding/IO.md index 974f98e..c1abc8a 100644 --- a/docs/wiki_src/coding/IO.md +++ b/docs/wiki_src/coding/IO.md @@ -11,6 +11,12 @@ You can use [`std/Monad`](/std/Monad.bruijn.html) to interact with the input monadically, or simply use [`std/List`](/std/List.bruijn.html) operations to work with the input as a normal list. +See [data structures](data-structures.md) to learn more about lists and +numbers. + +If you want your main function to ignore the input, just add an +additional (unbound) abstraction to your definition. + ## Example ``` bruijn diff --git a/docs/wiki_src/coding/REPL.md b/docs/wiki_src/coding/REPL.md index a801ef9..e3ec1a7 100644 --- a/docs/wiki_src/coding/REPL.md +++ b/docs/wiki_src/coding/REPL.md @@ -1,6 +1,6 @@ # REPL -The REPL is a very helpful feature for functional programming languages +The REPL is a very helpful tool for functional programming languages like bruijn. You can use it to continuously test or execute parts of your code. @@ -8,6 +8,8 @@ You can start the REPL using `stack run`{.bash} or (if installed) `bruijn`{.bash}. Any valid term will get reduced to normal form after pressing enter. +Common [data structures](data-structures.md) will get resolved in a +seperate line if detected (e.g. numbers, lists or strings). ## Definitions @@ -82,9 +84,9 @@ unreduced and the reduced expression. Helpful for golfed [compilation](compilation.md). ``` bruijn -> :blc [0] [0] -0100100010 -0010 +> :length [0] [0] +10 +4 ``` ### `:free`{.bruijn} diff --git a/docs/wiki_src/coding/combinators.md b/docs/wiki_src/coding/combinators.md index e69de29..b85b7fa 100644 --- a/docs/wiki_src/coding/combinators.md +++ b/docs/wiki_src/coding/combinators.md @@ -0,0 +1,74 @@ +# Combinators + +Combinators are short *closed* terms that can be combined with other +terms or combinators. + +## Common + +All of these combinators (and many more) can be found in +[`std/Combinator`](/std/Combinator.bruijn.html). The names are taken +from Raymond Smullyan's book "To Mock a Mockingbird"[^1]. + +`y`{.bruijn}/`z`{.bruijn}: *Fixed-point* combinators + +: used to achieve [recursion](recursion.md) + +: `(y g)`{.bruijn} = `(g (y g))`{.bruijn} + +`b`{.bruijn}/`b'`{.bruijn}/`b'''`{.bruijn} or `…∘…`{.bruijn}/`…∘∘…`{.bruijn}/`…∘∘∘…`{.bruijn}: *Blackbird* combinators + +: used to compose two functions with 1/2/3 arguments + +: `((f ∘ g) x)`{.bruijn} = `(f (g x))`{.bruijn} + +: `(((f ∘∘ g) x) y)`{.bruijn} = `(f ((g x) y))`{.bruijn} + +: `((((f ∘∘∘ g) x) y) z)`{.bruijn} = `(f (((g x) y) z))`{.bruijn} + +`c`{.bruijn} or `\‣`{.bruijn}: *Cardinal* combinator + +: used to flip arguments (e.g. for higher-order application) + +: `((\f x) y)`{.bruijn} = `((f y) x)`{.bruijn} + +`s`{.bruijn} or `…<*>…`{.bruijn}: *Starling* combinator + +: used to apply one argument to two functions (*substitution*) + +: `((f <*> g) x)`{.bruijn} = `((f x) (g x))`{.bruijn} + +`k`{.bruijn} or `const`{.bruijn}: *Kestrel* combinator + +: used to wrap a term inside an additional abstraction (also for + [boolean logic](data-structures.md#booleansbits-stdlogic)) + +: `(k f)`{.bruijn} = `[f]`{.bruijn} + +`i`{.bruijn} (Haskell's `id`{.haskell}): *Kestrel* combinator + +: used as identity function or to indicate an unused argument + +: `(i x)`{.bruijn} = `x`{.bruijn} + +`ψ`{.bruijn}: *Psi* combinator (Haskell's `on`{.haskell}) + +: used to apply two arguments to one function seperately + +: `((((ψ f) g) x) y)`{.bruijn} = `((f (g x)) (g y))`{.bruijn} + +`ω`{.bruijn}: *Mockingbird*/*omega* combinator + +: used to apply a term to itself + +: `(ω f)`{.bruijn} = `(f f)`{.bruijn} + +: Also: `Ω`{.bruijn} = `(ω ω)`{.bruijn} + +------------------------------------------------------------------------ + +If you enjoy the use of combinators, you might also enjoy bruijn's +sister language [Birb](https://esolangs.org/wiki/Birb). + +[^1]: Smullyan, Raymond M. To Mock a Mockingbird: and other logic + puzzles including an amazing adventure in combinatory logic. Oxford + University Press, USA, 2000. diff --git a/docs/wiki_src/coding/currying.md b/docs/wiki_src/coding/currying.md index d84eb0a..9a8e48d 100644 --- a/docs/wiki_src/coding/currying.md +++ b/docs/wiki_src/coding/currying.md @@ -1,13 +1,29 @@ # Currying -Lambda calculus naturally supports currying -- that is, only partially +Lambda calculus naturally supports currying -- that is, only *partially* applying a function. In fact *any* function can be applied with *any* amount of arguments! In bruijn, currying is a great way to make functions even more elegant. -Partially applying the `mul`{.bruijn} function: +For example, take the negation function: ``` bruijn -six [0 (+3)] (mul (+2)) +# subtracts argument from zero +-‣ [(+0) - 0] ⧗ Number → Number + +# equivalent curried version +-‣ sub (+0) +``` + +Currying is also very useful for higher-order functions. + +Multiplying values in a list by partially applying the `mul`{.bruijn} +function: + +``` bruijn +# doubles numbers in a list +double-list [0 <$> (mul (+2))] ⧗ (List Number) → (List Number) + +:test (double-list ((+1) : {}(+2))) ((+2) : {}(+4)) ``` diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md index 384ac29..0516bf7 100644 --- a/docs/wiki_src/coding/data-structures.md +++ b/docs/wiki_src/coding/data-structures.md @@ -62,7 +62,8 @@ a-box <>'a' ## Pairs [`std/Pair`](/std/Pair.bruijn.html) -Pairs (tuples) can store any two terms. +Pairs (tuples) can store any two terms. Pairs can be constructed using +the `…:…`{.bruijn} [mixfix](mixfix.md) function. Example: @@ -82,6 +83,11 @@ Lists are a repeated composition (right-associative) of pairs with a (heterogeneous) values and are recursively iterable. The call-by-need reduction order of bruijn allows lazy evaluation (i.e. infinite lists). +Due to the right-associativeness, writing lists by hand is slightly +annoying. The usage of the `…:…`{.bruijn} [mixfix](mixfix.md) and +`{}‣`{.bruijn} [prefix](prefix.md) functions to denote pairs and the +final `empty`{.bruijn} symbol is encouraged. + Example: ``` bruijn @@ -90,10 +96,19 @@ Example: :test ((foldr …+… (+0) ((+1) : ((+2) : {}(+3)))) =? (+6)) (true) ``` +The internal structure of the list encoding means that when a list is +applied to a function, the function is called with the head and tail of +the list. + +``` bruijn +:test ("abc" [[1]]) ('a') +:test ("abc" [[0]]) ("bc") +``` + ## Strings [`std/String`](/std/String.bruijn.html) Strings are just a list of binary encoded bytes. You may use -[`std/List`](/std/List.bruijn.html) in combinatoin with +[`std/List`](/std/List.bruijn.html) in combination with [`std/Number/Binary`](/std/Binary.bruijn.html) to interact with them. Example: diff --git a/docs/wiki_src/coding/examples.md b/docs/wiki_src/coding/examples.md index e69de29..f4d0b62 100644 --- a/docs/wiki_src/coding/examples.md +++ b/docs/wiki_src/coding/examples.md @@ -0,0 +1,134 @@ +# Examples + +## Hello world! + +Hello world using [lists](../coding/data-structures.md#lists-stdlist) +and [IO](../coding/IO.md)! + +``` bruijn +:import std/List . + +main ["Hello " ++ 0 ++ "!\n"] +``` + +``` bash +$ printf "world" | bruijn file.bruijn +Hello world! +``` + +## Syntax + +Example functions demonstrating the syntax without usage of +[`std/`](/std/). + +``` bruijn +# this is a comment +# returns ternary 1 (syntactic sugar) +get-one (+1) + +# we can use the function in all functions below its definition +get-one2 get-one + +# tests are similar to assertions in other languages +# they test equality using α-equivalence of reduced expressions +:test (get-one2) ((+1)) + +# indenting acts similarly to Haskell's where statement +get-one3 foo + bar (+1) + foo bar + +# equivalent of λx.x or Haskell's id x = x +id [0] + +# testing equivalent of (λx.x) (λx.λy.x) = λx.λy.x +# the numbers in the abstractions refer to arguments using +# De Bruijn indices +:test (id [[1]]) ([[1]]) + +# prefix function definition +!‣ [[1]] + +# use prefix function '!' +# ![0] becomes ([[1]] [0]) which in turn becomes [[0]] +:test (![0]) ([[0]]) + +# infix function definition: flip and apply arguments +…<>… [[0 1]] + +# use infix function '<>' +# [[0]] <> [[1]] becomes (([[0 1]] [[0]]) [[1]]) +:test ([[0]] <> [[1]]) ([[1]] [[0]]) + +# multiple arguments +number-set set-of-three (+1) (+2) (+3) + set-of-three [[[[0 1 2 3]]]] + +access-first [0 [[[0]]]] + +:test (access-first number-set) ((+1)) + +# ignore stdin and return string +main ["Hello world!\n"] +``` + +## Standard library + +``` bruijn +:import std/Combinator . +:import std/List . +:import std/Logic . +:import std/Number . +:import std/Option . +:import std/Pair . + +# pairs with some values +love pair me you + me [[[1]]] + you [[[2]]] + +:test (fst love) ([[[1]]]) +:test (snd love) ([[[2]]]) + +# you can also write (me : you) instead of (pair me you) +# also ^love and ~love instead of (fst love) and (snd love) + +# numerical operations +# remember that every mixfix chain is left-associative +five --((+8) + (-4) - (-2)) + +not-five? [if (0 =? (+5)) false true] + +# awesome mixfix functions +:test (∑ (+1) → (+3) | [++0]) ((+9)) +:test (∏ (+1) → (+3) | [++0]) ((+24)) + +:test (not-five? five) (false) + +:test ((uncurry mul (pair (+3) (+2))) =? (+6)) (true) + +# lazy evaluation using infinite lists and indexing +pow2 …!!… (iterate (…⋅… (+2)) (+1)) + +:test ((pow2 (+5)) =? (+32)) (true) + +# options +:test (map inc (some (+1))) (some (+2)) +:test (apply (some (+1)) [some ++0]) (some (+2)) + +# boolean +# the main function gets executed automatically +# ignore stdin arguments by not referencing 0 +main [¬(false ⋀? true ⋁? true)] + +:test (main [0]) (false) +``` + +## More examples + +You can find more example programs in +[`samples/`](https://github.com/marvinborner/bruijn/tree/main/samples) +of our source-code repository. The samples include several solutions to +[Advent of Code](https://adventofcode.com/) problems. + +Reading the source of the [standard library](/std/) can also be helpful. diff --git a/docs/wiki_src/coding/laziness.md b/docs/wiki_src/coding/laziness.md index feec480..20d1205 100644 --- a/docs/wiki_src/coding/laziness.md +++ b/docs/wiki_src/coding/laziness.md @@ -45,8 +45,8 @@ example: :time ((+10) ** (+500)) =? (+400) ``` -This works because a ternary number is just a list of trits which (in -this case) gets recursively generated by the `pow`{.bruijn} function. -The `eq?`{.bruijn} function just throws away the first argument if it's -already clear that the numbers can't be equal (in this case after the -first argument got bigger than `(+400)`{.bruijn}). +This works because a ternary number is just a concatenation of trits +which (in this case) gets recursively generated by the `pow`{.bruijn} +function. The `eq?`{.bruijn} function just throws away the first +argument if it's already clear that the numbers can't be equal (in this +case after the first argument got bigger than `(+400)`{.bruijn}). diff --git a/docs/wiki_src/coding/mixfix.md b/docs/wiki_src/coding/mixfix.md index c85b936..f42d0ab 100644 --- a/docs/wiki_src/coding/mixfix.md +++ b/docs/wiki_src/coding/mixfix.md @@ -1,9 +1,9 @@ # Mixfix Mixfix functions allow arbitrary infix operations based on "substitution -holes" by using the `…` symbol in (special character) definitions. The -symbols and terms always need to be delimited by a space character, else -they get interpreted as a [prefix](prefix.md). +holes" by using the `…` symbol in definitions. The symbols and terms +always need to be delimited by a space character, otherwise they get +interpreted as a [prefix](prefix.md). Example: @@ -31,3 +31,24 @@ literally: ``` bruijn :test (…+… (+4) (+3)) (add (+4) (+3)) ``` + +## Associativity + +If you write several mixfix operations without parenthesis, they will be +reduced in left-associative order. Just make sure that the longer mixfix +chain is not actually overwritten by *another* mixfix chain. + +``` bruijn +:test ((+8) + (-4) ⋅ (-2)) ((-8)) + +# (don't do this) +…+…⋅… [[[(+16)]]] + +:test ((+8) + (-4) ⋅ (-2)) ((+16)) +``` + +## Allowed characters + +Mixfix functions can use any characters of `!?*@:;+-_#$%^&<>/\|{}~=` as +well as mathematical unicode operators and arrows. Each part must be at +least 1 character long. diff --git a/docs/wiki_src/coding/performance.md b/docs/wiki_src/coding/performance.md deleted file mode 100644 index e69de29..0000000 --- a/docs/wiki_src/coding/performance.md +++ /dev/null diff --git a/docs/wiki_src/coding/prefix.md b/docs/wiki_src/coding/prefix.md index 589e081..64f36e9 100644 --- a/docs/wiki_src/coding/prefix.md +++ b/docs/wiki_src/coding/prefix.md @@ -11,7 +11,7 @@ Example: ``` bruijn # defines a negation prefix function called '-' --‣ [(+0) - 0] +-‣ [(+0) - 0] ⧗ Number → Number # returns 0 - 10 = -10 :test (-(+10)) ((-10)) @@ -23,3 +23,9 @@ literally: ``` bruijn :test (-‣ (+10)) ((-10)) ``` + +## Allowed characters + +Prefix functions can use any characters of `!?*@:;+-_#$%^&<>/\|{}~=` as +well as mathematical unicode operators and arrows. They must be at least +1 character long. diff --git a/docs/wiki_src/coding/recursion.md b/docs/wiki_src/coding/recursion.md index 68148e5..9625ef9 100644 --- a/docs/wiki_src/coding/recursion.md +++ b/docs/wiki_src/coding/recursion.md @@ -28,7 +28,7 @@ outer argument is the initial function again. Example for using `y`{.bruijn} to find the factorial of 2: ``` bruijn -# here, `1` is the outer argument (y g) +# here, `1` is the induced outer argument `(y g)` # `0` is the accumulator (the argument of `factorial`) g [[=?0 (+1) (0 ⋅ (1 --0))]] @@ -37,7 +37,7 @@ factorial y g ⧗ Number → Number :test ((factorial (+3)) =? (+6)) (true) ``` -In-the-wild, this could look like this. +In the wild it might look like this: ``` bruijn # 3 abstractions => two arguments @@ -50,7 +50,9 @@ length z [[[rec]]] (+0) ⧗ (List a) → Number case-end 1 ``` -Also see [coding style](style.md) for other style suggestions. +Read [list data structure](data-structures.md#lists-stdlist) for more +information. Also read [coding style](style.md) for other style +suggestions. ## Mutual recurrence relations @@ -69,9 +71,9 @@ g [[[=?0 true (1 --0)]]] # the even? recursive call will be the first argument (2) h [[[=?0 false (2 --0)]]] -even? head (y* g h) ⧗ Number → Bool +even? head (y* g h) ⧗ Number → Boolean -odd? tail (y* g h) ⧗ Number → Bool +odd? tail (y* g h) ⧗ Number → Boolean ``` Read more about this in the blog post [Variadic fixed-point diff --git a/docs/wiki_src/coding/style.md b/docs/wiki_src/coding/style.md index d0ec7a9..a9621d7 100644 --- a/docs/wiki_src/coding/style.md +++ b/docs/wiki_src/coding/style.md @@ -1,16 +1,59 @@ # Coding style -## Scoping +## Program + +- Every function has to be delimited by one empty line. +- Every (non-scoped) function must have a comment directly above it. +- Tests must appear in a single block (no empty lines) one line under + the definition. + +See the [standard library](/std/) for inspiration. + +## Function naming + +De Bruijn indices can be seen as a disadvantage to readability. It's +therefore much more important to name the functions appropriately. + +For functions that return a boolean, we suggest using the suffix `?`. If +your function has different cases it's recommended to use the `case-` +prefix in scoped sub-terms. + +``` bruijn +# from std/Ternary +zero? [0 case-end case-neg case-pos i] ⧗ Number → Boolean + case-end true + case-neg [false] + case-pos [false] +``` + +Appropriate [type signatures](../introduction/syntax.md#types) are also +encouraged. ## If/else -redundant +Since booleans are just lambda terms either returning its first or +second argument, the use of if/else procedures is generally redundant. +See [bit/boolean data +structure](data-structures.md#booleansbits-stdlogic). + +``` bruijn +:test (true 'a' 'b') ('a') +:test (false 'a' 'b') ('b') +``` ## Head/tail -redundant +The internal structure of the list encoding means that when a list is +applied to a function, the function is called with the head and tail of +the list. + +``` bruijn +:test ("abc" [[1]]) ('a') +:test ("abc" [[0]]) ("bc") +``` -## Type signatures +Therefore the recommended style for coding with lists is to use +`head`{.bruijn}/`tail`{.bruijn} only when truly needed. ## Recursion diff --git a/docs/wiki_src/coding/test-driven-development.md b/docs/wiki_src/coding/test-driven-development.md index f62c448..56c1bf1 100644 --- a/docs/wiki_src/coding/test-driven-development.md +++ b/docs/wiki_src/coding/test-driven-development.md @@ -6,21 +6,22 @@ creating functions, we suggest the following procedure: - Write a comment, a type signature, and the head of the function ``` bruijn -# measures the length of a list -length y [[[rec]]] (+0) ⧗ (List a) → Number +# returns the item at index in a list, starting from 0 +index y [[[rec]]] ⧗ (List a) → Number → a ``` -- Write several tests including all edge cases +- Write several tests including edge cases ``` bruijn -# measures the length of a list -length y [[[rec]]] (+0) ⧗ (List a) → Number - -:test (length empty) ((+0)) -:test (length "a") ((+1)) -:test (length ({}empty)) ((+1)) -:test (length (empty : {}empty)) ((+2)) -:test (length ("abc")) ((+3)) +# returns the item at index in a list, starting from 0 +index y [[[rec]]] ⧗ (List a) → Number → a + +:test (empty !! (+0)) (empty) +:test ({}(+1) !! (+0)) ((+1)) +:test (((+1) : ((+2) : {}(+3))) !! (+0)) ((+1)) +:test (((+1) : ((+2) : {}(+3))) !! (+2)) ((+3)) +:test (((+1) : ((+2) : {}(+3))) !! (-1)) (empty) +:test (((+1) : ((+2) : {}(+3))) !! (+3)) (empty) ``` - Finish the implementation until all tests pass (e.g. using the @@ -28,15 +29,16 @@ length y [[[rec]]] (+0) ⧗ (List a) → Number - Refactor and clean up the definition ``` bruijn -# measures the length of a list -length y [[[rec]]] (+0) ⧗ (List a) → Number - rec 0 [[[case-inc]]] case-end - case-inc 5 ++4 1 - case-end 1 - -:test (length empty) ((+0)) -:test (length "a") ((+1)) -:test (length ({}empty)) ((+1)) -:test (length (empty : {}empty)) ((+2)) -:test (length ("abc")) ((+3)) +# returns the item at index in a list, starting from 0 +index y [[[rec]]] ⧗ (List a) → Number → a + rec 0 [[[case-index]]] case-end + case-index =?4 2 (5 --4 1) + case-end empty + +:test (empty !! (+0)) (empty) +:test ({}(+1) !! (+0)) ((+1)) +:test (((+1) : ((+2) : {}(+3))) !! (+0)) ((+1)) +:test (((+1) : ((+2) : {}(+3))) !! (+2)) ((+3)) +:test (((+1) : ((+2) : {}(+3))) !! (-1)) (empty) +:test (((+1) : ((+2) : {}(+3))) !! (+3)) (empty) ``` diff --git a/docs/wiki_src/coding/typing.md b/docs/wiki_src/coding/typing.md deleted file mode 100644 index e69de29..0000000 --- a/docs/wiki_src/coding/typing.md +++ /dev/null diff --git a/docs/wiki_src/coding/uniform-function-call-syntax.md b/docs/wiki_src/coding/uniform-function-call-syntax.md index e69de29..3999961 100644 --- a/docs/wiki_src/coding/uniform-function-call-syntax.md +++ b/docs/wiki_src/coding/uniform-function-call-syntax.md @@ -0,0 +1,14 @@ +# Uniform function call syntax (UFCS) + +UFCS is a syntactic feature that allows you to use functions in a +different (perhaps more "natural") order. + +By using the dot `.` between two terms, the first term will be applied +to the second term instead of the other way around. + +Example: + +``` bruijn +:test ("abc".length) (length "abc") +:test ("abc".length.inc) ((+4)) +``` diff --git a/docs/wiki_src/index.md b/docs/wiki_src/index.md index 3049322..000f874 100644 --- a/docs/wiki_src/index.md +++ b/docs/wiki_src/index.md @@ -3,4 +3,6 @@ Bruijn is basically pure lambda calculus with a bit of syntactic sugar. It has no side effects, primitive functions or datatypes. -Browse this wiki by using the search or by clicking *next* or any of the links. +Browse this wiki by using the search or by clicking *next* or any of the +links. If you prefer free-flowing text, read the blog post [The bruijn +programming language](https://text.marvinborner.de/2023-04-06-01.html). diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md index 59a7c59..574c5ee 100644 --- a/docs/wiki_src/introduction/lambda-calculus.md +++ b/docs/wiki_src/introduction/lambda-calculus.md @@ -4,33 +4,38 @@ Bruijn is based on De Bruijn indexed lambda calculus. ## Traditional lambda calculus -Lambda calculus basically has three types of expressions: +Lambda calculus basically has three types of terms: -- *Variable*: `x` represents another expression. -- *Abstraction*: `λx.E` accepts an argument x and binds it to - expression `E` respectively. It's helpful to think of abstractions - as anonymous functions. +- *Variable*: `x` binds the named variable `x` to an abstraction. +- *Abstraction*: `λx.E` accepts an argument `x` and binds it to term + `E` respectively. It's helpful to think of abstractions as anonymous + functions. - *Application*: `(f x)` applies `f` to `x` -- the standard convention allows repeated left-associative application: `(f x y z)` is `(((f x) y) z)`. -Combining these expressions and removing redundant parentheses can -result in expressions like λx.λy.x y, basically representing a function -with two parameters that uses its second parameter as an argument for -its first. +Combining these terms and removing redundant parentheses can result in +terms like λx.λy.x y, basically representing a function with two +parameters that uses its second parameter as an argument for its first. -Evaluating expressions is called *reduction*. There's only one rule you -need to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an -abstraction with an argument substitutes the argument inside the -expression of the abstraction ("β-reduction"). There are many different -kinds of reduction techniques, but they basically all come back to this -simple rule -- mainly because of the "Church-Rosser theorem" that states -that the order of reduction doesn't change the eventual result. +Evaluating terms is called *reduction*. There's only one rule you need +to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an +abstraction with an argument substitutes the argument inside the body of +the abstraction ("β-reduction"). There are many different kinds of +reduction techniques, but they basically all come back to this simple +rule -- mainly because of the "Church-Rosser theorem" that states that +the order of reduction doesn't change the eventual result. When we talk about reduction in bruijn, we typically mean "reduction until normal form" -- we reduce until the term can't be reduced any further (there does not exist any `((λx.E) A)`). +``` bruijn +((λx.x) (λx.x)) ⤳ (λx.x) +((λx.x) (λx.λy.x)) ⤳ (λx.λy.x) +((λx.λy.x) (λx.x)) ⤳ (λy.λx.x) +``` + ## De Bruijn indices Programs written in lambda calculus often have many abstractions and diff --git a/docs/wiki_src/introduction/setup.md b/docs/wiki_src/introduction/setup.md index 92f9886..e47ea6f 100644 --- a/docs/wiki_src/introduction/setup.md +++ b/docs/wiki_src/introduction/setup.md @@ -1,6 +1,52 @@ # Setup -- unicode keymap -- editors -- syntax highlighting -- broogle +In theory you can use any common editor and operating system. Please +create an [issue on +GitHub](https://github.com/marvinborner/bruijn/issues/new) if you have +problems setting up bruijn. + +## Recommended setup + +The recommended setup is to use [Vim](https://www.vim.org/) and its +bruijn plugin. + +The Vim plugin adds syntax highlighting for bruijn files as well as a +custom keymap for typing commonly used unicode symbols. + +### Installation + +1. Use Vim and [vim-plug](https://github.com/junegunn/vim-plug) (or + comparable plugin managers) +2. Add `"Plug 'marvinborner/bruijn', { 'rtp': 'editors/vim' }"` to your + `.vimrc` +3. Run `:PlugInstall` + +### Unicode abbreviations + +You can find all abbreviations in +[`editors/vim/syntax/bruijn.vim`](https://github.com/marvinborner/bruijn/blob/main/editors/vim/syntax/bruijn.vim). +Abbreviations get replaced after pressing space or `C-]`. Feel free to +suggest improvements or create your own abbreviations. + +## Alternatives + +We have a Kate XML syntax highlighting file in +[`editors/kate/bruijn.xml`](https://github.com/marvinborner/bruijn/blob/main/editors/kate/bruijn.xml), +although it has *not* actually been tested with Kate (only as a syntax +highlighting file for `pandoc`). + +## Broogle + +Broogle is a tool for searching standard library functions by name, type +signatures, or comment. It's highly inspired by Haskell's +[hoogle](https://hoogle.haskell.org/). + +You can use it after cloning [bruijn's +repository](https://github.com/marvinborner/bruijn) and installing `rg` +(`ripgrep`), `jq`, `sed`, and `awk`. + +``` bash +./broogle.sh -t "a -> a" +./broogle.sh -f "i" +./broogle.sh -c "idiot combinator" +``` diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md index 55e2c21..4dbc784 100644 --- a/docs/wiki_src/introduction/syntax.md +++ b/docs/wiki_src/introduction/syntax.md @@ -5,12 +5,16 @@ an esoteric programming language. Most notably the usage of lambda calculus logic, combinators, and De Bruijn indices can be confusing at first -- it's definitely possible to get used to them though! -Bruijn uses a [variation of lambda calculus](lambda-calculus.md). +Bruijn uses a [variation of lambda calculus](lambda-calculus.md). For +subjective syntax rules, read [coding style](../coding/style.md). Also +see the [examples](../coding/examples.md). ## Definitions Bruijn works by defining named substitution rules, where each usage of -the identifier will get substituted respectively. +the identifier will get substituted respectively. You can't use +definitions before they are defined, every file gets substituted from +top to bottom. Since there's no other major syntactic block, bruijn omits the equal symbol for definitions. @@ -55,7 +59,7 @@ closed1 [[[2 0] 1]] Bruijn does not give warnings for open terms and reduces them as normal. In some cases it's actually encouraged to use open terms as sub-terms -for better readability (see [coding style +for improved readability (see [coding style suggestions](../coding/style.md)). ## Imports @@ -101,8 +105,8 @@ After running: reduced to [[1]] = [[0]] Tests are always run for the executed file and any files it contains. If -they take too long, you can enable the *YOLO* mode by using bruijn's -`-y` argument. +they take too long and you're sure your code is correct, you can enable +the *YOLO* mode to disable tests by using bruijn's `-y` argument. ## Scoping @@ -145,4 +149,32 @@ structures](../coding/data-structures.md). ## Types -TODO. +As of right now, typing is entirely optional and *purely* for +documentation/aesthetics. Aside from syntax, types do not get checked in +any way. + +We do have plans to implement type checking in the future, unfortunately +almost all trivial typing mechanisms for pure lambda calculus reduce its +power immensely. + +The current syntax of types is quite simple: + + POLYMORPHIC := [a-z]+ + CONSTRUCTOR := ([A-Z][a-z]* TYPE) + FUNCTION := (TYPE → ... → TYPE) + IDENTIFIER := [A-Z][a-z]* + TYPE := IDENTIFIER | TYPE-VARIABLE | CONSTRUCTOR | FUNCTION + SIGNATURE := TYPE → ... → Type + +The type signature can be written at the end of any bruijn term using +the `⧗`{.bruijn} symbol. + +Examples: + +``` bruijn +# from std/Combinator +c [[[2 0 1]]] ⧗ (a → b → c) → b → a → c + +# from std/List +empty? [0 [[[false]]] true] ⧗ (List a) → Boolean +``` diff --git a/docs/wiki_src/technical/arithmetic.md b/docs/wiki_src/technical/arithmetic.md deleted file mode 100644 index e69de29..0000000 --- a/docs/wiki_src/technical/arithmetic.md +++ /dev/null diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md new file mode 100644 index 0000000..05fd683 --- /dev/null +++ b/docs/wiki_src/technical/performance.md @@ -0,0 +1,24 @@ +# Performance + +The reduction of lambda calculus is (practically) not very efficient. As +an extension, bruijn also suffers from bad performance. + +Bruijn's interpreter works by substituting the entire program into one +huge lambda calculus term that will then get reduced by the +[reducer](reduction.md). As a result, many equivalent terms get +evaluated multiple times (although some of this get's solved by bruijn's +call-by-need reduction strategy). We currently work on a solution that +reduces all equivalent terms as one, which turns out is not actually +that trivial. Follow the [blog](https://text.marvinborner.de) to keep up +to date with the development. + +Aside from that, bruijn is still much faster than most of the hobby +programming languages based on pure lambda calculus. This is because of +the [RKNL reducer](reduction.md) and our choice of default [number/byte +encodings](../coding/data-structures.md). + +``` bruijn +> :import std/Math . +> :time fac (+30) +0.15 seconds +``` diff --git a/docs/wiki_src/technical/reduction.md b/docs/wiki_src/technical/reduction.md index e69de29..97bd78f 100644 --- a/docs/wiki_src/technical/reduction.md +++ b/docs/wiki_src/technical/reduction.md @@ -0,0 +1,12 @@ +# Reduction + +Bruijn uses the RKNL abstract machine reducer[^1]. RKNL uses the +call-by-need reduction strategy, similar to Haskell and other functional +programming languages. For you this means that you have efficient +support for [laziness](../coding/laziness.md) with generally less +redundant reductions. + +[^1]: [Biernacka, Małgorzata, Witold Charatonik, and Tomasz Drab. "A + simple and efficient implementation of strong call by need by an + abstract machine." Proceedings of the ACM on Programming Languages + 6.ICFP (2022): 109-136.](https://doi.org/10.5281/zenodo.6786796) @@ -1,346 +1,35 @@ <p align="center"> <img width="200" src="https://raw.githubusercontent.com/marvinborner/bruijn/main/docs/res/logo.png" alt="Bruijn logo"/> </p> -<h1 align="center"> -bruijn -</h1> -> A purely academic programming language based on lambda calculus and De -> Bruijn indices written in Haskell. +> A purely functional programming language based on lambda calculus and +> De Bruijn indices written in Haskell. -[Jump to examples](#Examples) or use the navigation tree to jump to -other sections. - -Docs, articles, examples and more: +Wiki, docs, articles, examples and more: [website](https://bruijn.marvinborner.de). ## Features -- **De Bruijn indices[\[0\]](#References)** eliminate the complexity of - α-equivalence and α-conversion +- **De Bruijn indices** eliminate the complexity of α-equivalence and + α-conversion - Unique **bracket-style representation** for lambda abstractions enables improved human-readability and faster syntactic perception - **Call-by-need** reduction with great time/memory complexity by using - the RKNL[\[4\]](#References) abstract machine (similar to + the RKNL abstract machine (similar to [calm](https://github.com/marvinborner/calm/)) - **Syntactic sugar** for unary/binary/ternary numerals and binary-encoded strings and chars - **No primitive functions** - every function is implemented in Bruijn itself -- Highly space-efficient compilation to **binary lambda calculus - (BLC)[\[2\]](#References)[\[3\]](#References)** additionally to normal - interpretation and REPL +- Highly space-efficient compilation to **binary lambda calculus (BLC)** + additionally to normal interpretation and REPL - Strongly **opinionated parser** with strict syntax rules - **Recursion** can be implemented using combinators such as Y, Z or ω - Substantial **standard library** featuring many useful functions (see `std/`) -## Basics - -### De Bruijn indices - -De Bruijn indices[\[0\]](#References) replace the concept of variables -in lambda calculus. The index basically represents the abstraction layer -you want to reference beginning at 0 with the innermost layer. - -For example, λx.x becomes λ0 because x referenced the first abstraction -layer. Furthermore, λx.λy.xy becomes λλ10 and so forth. - -You can read more about De Bruijn indices on -[Wikipedia](https://en.wikipedia.org/wiki/De_Bruijn_index). - -### Syntax - -In general the syntax of bruijn is pretty similar to the previously -presented normal lambda calculus syntax with De Bruijn indices. The main -difference of the syntax of expressions is the usage of square brackets -instead of λs (e.g. `[[1 0]]` instead of λλ10). - -You can use any function that you’ve previously defined. You can also -overwrite previously defined functions. The environment gets interpreted -from bottom to top (starting at `main`). - -The following are the main syntax specifications in the (minorly -extended) [Backus-Naur -form](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form) -(prefix/infix/mixfix operators are omitted for simplicity). - - <identifier> ::= [a-ω,A-Ω,_][a-ω,A-Ω,0-9,?,!,',-]* - <namespace> ::= [A-Ω][a-ω,A-Ω]+ - <abstraction> ::= "[" <expression> "]" - <number> ::= ("+" | "-")[0-9]+[u|b|t] - <bruijn> ::= [0-9] - <singleton> ::= <bruijn> | <number> | <abstraction> | "(" <application> ")" | [namespace.]<identifier> - <application> ::= <singleton> <singleton> - <expression> ::= <application> | <singleton> - <test> ::= ":test " "(" <expression> ") (" <expression> ")" - <import> ::= ":import " <path> [namespace] - <input> ::= ":input " <path> - <comment> ::= "# " <letter>* - -Differences in syntax between REPL and file: - -**For files**: - -The execution of a file begins at the `main` function. Its existence is -mandatory. Note the missing equal sign in definitions. - - <definition> ::= <identifier> <expression> - <line> ::= <definition> | <comment> | <import> | <test> | "\n" - -**For REPL**: - - <definition> ::= <identifier> = <expression> - <watch> ::= ":watch " <path> - <time> ::= ":time " <expression> - <free> ::= ":free" - <line> ::= <definition> | <expression> | <comment> | <import> | <watch> | <test> | <time> | <free> | "\n" - -### Numbers - -Numbers in bruijn always have a sign in front of them or else they will -be mistaken for De Bruijn indices. They also need to be between -parenthesis because of prefix functions. You can then enter a character -indicating the desired base of the number. - -Generally the decimal representation is only syntactic sugar for a -lambda calculus encoding. The default base is balanced ternary because -it’s a great compromise between performance and size (according to -[\[1\]](#References)). The currently supported base suffixes are ‘t’ for -balanced ternary (default), ‘b’ for binary and ‘u’ for unary -(church-encoded). - -You don’t have to care about the internals too much though as long as -you use the included operations from the standard library -(`std/Number/`). The REPL even tries its best at displaying decimal -numbers directly for expressions that look like numbers. - -For example, in the REPL: - - λ (+42) - *> [[[[(0 (2 (2 (2 (1 3)))))]]]] - ?> 42t - - λ (+42b) - *> [[[(0 (1 (0 (1 (0 (1 2))))))]]] - ?> 42b - -### Standard library - -You may want to use the included standard library to reach your -program’s full potential. It includes many common combinators as well as -functions for numerical, boolean and IO operations and much more. - -For example, you can import the standard library for numbers using -`:import std/Number`. You can find all available libraries in the `std/` -directory. - -### Broogle - -You can use the broogle script (inspired by Haskell’s hoogle) to search -for standard library functions by type, name or comment: - - ./broogle.sh -t "a -> a" - ./broogle.sh -f "i" - ./broogle.sh -c "idiot combinator" - -The script uses the dependencies `rg`, `jq`, `sed` and `awk`. - -### Examples - -You can find more “real world” examples here: [samples](/samples). - -You can try these by experimenting in the REPL or by running them as a -file. - -**Remember** that you need an equal sign between the function name and -its definition if you’re using the REPL. - -#### Plain execution without any predefined functions - -Without using its standard library bruijn is basically unmodified pure -lambda calculus with syntactically sugared numerals, strings and chars. -Bruijn doesn’t support any numerical operations or any other -infix/prefix functions by default. Using it without its standard library -can be quite fun, though - especially for exploring and understanding -the logic of lambda calculus: - - # this is a comment - # we now define a function returning a ternary 1 (syntactic sugar) - get-one (+1) - - # we can use the function in all functions below its definition - get-one2 get-one - - # tests are similar to assertions in other languages - # they test equality using α-equivalence of reduced expressions - # in this example they're used to show the reduced expressions - :test (get-one2) ((+1)) - - # remember that numbers always need to be written in parenthesis - # therefore two braces are needed in tests because testing exprs - # must always be in parenthesis as well - - # indenting acts similarly to Haskell's where statement - get-one3 foo - bar (+1) - foo bar - - # equivalent of λx.x or Haskell's id x = x - id [0] - - # testing equivalent of (λx.x) (λx.λy.x) = λx.λy.x - # the numbers in the abstractions refer to arguments using - # De Bruijn indices - :test (id [[1]]) ([[1]]) - - # prefix function definition - !‣ [[1]] - - # use prefix function '!' - # ![0] becomes ([[1]] [0]) which in turn becomes [[0]] - :test (![0]) ([[0]]) - - # infix function definition: flip and apply arguments - …<>… [[0 1]] - - # use infix function '<>' - # [[0]] <> [[1]] becomes (([[0 1]] [[0]]) [[1]]) - :test ([[0]] <> [[1]]) ([[1]] [[0]]) - - # multiple arguments - number-set set-of-three (+1) (+2) (+3) - set-of-three [[[[0 1 2 3]]]] - - access-first [0 [[[0]]]] - - :test (access-first number-set) ((+1)) - - # ignore args and return string - main ["Hello world!\n"] - -#### Using standard library - -Concatenating “Hello world” program using IO (the first argument of the -`main` function is a binary representation of stdin): - - :import std/List . - - main ["Hello " ++ 0 ++ "!\n"] - -You can then use `printf "world" | bruijn file.bruijn` to get “Hello -world!” - -Some other great functions: - - :import std/Combinator . - :import std/List . - :import std/Logic . - :import std/Number . - :import std/Option . - :import std/Pair . - - # pairs with some values - love pair me you - me [[[1]]] - you [[[2]]] - - :test (fst love) ([[[1]]]) - :test (snd love) ([[[2]]]) - - # you can also write (me : you) instead of (pair me you) - # also (^love) and (~love) instead of (fst love) and (snd love) - - # numerical operations - # remember that every mixfix chain is left-associative - five --((+8) + (-4) - (-2)) - - not-five? [if (0 =? (+5)) false true] - - # awesome mixfix functions - :test (∑ (+1) → (+3) | [++0]) ((+9)) - :test (∏ (+1) → (+3) | [++0]) ((+24)) - - :test (not-five? five) (false) - - :test ((uncurry mul (pair (+3) (+2))) =? (+6)) (true) - - # lazy evaluation using infinite lists and indexing - pow2 …!!… (iterate (…⋅… (+2)) (+1)) - - :test ((pow2 (+5)) =? (+32)) (true) - - # options - :test (map inc (some (+1))) (some (+2)) - :test (apply (some (+1)) [some ++0]) (some (+2)) - - # boolean - # the main function gets executed automatically - # ignore stdin arguments by not referencing 0 - main [¬(false ⋀? true ⋁? true)] - - :test (main [0]) (false) - -Read the files in `std/` for an overview of all functions/libraries or -visit the interactive [website](https://bruijn.marvinborner.de). - -### Compilation - -You can compile bruijn to John Tromp’s -BLC[\[2\]](#References)[\[3\]](#References). Only the used functions -actually get compiled in order to achieve a minimal binary size. - -BLC uses the following encoding: - -| term | lambda | bruijn | BLC | -|:-------------|:-------|:-------|:-----------------| -| abstraction | λM | \[M\] | 00M | -| application | MN | MN | 01MN | -| bruijn index | i | i | 1<sup>i+1</sup>0 | - -You may also want to use my [BLoC](https://github.com/marvinborner/bloc) -format, which removes redundant duplicates – very useful to reduce the -size of typical bruijn programs. Typical workflow using the `bloc` util: - - bruijn -B program.bruijn | bloc --from-blc -i - -o out.bloc - cat input | bruijn -E <(bloc --from-bloc -i out.bloc) - -## Installation - -You first need to install Haskell and Haskell Stack using the guidelines -of your operating system. - -Using Haskell Stack, run `stack run` or `stack run -- [args]` to play -around and use `stack install` to install bruijn into your path. - -## REPL config - -You can configure the REPL by editing the `config` file. `stack install` -or `stack run` will move the file into a data directory. - -More options can be found -[here](https://github.com/judah/haskeline/wiki/UserPreferences). - -## Usage - -Please read the usage information in the executable by using the `-h` -argument. - -## References +## Wiki -0. De Bruijn, Nicolaas Govert. “Lambda calculus notation with nameless - dummies, a tool for automatic formula manipulation, with application - to the Church-Rosser theorem.” Indagationes Mathematicae - (Proceedings). Vol. 75. No. 5. North-Holland, 1972. -1. Mogensen, Torben. “An investigation of compact and efficient number - representations in the pure lambda calculus.” International Andrei - Ershov Memorial Conference on Perspectives of System Informatics. - Springer, Berlin, Heidelberg, 2001. -2. Tromp, John. “Binary lambda calculus and combinatory logic.” - Randomness and Complexity, from Leibniz to Chaitin. 2007. 237-260. -3. Tromp, John. “Functional Bits: Lambda Calculus based Algorithmic - Information Theory.” (2022). -4. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and - efficient implementation of strong call by need by an abstract - machine. Proceedings of the ACM on Programming Languages, 6(ICFP), - 109-136. +Learn anything about bruijn in the +[wiki](https://bruijn.marvinborner.de/wiki/) (also found in +`docs/wiki_src/`). |