1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
# 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). 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. 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.
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 improved 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 and you're sure your code is correct, you can enable
the *YOLO* mode to disable tests 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)`{.bruijn}
- `b` for binary base (positive): `(+42b)`{.bruijn}
- `t` for balanced ternary (positive/negative): `(-42t)`{.bruijn}
- *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
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
```
|
