15 files changed, 384 insertions, 49 deletions

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))
+```