Started creating new docs with wiki

author: Marvin Borner 2023-11-06 00:24:11 +0100
committer: Marvin Borner 2023-11-06 00:24:31 +0100
commit: 9d722a0b6138827de743f9fe4acbf3f2c1830bb0 (patch)
tree: 789b8df72f0f2cae2bb4009ddb93b914bf83eb2c /docs
parent: 027fc0f91ae7bf64564091fbcec7694f5d53d8fe (diff)
31 files changed, 1024 insertions, 15 deletions
diff --git a/docs/.gitignore b/docs/.gitignore
index 4e1ae2d..7595ce4 100644
--- a/docs/.gitignore
+++ b/docs/.gitignore
@@ -1 +1,2 @@
 std/
+wiki/
diff --git a/docs/gen.sh b/docs/gen.sh
index 5d295e7..f79ce6b 100755
--- a/docs/gen.sh
+++ b/docs/gen.sh
@@ -18,3 +18,8 @@ done
 sed -e "s@LINKS@$links@g" index.template >std/index.html
 
 cp res/* content.js content.css index.css std/
+
+echo "std done"
+
+mkdocs build
+echo "wiki done"
diff --git a/docs/index.html b/docs/index.html
index 3303ffc..deb1d92 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -56,7 +56,7 @@
 		<div class="example">
 			<p>
 				Substantial standard library.<br>
-				<a href="std/">Docs</a>
+				<a href="std/">Source</a>
 			</p>
 			<pre class="code">
 <span class="repl">></span> <span class="mixfix">∏</span> <span class="ternary">(+1)</span> <span class="mixfix">→</span> <span class="ternary">(+3)</span> <span class="mixfix">|</span> <span class="symbol">++‣</span>
@@ -80,7 +80,7 @@ hello world!</pre>
 		</div>
 
 		<div class="bar big">
-			Learn more: <a href="https://github.com/marvinborner/bruijn">GitHub</a>
+            Learn more: <a href="wiki/">Wiki</a>, <a href="std/">Std</a>
 		</div>
 
 		<div class="instructions">
@@ -104,16 +104,6 @@ in std/Number/Unary.bruijn:35
 		</div>
 
 		<div class="instructions">
-			<h1>Syntax highlighting</h1>
-			<ol>
-				<li>Use vim and vim-plug</li>
-				<li>Add "Plug 'marvinborner/bruijn', { 'rtp': 'editors/vim' }" to your .vimrc</li>
-				<li>Run :PlugInstall</li>
-			</ol>
-			Learn more: <a href="https://github.com/marvinborner/bruijn/tree/main/editors">GitHub</a>
-		</div>
-
-		<div class="instructions">
 			<h1>Why?</h1>
 			<ul>
 				<li>Compiled binary lambda calculus is incredibly expressive and tiny. Read the articles by <a href="https://justine.lol/lambda/#why">Justine</a> and <a href="https://tromp.github.io/cl/cl.html">Tromp</a>.</li>
@@ -130,11 +120,13 @@ in std/Number/Unary.bruijn:35
 				<!-- feel free to add your own -->
 				<li><a href="https://text.marvinborner.de/2023-04-06-01.html">The bruijn programming language</a></li>
 				<li><a href="https://text.marvinborner.de/2023-04-07-01.html">Data structures in pure lambda calculus</a></li>
+				<li><a href="https://text.marvinborner.de/2023-06-18-15.html">Variadic fixed-point combinators</a></li>
+				<li><a href="https://text.marvinborner.de/2023-09-03-21.html">Homoiconic self interpretation of lambda calculus</a></li>
 			</ul>
 		</div>
 
 		<div class="bar big">
-			Standard library: <a href="std/">Docs</a>
+			Open-source: <a href="https://github.com/marvinborner/bruijn">GitHub</a>
 		</div>
 
 		<script src="script.js" charset="utf-8"></script>
diff --git a/docs/index.template b/docs/index.template
index 9cbb1f5..c33f5db 100644
--- a/docs/index.template
+++ b/docs/index.template
@@ -8,6 +8,7 @@
 	</head>
 	<body>
 		<h1>bruijn standard library</h1>
+This is the browsable standard library of the bruijn programming language. Follow any of the links below to see the source of the corresponding module.
 		<ol>
 			LINKS
 		</ol>
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
new file mode 100644
index 0000000..9b557ca
--- /dev/null
+++ b/docs/mkdocs.yml
@@ -0,0 +1,59 @@
+site_name: Bruijn Wiki
+docs_dir: wiki_src/
+site_dir: wiki/
+
+extra_css: [custom.css]
+
+theme:
+  name: terminal
+  palette: dark
+  features:
+    - navigation.top.cursor_animation.hide
+    - footer.prev_next
+
+nav:
+  - Index: index.md
+  - Introduction:
+    - introduction/installation.md
+    - introduction/lambda-calculus.md
+    - introduction/setup.md
+    - introduction/syntax.md
+  - Coding:
+    - coding/REPL.md
+    - TDD: coding/test-driven-development.md
+    - coding/mixfix.md
+    - coding/prefix.md
+    - coding/recursion.md
+    - coding/data-structures.md
+    - coding/combinators.md
+    - coding/currying.md
+    - coding/laziness.md
+    - coding/IO.md
+    - coding/meta-programming.md
+    - UFCS: coding/uniform-function-call-syntax.md
+    - coding/style.md
+    - coding/typing.md
+    - coding/compilation.md
+    - coding/performance.md
+    - coding/examples.md
+  - Technical:
+    - technical/arithmetic.md
+    - technical/reduction.md
+  - Landing page: https://bruijn.marvinborner.de
+  - GitHub: https://github.com/marvinborner/bruijn
+
+markdown_extensions:
+  - attr_list
+  - def_list
+  - footnotes
+  - md_in_html
+  - meta
+  - toc:
+      permalink: "#"
+      permalink_title: Anchor link to this section for reference
+  - pymdownx.caret
+  - pymdownx.mark
+  - pymdownx.tilde
+  - pymdownx.snippets:
+      base_path: 
+        - wiki_src
diff --git a/docs/readme.md b/docs/readme.md
index a8b0829..da286b9 100644
--- a/docs/readme.md
+++ b/docs/readme.md
@@ -1,4 +1,4 @@
 # Docs
 
-Visit the compiled [docs](https://bruijn.marvinborner.de) for the full
-experience.
+These files get translated to HTML. Visit the compiled
+[docs](https://bruijn.marvinborner.de) for the full experience.
diff --git a/docs/wiki_src/coding/IO.md b/docs/wiki_src/coding/IO.md
new file mode 100644
index 0000000..974f98e
--- /dev/null
+++ b/docs/wiki_src/coding/IO.md
@@ -0,0 +1,29 @@
+# IO
+
+Bruijn supports a variant of John Tromp's monadic IO[^1].
+
+Every program's `main`{.bruijn} function has an additional abstraction
+that gets applied with a lazy list of input bytes. These bytes are
+encoded as the syntactic sugar encoding of binary numbers, which can be
+manipulated with [`std/Number/Binary`](/std/Number_Binary.bruijn.html).
+
+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.
+
+## Example
+
+``` bruijn
+:import std/List .
+
+# reverse the input list
+main [<~>0]
+```
+
+``` bash
+$ printf "tacocat" | bruijn reverse.bruijn
+tacocat
+```
+
+[^1]: [Tromp, John. "Functional Bits: Lambda Calculus based Algorithmic
+    Information Theory." (2023).](https://tromp.github.io/cl/LC.pdf)
diff --git a/docs/wiki_src/coding/REPL.md b/docs/wiki_src/coding/REPL.md
new file mode 100644
index 0000000..a801ef9
--- /dev/null
+++ b/docs/wiki_src/coding/REPL.md
@@ -0,0 +1,100 @@
+# REPL
+
+The REPL is a very helpful feature for functional programming languages
+like bruijn. You can use it to continuously test or execute parts of
+your code.
+
+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.
+
+## Definitions
+
+Since everything you type will get evaluated, definitions (compared to
+definitions in files) require an equal sign:
+
+``` bruijn
+> id = [0]
+> id
+[0]
+```
+
+## Commands
+
+### `:import`{.bruijn}/`:input`{.bruijn}
+
+Equivalent to the [respective commands in
+files](../introduction/syntax.md#imports).
+
+``` bruijn
+> :import std/Math .
+```
+
+### `:test`{.bruijn}
+
+Equivalent to the [test command in
+files](../introduction/syntax.md#tests).
+
+``` bruijn
+> :test ([0]) ([[1]])
+ERROR test failed: [0] = [[1]]
+      reduced to [0] = [[1]]
+```
+
+### `:watch`{.bruijn}
+
+`:watch`{.bruijn} re-imports the file automatically after every saved
+change. It will rerun any test the watched file contains.
+
+``` bruijn
+> :watch collatz-proof
+```
+
+This can be very helpful for [test driven
+development](test-driven-development.md).
+
+### `:time`{.bruijn}
+
+Measures the time from start of reduction to its end (normal form) in
+seconds.
+
+``` bruijn
+> :time fac (+30)
+0.15 seconds
+```
+
+### `:blc`{.bruijn}
+
+Translates both the unreduced and the reduced expression to binary
+lambda calculus. Helpful for golfed [compilation](compilation.md).
+
+``` bruijn
+> :blc [0] [0]
+0100100010
+0010
+```
+
+### `:length`{.bruijn}
+
+Measures the length of the binary lambda calculus encoding of both the
+unreduced and the reduced expression. Helpful for golfed
+[compilation](compilation.md).
+
+``` bruijn
+> :blc [0] [0]
+0100100010
+0010
+```
+
+### `:free`{.bruijn}
+
+The `free` command frees the current environment including all defined
+identifiers and imported files.
+
+``` bruijn
+> id = [0]
+> :free
+> id
+ERROR undefined identifier id
+```
diff --git a/docs/wiki_src/coding/combinators.md b/docs/wiki_src/coding/combinators.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/coding/combinators.md
diff --git a/docs/wiki_src/coding/compilation.md b/docs/wiki_src/coding/compilation.md
new file mode 100644
index 0000000..9863c21
--- /dev/null
+++ b/docs/wiki_src/coding/compilation.md
@@ -0,0 +1,44 @@
+# Compilation
+
+Bruijn can be compiled to John Tromp’s binary lambda calculus (BLC).
+
+BLC uses the following encoding:
+
+| term         | lambda | bruijn  | BLC              |
+|:-------------|:-------|:--------|:-----------------|
+| abstraction  | λM     | `[M]`   | 00M              |
+| application  | (MN)   | `(M N)` | 01MN             |
+| bruijn index | i      | `i`     | 1<sup>i+1</sup>0 |
+
+There are two modes of compilation:
+
+- **Bitwise** compiles to BLC and encodes every bit as 1 bit and pads
+  the last remaining byte: `bruijn -b path`
+- **ASCII** compiles to BLC and encodes every bit as 1 ASCII character
+  (`'0'`/`'1'`): `bruijn -B path`
+
+## Compilation overhead
+
+Typical compilation to BLC results in much redundant code, since every
+used function gets substituted and translated separately. In
+`((+3) + (+4) + (+3))`, for example, `add` gets compiled to BLC two
+times, resulting in a redundant overhead of around 3500 bits.
+
+This is because BLC was never intended for compilation of normal
+programs, but mainly as an academic encoding model. This also means that
+it’s quite good for writing very expressive and minimal programs
+(i.e. obfuscated code golfing, see [John Tromp’s
+IOCCC](https://ioccc.org/2012/tromp/hint.html)).
+
+Most programs, however, won’t be golfed and can result in rather large
+compiled programs. While there’s not really any practical need for
+compilation aside from golfing, you could still use the
+[BLoC](https://github.com/marvinborner/bloc) project to optimize
+redundant terms.
+
+Typical workflow:
+
+``` bash
+$ bruijn -B program.bruijn | bloc --from-blc -i - -o out.bloc
+$ cat input | bruijn -E <(bloc --from-bloc -i out.bloc)
+```
diff --git a/docs/wiki_src/coding/currying.md b/docs/wiki_src/coding/currying.md
new file mode 100644
index 0000000..d84eb0a
--- /dev/null
+++ b/docs/wiki_src/coding/currying.md
@@ -0,0 +1,13 @@
+# Currying
+
+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:
+
+``` bruijn
+six [0 (+3)] (mul (+2))
+```
diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md
new file mode 100644
index 0000000..384ac29
--- /dev/null
+++ b/docs/wiki_src/coding/data-structures.md
@@ -0,0 +1,111 @@
+# Data structures
+
+Bruijn's standard library defines several common data structures.
+
+Relevant blog post: [Data structures in pure lambda
+calculus](https://text.marvinborner.de/2023-04-07-01.html).
+
+## States
+
+For storing states (i.e. enums), you can use the available libraries and
+syntactic sugar.
+
+### Booleans/bits [`std/Logic`](/std/Logic.bruijn.html)
+
+-   typical [Church
+    booleans](https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans)
+    -- fast and reliable
+-   encoding: `true`{.bruijn}=`[[1]]`{.bruijn},
+    `false`{.bruijn}=`[[0]]`{.bruijn}
+
+### Unary numbers [`std/Number/Unary`](/std/Number_Unary.bruijn.html)
+
+-   `u` suffix for syntactic sugar, e.g. `(+3u)`{.bruijn}
+-   encoding: `(+4u)`{.bruijn}=`[[(1 (1 (1 (1 0))))]]`{.bruijn}
+-   typical [Church
+    numerals](https://en.wikipedia.org/wiki/Church_encoding#Church_numerals),
+    simple but high space/time complexity
+-   only positive numbers
+
+### Binary numbers [`std/Number/Binary`](/std/Number_Binary.bruijn.html)
+
+-   `b` suffix for syntactic sugar, e.g. `(+3b)`{.bruijn}
+-   encoding: `(+4b)`{.bruijn}=`[[[0 (0 (1 2))]]]`{.bruijn}
+-   encoding for chars/strings, e.g. `'0'`{.bruijn}=`(+48b)`{.bruijn}
+-   faster and more compact than unary
+-   only positive numbers (excluding two's complement)
+
+### Balanced ternary [`std/Number/Ternary`](/std/Number_Ternary.bruijn.html)
+
+-   default syntactic sugar for numbers (optional suffix `t`),
+    e.g. `(+3)`{.bruijn}
+-   encoding: `(+4)`{.bruijn}=`[[[[(1 (1 3))]]]]`,
+    `(-4)`{.bruijn}=`[[[[(2 (2 3))]]]]`{.bruijn}
+-   faster and more compact than binary[^1]
+-   positive and negative numbers
+
+## Boxes [`std/Box`](/std/Box.bruijn.html)
+
+Boxes are good for storing single values as immutable object with an
+empty/full state.
+
+Example:
+
+``` bruijn
+a-box <>'a'
+
+:test (set? a-box) (true)
+:test (get 'b' a-box) ('a')
+:test (get 'b' empty) ('b')
+:test (store! a-box 'b') (<>'b')
+```
+
+## Pairs [`std/Pair`](/std/Pair.bruijn.html)
+
+Pairs (tuples) can store any two terms.
+
+Example:
+
+``` bruijn
+one-two (+1) : (+2)
+
+:test (^one-two) ((+1))
+:test (~one-two) ((+2))
+:test (inc <$> one-two) ((+2) : (+3))
+:test (uncurry add one-two) ((+3))
+```
+
+## Lists [`std/List`](/std/List.bruijn.html)
+
+Lists are a repeated composition (right-associative) of pairs with a
+`empty`{.bruijn} ending symbol `[[1]]`{.bruijn}. They can store any
+(heterogeneous) values and are recursively iterable. The call-by-need
+reduction order of bruijn allows lazy evaluation (i.e. infinite lists).
+
+Example:
+
+``` bruijn
+:test (length (take (+3) (repeat (+4)))) ((+3))
+:test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : {}(+4))))))
+:test ((foldr …+… (+0) ((+1) : ((+2) : {}(+3)))) =? (+6)) (true)
+```
+
+## 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/Number/Binary`](/std/Binary.bruijn.html) to interact with them.
+
+Example:
+
+``` bruijn
+:test (lines "abc\ndef") ("abc" : {}"def")
+:test ("ab" =? "ab") (true)
+```
+
+[^1]: [Mogensen, Torben Æ. "An investigation of compact and efficient
+    number representations in the pure lambda calculus." Perspectives of
+    System Informatics: 4th International Andrei Ershov Memorial
+    Conference, PSI 2001 Akademgorodok, Novosibirsk, Russia, July 2--6,
+    2001 Revised Papers 4. Springer Berlin Heidelberg,
+    2001.](https://doi.org/10.1007/3-540-45575-2_20)
diff --git a/docs/wiki_src/coding/examples.md b/docs/wiki_src/coding/examples.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/coding/examples.md
diff --git a/docs/wiki_src/coding/laziness.md b/docs/wiki_src/coding/laziness.md
new file mode 100644
index 0000000..feec480
--- /dev/null
+++ b/docs/wiki_src/coding/laziness.md
@@ -0,0 +1,52 @@
+# Laziness
+
+Due to the call-by-need reduction order of bruijn, several operations
+are lazily evaluated (automagically!).
+
+## Infinite lists
+
+You can use infinite list generators like `repeat`{.bruijn} or
+`iterate`{.bruijn} to lazily interact with list elements.
+
+``` bruijn
+:import std/List .
+
+:test (length (take (+3) (repeat (+4)))) ((+3))
+:test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : {}(+4))))))
+```
+
+## Math
+
+``` bruijn
+# power function
+:test ((iterate (…⋅… (+2)) (+1)) !! (+3)) ((+8))
+
+# prime numbers
+primes nub ((…≠?… (+1)) ∘∘ gcd) (iterate ++‣ (+2)) ⧗ (List Number)
+
+:test (take (+4) primes) ((+2) : ((+3) : ((+5) : {}(+7))))
+
+# fibonacci
+fibs head <$> (iterate [~0 : (^0 + ~0)] ((+0) : (+1))) ⧗ (List Number)
+
+:test (take (+4) primes) ((+0) : ((+1) : ((+1) : {}(+2))))
+```
+
+## Optimization
+
+Laziness can (in some cases) produce huge performance boosts. For
+example:
+
+``` bruijn
+# 11 seconds
+:time (+10) ** (+500)
+
+# 0.1 seconds
+: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}).
diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md
new file mode 100644
index 0000000..44f5ea2
--- /dev/null
+++ b/docs/wiki_src/coding/meta-programming.md
@@ -0,0 +1,72 @@
+# Meta programming
+
+TODO: more (blog)
+
+Bruijn has a homoiconic meta encoding similar to Lisp's quoting feature.
+
+Blog post with more details: [Homoiconic self interpretation of lambda
+calculus](https://text.marvinborner.de/2023-09-03-21.html).
+
+## Encoding
+
+``` bruijn
+`X     ⤳ [[[2 (+Xu)]]]
+`(M N) ⤳ [[[1 `M `N]]]
+`[M]   ⤳ [[[0 `M]]]
+```
+
+Any quoted term gets converted to this encoding:
+
+``` bruijn
+# example quotations
+:test (`0) ([[[2 (+0u)]]])
+:test (`[0]) ([[[0 [[[2 (+0u)]]]]]])
+:test (`'0') ([[[0 [[[0 [[[0 [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[2 (+2u)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])
+
+# quotes are nestable!
+:test (``0) ([[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]])
+:test (`[0 `0]) ([[[0 [[[1 [[[2 (+0u)]]] [[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]]]]]]]])
+```
+
+## Quasiquotation
+
+Quoted terms can be escaped (*unquoted*) using the comma symbol.
+Unquoted terms will be fully evaluated first before getting quoted
+again.
+
+``` bruijn
+:test (```,[0]) (``[0])
+:test (`,`,[0]) ([0])
+:test (`[0 `,[0]]) (`[0 [0]])
+```
+
+Unquoted De Bruijn indices will get bound to the respective abstraction
+outside of its meta encoding.
+
+``` bruijn
+# adds two using normal quotation
+add-two `[0 + (+2u)]
+
+:test (!add-two (+2u)) ((+4u))
+
+# adds two using a reaching De Bruijn index
+add-two* [`(,0 + (+2u))]
+
+:test (!(add-two* (+2u))) ((+4u))
+```
+
+## Meta library [`std/Meta`](/std/Meta.bruijn.html)
+
+The meta library enables simple interaction with the meta encoding.
+
+Examples:
+
+``` bruijn
+# testing equivalence
+:test (α-eq? `[0 0] `[0 0]) (true)
+:test (α-eq? `α-eq? `α-eq?) (true)
+
+# BLC length of meta term
+:test (length `[0]) ((+4u))
+:test (length `[[1 1]]) ((+12u))
+```
diff --git a/docs/wiki_src/coding/mixfix.md b/docs/wiki_src/coding/mixfix.md
new file mode 100644
index 0000000..c85b936
--- /dev/null
+++ b/docs/wiki_src/coding/mixfix.md
@@ -0,0 +1,33 @@
+# 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).
+
+Example:
+
+``` bruijn
+…+… add
+
+# the "holes" get applied in normal order
+:test ((+4) + (+3)) (add (+4) (+3))
+```
+
+You can define as many holes as you like. Make sure to place parenthesis
+for applications inside substitution holes.
+
+``` bruijn
+{…<$>…|… [[[2 - 1 + 0]]]
+
+# evaluated as (5 - 2) + 1 = 4
+:test ({ (+5) <$> (+2) | (+1)) ((+4))
+:test ({ ((+3) + (+1)) <$> (+2) | (+1)) ((+4))
+```
+
+You can use them as normal functions by writing the identifier
+literally:
+
+``` bruijn
+:test (…+… (+4) (+3)) (add (+4) (+3))
+```
diff --git a/docs/wiki_src/coding/performance.md b/docs/wiki_src/coding/performance.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/coding/performance.md
diff --git a/docs/wiki_src/coding/prefix.md b/docs/wiki_src/coding/prefix.md
new file mode 100644
index 0000000..589e081
--- /dev/null
+++ b/docs/wiki_src/coding/prefix.md
@@ -0,0 +1,25 @@
+# Prefix
+
+Prefix functions are symbols written directly in front of another term
+(without space). The term gets applied as an argument to the prefix
+function. Use [mixfix functions](mixfix.md) if the function has more
+than one argument.
+
+They are defined by the `‣`{.bruijn} suffix.
+
+Example:
+
+``` bruijn
+# defines a negation prefix function called '-'
+-‣ [(+0) - 0]
+
+# returns 0 - 10 = -10
+:test (-(+10)) ((-10))
+```
+
+You can use them as normal functions by writing the identifier
+literally:
+
+``` bruijn
+:test (-‣ (+10)) ((-10))
+```
diff --git a/docs/wiki_src/coding/recursion.md b/docs/wiki_src/coding/recursion.md
new file mode 100644
index 0000000..68148e5
--- /dev/null
+++ b/docs/wiki_src/coding/recursion.md
@@ -0,0 +1,78 @@
+# Recursion
+
+Just as normal lambda calculus, bruijn does *not* support typical
+recursion.
+
+If you want to recursively call a function (or imitate `for`/`while`
+loops), you need to use *fixed-point combinators* like `y`{.bruijn} from
+[`std/Combinator`](/std/Combinator.bruijn.html).
+
+Fixed-point combinators have the fascinating property of inducing
+recursive behaviour in programming languages without support for
+recursion.
+
+Say we want a function `g`{.bruijn} to be able to call itself. With the
+`y`{.bruijn} combinator the following equivalence is obtained:
+
+``` bruijn
+  (y g)
+⤳ [[1 (0 0)] [1 (0 0)]] g
+⤳ [g (0 0)] [g (0 0)]
+⤳ g ([g (0 0)] [g (0 0)])
+≡ g (y g)
+```
+
+With this equivalence, `g`{.bruijn} is able to call itself since its
+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)
+# `0` is the accumulator (the argument of `factorial`)
+g [[=?0 (+1) (0 ⋅ (1 --0))]]
+
+factorial y g ⧗ Number → Number
+
+:test ((factorial (+3)) =? (+6)) (true)
+```
+
+In-the-wild, this could look like this.
+
+``` bruijn
+# 3 abstractions => two arguments
+# 2 is recursive call
+# 1 is accumulator (+0)
+# 0 is argument (list)
+length z [[[rec]]] (+0) ⧗ (List a) → Number
+    rec 0 [[[case-inc]]] case-end
+        case-inc 5 ++4 1
+        case-end 1
+```
+
+Also see [coding style](style.md) for other style suggestions.
+
+## Mutual recurrence relations
+
+For solving mutual recurrence relations, you can use the *variadic
+fixed-point combinator* `y*`{.bruijn} from
+[`std/List`](/std/List.bruijn.html). This combinator produces all the
+fixed points of a function as an iterable [list](data-structures.md).
+
+Example `even?`{.bruijn}/`odd?`{.bruijn} implementation using
+`y*`{.bruijn}:
+
+``` bruijn
+# the odd? recursive call will be the second argument (1)
+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
+
+odd? tail (y* g h) ⧗ Number → Bool
+```
+
+Read more about this in the blog post [Variadic fixed-point
+combinators](https://text.marvinborner.de/2023-06-18-15.html).
diff --git a/docs/wiki_src/coding/style.md b/docs/wiki_src/coding/style.md
new file mode 100644
index 0000000..d0ec7a9
--- /dev/null
+++ b/docs/wiki_src/coding/style.md
@@ -0,0 +1,36 @@
+# Coding style
+
+## Scoping
+
+## If/else
+
+redundant
+
+## Head/tail
+
+redundant
+
+## Type signatures
+
+## Recursion
+
+[Recursion](recursion.md) should almost always be achieved with the
+`y`{.bruijn} or `z`{.bruijn} combinators.
+
+A common coding style in bruijn's standard library is to use the scoped
+`rec` function to indicate recursion. You would then use `n+1`
+abstraction around `rec` to indicate `n` arguments and the additionally
+induced recursive call.
+
+Example of the `length`{.bruijn} function for lists:
+
+``` bruijn
+# 3 abstractions => two arguments
+# 2 is recursive call
+# 1 is accumulator (+0)
+# 0 is argument (list)
+length z [[[rec]]] (+0) ⧗ (List a) → Number
+    rec 0 [[[case-inc]]] case-end
+        case-inc 5 ++4 1
+        case-end 1
+```
diff --git a/docs/wiki_src/coding/test-driven-development.md b/docs/wiki_src/coding/test-driven-development.md
new file mode 100644
index 0000000..f62c448
--- /dev/null
+++ b/docs/wiki_src/coding/test-driven-development.md
@@ -0,0 +1,42 @@
+# Test driven development (TDD)
+
+The suggested technique for bruijn development is the TDD method. When
+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
+```
+
+-   Write several tests including all 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))
+```
+
+-   Finish the implementation until all tests pass (e.g. using the
+    [`:watch`{.bruijn} repl command](REPL.md#watch))
+-   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))
+```
diff --git a/docs/wiki_src/coding/typing.md b/docs/wiki_src/coding/typing.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/coding/typing.md
diff --git a/docs/wiki_src/coding/uniform-function-call-syntax.md b/docs/wiki_src/coding/uniform-function-call-syntax.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/coding/uniform-function-call-syntax.md
diff --git a/docs/wiki_src/custom.css b/docs/wiki_src/custom.css
new file mode 100644
index 0000000..fdcea31
--- /dev/null
+++ b/docs/wiki_src/custom.css
@@ -0,0 +1,56 @@
+.headerlink {
+	display: none;
+}
+
+h2,h3,h4,h5,h6 {
+	line-height: var(--global-line-height);
+	margin-bottom: 0.5em;
+}
+
+.terminal h1 {
+    font-size: 2.33em;
+}
+
+.terminal h1 > * {
+	font-size: inherit;
+}
+
+.terminal h2 {
+    font-size: 1.83em;
+}
+
+.terminal h2 > * {
+	font-size: inherit;
+}
+
+.terminal h3{
+    font-size: 1.50em;
+}
+
+.terminal h3 > * {
+	font-size: inherit;
+}
+
+.terminal h4 {
+    font-size: 1.33em;
+}
+
+.terminal h4 > * {
+	font-size: inherit;
+}
+
+.terminal h5 {
+    font-size: 1.16em;
+}
+
+.terminal h5 > * {
+	font-size: inherit;
+}
+
+.terminal h6 {
+    font-size: 1em;
+}
+
+.terminal h6 > * {
+	font-size: inherit;
+}
diff --git a/docs/wiki_src/index.md b/docs/wiki_src/index.md
new file mode 100644
index 0000000..3049322
--- /dev/null
+++ b/docs/wiki_src/index.md
@@ -0,0 +1,6 @@
+# Bruijn wiki
+
+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.
diff --git a/docs/wiki_src/introduction/installation.md b/docs/wiki_src/introduction/installation.md
new file mode 100644
index 0000000..3334ad3
--- /dev/null
+++ b/docs/wiki_src/introduction/installation.md
@@ -0,0 +1,24 @@
+# Installation
+
+You first need to install Haskell's
+[Stack](https://docs.haskellstack.org/en/stable/) using their official
+instructions for your operating system. After that, clone the bruijn
+repository using
+
+``` bash
+$ git clone https://github.com/marvinborner/bruijn
+$ cd bruijn
+```
+
+Then, run bruijn using `stack run`{.bash}. This starts bruijn's
+[REPL](../coding/REPL.md). You can now play around with bruijn.
+
+Passing normal arguments to `bruijn`{.bash} with `stack`{.bash} can be
+done with `stack run -- [args]`. If you enjoy it, you can install
+`bruijn` into your stack path using `stack install`.
+
+------------------------------------------------------------------------
+
+Please create an issue on
+[GitHub](https://github.com/marvinborner/bruijn/issues/new) if you
+encounter any issues.
diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md
new file mode 100644
index 0000000..59a7c59
--- /dev/null
+++ b/docs/wiki_src/introduction/lambda-calculus.md
@@ -0,0 +1,76 @@
+# Lambda calculus
+
+Bruijn is based on De Bruijn indexed lambda calculus.
+
+## Traditional lambda calculus
+
+Lambda calculus basically has three types of expressions:
+
+-   *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.
+-   *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.
+
+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.
+
+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)`).
+
+## De Bruijn indices
+
+Programs written in lambda calculus often have many abstractions and
+therefore at least as many variables. I hate naming variables,
+especially if you need hundreds of them for small programs. With that
+many variables it's also really complicated to compare two expressions,
+since you first need to resolve shadowed and conflicting variables
+("α-conversion").
+
+De Bruijn replace the concept of variables by using numeric references
+to the abstraction layer. Let me explain using an example: The
+expression `λx.x` becomes `λ0` -- the `0` refers to the first parameter
+of the abstraction. Subsequently, the expression `λx.λy.x y` becomes
+`λλ1 0`{.bruijn}. Basically, if you're reading from left to right
+starting at the abstraction you want to bind, you increment on every
+occurring `λ` until you arrive at the index.
+
+While confusing at first, programs written with De Bruijn indices can
+actually be way easier to understand than the equivalent program with
+named variables.
+
+## Bruijn's bracketing
+
+Bruijn's final syntactic variation from lambda calculus is the use of
+square brackets instead of lambda symbols. By putting the entire
+abstracted term in brackets, it's much clearer where indices and the
+respective terms are bound to.
+
+Representing `λλ1 0` in bruijn's syntax then becomes `[[1 0]]`{.bruijn}.
+The application of `λ0` and `λλ1 0` becomes `[0] [[1 0]]`{.bruijn}.
+
+------------------------------------------------------------------------
+
+Random example reductions:
+
+``` bruijn
+[0] [[1]]       ⤳ [[1]]
+[[0]] [[1]]     ⤳ [0]
+[[1]] [[1]]     ⤳ [[[1]]]
+[[0]] [0] [[1]] ⤳ [[1]]
+[[0 1]] [0]     ⤳ [0 [0]]
+[[1 0]] [0]     ⤳ [0]
+```
diff --git a/docs/wiki_src/introduction/setup.md b/docs/wiki_src/introduction/setup.md
new file mode 100644
index 0000000..92f9886
--- /dev/null
+++ b/docs/wiki_src/introduction/setup.md
@@ -0,0 +1,6 @@
+# Setup
+
+-   unicode keymap
+-   editors
+-   syntax highlighting
+-   broogle
diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md
new file mode 100644
index 0000000..55e2c21
--- /dev/null
+++ b/docs/wiki_src/introduction/syntax.md
@@ -0,0 +1,148 @@
+# Syntax
+
+Bruijn has an arguably weird syntax, although it's not strictly meant as
+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).
+
+## Definitions
+
+Bruijn works by defining named substitution rules, where each usage of
+the identifier will get substituted respectively.
+
+Since there's no other major syntactic block, bruijn omits the equal
+symbol for definitions.
+
+For example:
+
+``` bruijn
+# define `id` as [0]
+id [0]
+
+# [0] [0] ⤳ [0]
+still-id id id
+
+# `main` is now [0]
+main still-id
+```
+
+Note that this does *not* actually extend the functionality of lambda
+calculus. These identifiers are static constants and can't be
+dynamically changed.
+
+In fact, bruijn's interpreter works by producing *one* final huge lambda
+calculus expression for any given program, that then gets reduced by a
+normal lambda calculus reducer.
+
+## Open terms
+
+If you use De Bruijn indices that reach out of their environment, you
+have created an *open term*. Depending on the context, these terms are
+typically seen as invalid if standing by themself.
+
+``` bruijn
+# open terms
+open0 0
+open1 [[2]]
+open2 [[0 1] 1]
+
+# closed terms
+closed0 [0 [1]]
+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
+suggestions](../coding/style.md)).
+
+## Imports
+
+Files can either be imported into a namespace (capital word) or the
+current environment (.):
+
+``` bruijn
+:import std/Pair P
+:import std/Logic .
+
+main [P.pair true false]
+```
+
+All paths get the `.bruijn` extension appended automatically.
+
+Only top-level definitions get imported using `:import`{.bruijn}. If you
+also want to import second-level definitions (for example imported
+definitions from the imported file), you can use `:input`{.bruijn}.
+
+``` bruijn
+:input std/Math
+```
+
+## Tests
+
+Tests compare the *normal form* of two expressions. Note that the
+parentheses around the two terms are always mandatory.
+
+``` bruijn
+:test ([0] [[1]]) ([[1]] [[1]] [0])
+```
+
+Execution succeeds silently. Example of failing test:
+
+``` bruijn
+:test ([0] [[1]]) ([[1]] [0])
+```
+
+After running:
+
+    ERROR test failed: ([0] [[1]]) = ([[1]] [0])
+          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.
+
+## Scoping
+
+Indented lines (by tab) act as a `where` statement for the less indented
+lines.
+
+``` bruijn
+foo [[0]]
+
+bar [0] foo
+    foo bar
+        bar [[1]]
+
+# foo is still `[[0]]`
+# bar is `[0] [[1]]`
+main [[0 foo bar]]
+```
+
+Also note that bruijn does *not* support recursion -- you wouldn't be
+able to use `bar`{.bruijn} in `foo`{.bruijn} without its sub definition.
+See [recursion](../coding/recursion.md) to learn how to use recursion
+anyway.
+
+## Syntactic sugar
+
+Some typical data encodings are provided as syntactic sugar. You can
+learn more about the internal specifics in [data
+structures](../coding/data-structures.md).
+
+-   *Numbers*: `(SXB)`{.bruijn} where `S` is `+`/`-`, `X` is a number
+    and `B` is the *base* of the encoded number (or `t` by default)
+    -   `u` for unary base (postive, Church): `(+42u)`
+    -   `b` for binary base (positive): `(+42b)`
+    -   `t` for balanced ternary (positive/negative): `(-42t)`
+-   *Characters*: `'C'`{.bruijn} where `C` is any ASCII character
+-   *Strings*: `"X1..XN"`{.bruijn} where `X1...XN` are any ASCII
+    characters
+-   *Quotes*: `` `T ``{.briujn} where `T` is any lambda term ([meta
+    programming](../coding/meta-programming.md))
+
+## Types
+
+TODO.
diff --git a/docs/wiki_src/technical/arithmetic.md b/docs/wiki_src/technical/arithmetic.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/technical/arithmetic.md
diff --git a/docs/wiki_src/technical/reduction.md b/docs/wiki_src/technical/reduction.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/wiki_src/technical/reduction.md
author	Marvin Borner	2023-11-06 00:24:11 +0100
committer	Marvin Borner	2023-11-06 00:24:31 +0100
commit	9d722a0b6138827de743f9fe4acbf3f2c1830bb0 (patch)
tree	789b8df72f0f2cae2bb4009ddb93b914bf83eb2c /docs
parent	027fc0f91ae7bf64564091fbcec7694f5d53d8fe (diff)