The bruijn Programming Language

The bruijn programming language is basically pure lambda calculus with a sprinkle of syntactic sugar. It has no side effects, just monadic input and output. It doesn’t even have any primitive functions like arithmetic operations.

Well, what can the language do, then? And how can this be even remotely performant?

Lambda calculus

To explain the basic concepts of the programming language, let me first remind you of the rules of the lambda calculus. It basically has three types of expressions:

Not too complicated, right? 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. 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.

De Bruijn

Expressions in lambda calculus can get really big. Writing “real-world” functions in pure lambda calculus results in a big mess of variable names. Due to the fact that there’s no strict rule on shadowing variables, inferring the binding of identifiers is not always trivial. Especially if we want to write an algorithm that compares two expressions, we first need to convert the identifiers within both expressions to some kind of standardised format before we can compare it (“alpha conversion”). This sucks.

You could solve this by just not repeating/shadowing variables. Unfortunately this is really bad for usability and readability – as I said, expressions can get really big.

Luckily, there’s a solution: De Bruijn indices. They replace the concept of identifiers 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.

Interestingly enough, the more I’ve worked with De Bruijn indices, the more comfortable I felt with coding using them directly. So much so, that I’ve decided to name the language after De Bruijn himself. Thinking about “variables” in terms of abstraction layer depth has helpful consequences for functional thinking and makes techniques like currying much more enjoyable.

Bracketing

I still don’t like this syntax, though. Actually writing multiple expressions after another always needs explicit parentheses to denote the start and end of the abstractions – for example applying λ0 to λλ1 0 results in (λ0)(λλ1 0).

Let me propose a better, more readable syntax: How about explicitly specifying the start and end of all abstractions and therefore eliminating the need for the λ symbol simultaneously? Such start and end symbols should obviously differ from the application notation (round brackets) – so how about using square brackets?¹

Representing λλ1 0 in bruijn’s syntax then becomes [[1 0]]. The application of λ0 and λλ1 0 becomes [0] [[1 0]] – neat!

Syntax

Let’s first have some kind of syntax for defining substitution rules so we can reuse expressions without needing to rewrite them. Bruijn then only evaluates the main expression. Identifiers in bruijn are lower case words, we can therefore just write the name of the identifier and its definition – we don’t even need an equal sign!

id [0]

# [0] [0] ⤳ [0]
still-id id id

# 'main' is now [0]
main still-id

As bruijn has no primitive functions, every operation has to be coded manually. That’s why bruijn has a comprehensive standard library, implementing many of the default operations for numbers/bytes/strings. Keep in mind that the standard library is obviously still raw bruijn code though.

Imports

Files can either be imported into a namespace (capital word) or the current environment (.):

:import std/Pair P
:import std/Logic .

main [P.pair true false]

Only top-level definitions get imported using :import. If you also want to import second-level definitions (for example imported definitions from the other file), you can use :input.

foo [[0]]

bar [0] foo
    foo [[1]]

# foo is still '[[0]]'
# bar is '[0] [[1]]'
main [[0 foo bar]]

The main function always gets called with the program’s argument. If we don’t want to use it, we just don’t refer to it by creating a redundant abstraction!

Sugar

Syntactic sugar provides huge improvements regarding usability and readability: For example, you can encode numbers in lambda calculus using the “Church encoding”. Basically, it’s just a

n

-times repeated application of arguments – therefore encoding data using abstraction references. The church-encoded decimal number

5

is represented as [[1 (1 (1 (1 (1 0))))]]. One can only imagine how long big numbers can get – nobody wants to type that! Instead, bruijn provides the equivalent (+5u), where u denotes the base of the number (in this case, unary).

# balanced ternary numbers (the default base)
(+5) ⤳ (+5t)
(+5t) ⤳ [[[[(2 (2 (1 3)))]]]]

# balanced ternary numbers can even be negative!
(-5) ⤳ [[[[(1 (1 (2 3)))]]]]

# binary numbers
(+5b) ⤳ [[[(1 (0 (1 2)))]]]

# characters (binary-encoded)
'a' ⤳ [[[(1 (0 (0 (0 (0 (1 (1 (0 2))))))))]]]

# strings (characters as list)
"abc" ⤳ [((0 [[[(1 (0 (0 (0 (0 (1 (1 (0 2))))))))]]]) [((0 [[[(0 (1 (0 (0 (0 (1 (1 (0 2))))))))]]]) [((0 [[[(1 (1 (0 (0 (0 (1 (1 (0 2))))))))]]]) [[0]])])])]

I hope it’s obvious why such syntactic sugar is really important for bruijn. If you want to understand the specifics of the internal representation of such syntactic sugar, I highly recommend my article “Data structures in pure lambda calculus”.

Mixfix

An elegant way of making the code more readable is the introduction of so-called mixfixes. Inspired by languages like Agda, we can define mixfix functions using special characters and “substitution holes”:

:import std/Number .

…+… add

# returns 5 + 3 = 8
main [(+5) + (+3)]

# mixfixes get resolved from left to right: ((2 - 1) + 0)
{…<$>…|… [[[2 - 1 + 0]]]

# returns (5 - 2) + 1 = 4
main [{ (+5) <$> (+2) | (+1)]

You can also define prefix functions. They are similar to mixfix functions, but don’t require spaces between their name and arguments and only allow a single argument:

# defines a negation prefix function called '-'
-‣ [(+0) - 0]

# returns 0 - 10 = -10
main [-(+10)]

Coding

Actually solving problems using bruijn is not always that simple. Especially if you’re not using the already defined functions from the standard library. If you’re interested how basic functions like add or pair are implemented, feel free to browse the open-source code on GitHub or the automatically generated documentation.

Recursion

One of the most important procedures of programming are loops and recursion. Both are not available in pure lambda calculus as well as bruijn, as they would add unnecessary complexity.

Luckily, logicians like Haskell Curry and Alan Turing have found some ways to implement the behaviour of recursion without actually having recursive calls (mind-blown). There are great articles online like this explaining the exact behaviour better than I ever could. So let’s just look at how these so-called “fixed-point combinators” can be implemented in bruijn:

# y combinator (very popular)
y [[1 (0 0)] [1 (0 0)]]

# z combinator
z [[1 [1 1 0]] [1 [1 1 0]]]

# turing combinator
θ [[0 (1 1 0)]] [[0 (1 1 0)]]

Now imagine we want to add the numbers from

1

n

and return the result. The standard library has great functions for such operations already, but let’s try doing this by only using the y combinator, the + mixfix function, the -- prefix function (decrements a number by one), and the =? prefix function (returns true if the number is zero, false otherwise).

First, we look at how languages like Haskell could solve such a problem without using pattern matching:

sum x = if x == 0 then 0 else x + (sum (x - 1))

Representing if conditions in bruijn can be done using the std/Logic library and its if or …?…:… functions. However, one of the neat things about the representation of booleans in bruijn is that we can actually write conditions even simpler:

true [[1]]

false [[0]]

# returns 42 if the argument is true, -42 if false
foo [0 (+42) (-42)]

Okay, so we know that the function should basically be [=?0 (+0) (0 + magic)], where magic is some kind of recursive call. This is where we use the y combinator. Its usage introduces one additional abstraction representing the recursive call:

sum y [[=?0 (+0) (0 + (1 --0))]]

Laziness

One of the greatest features of Haskell (in my opinion) is laziness. You can easily do things like take 3 $ map (*2) [1..] returning [2,4,6]. Haskell supports many different kinds of laziness – I want to focus on the laziness of lists though.

Since bruijn should represent pure lambda calculus as closely as possible, it’s not acceptable to implement some kind of special reduction strategy for lazy evaluation. Instead, bruijn uses the very common call-by-need reduction strategy (specifically, the RKNL abstract machine), which yields automagic laziness for many kinds of terms.

The list representation I’ve chosen for bruijn is quite similar to Lisp-like languages: A list is just a repeated application of pairs. In bruijn, a pair can be defined as [0 (+4) (+2)], constructed by [[[0 2 1]]] (as I said, more information can be found in my article “Data structures in pure lambda calculus”).

Constructing infinite lists can then easily be done using the y combinator. For example:

# uses the y combinator and the pair constructor ':'
iterate y [[[0 : (2 1 (1 0))]]]

Using this, (iterate ++‣ (+0)) results in ((+0) : ((+1) : ((+2) : ((+3) : .... Now to the amazing part: Writing a take and map function, while being especially careful regarding reduction order, results in the following code:

:import std/List .
:import std/Number .

# equivalent of Haskell's `take 3 $ map (*2) [1..]`
foo take (+3) (map (mul (+2)) (iterate ++‣ (+1)))

Several functions in std/List like {…|…} make such lazy operations even easier.

Currying

Lambda calculus naturally supports currying – that is, only partially applying a function. In bruijn, currying (or schönfinkeling, to be historically accurate) is therefore a great way to make functions even more elegant.

As a matter of fact, we used currying in the previous examples: (mul (+2)) is the partially applied multiplication function – the fully expanded form would be [mul (+2) 0].

However, you need to be careful: Some functions don’t want to reduce into a normal form if they’re not given enough arguments. For example, just writing add without any arguments results in an infinite loop due to its pseudo-recursive behaviour.

I/O

As originally proposed by John Tromp in their legendary algorithmic information theory paper, bruijn supports “monadic” I/O by calling the main function with a lazy list of input bytes. Monadic because the bytes can then be read/written using typical monadic operations like bind/return (see std/Monad for more). The resulting reduced expression then represents the output!

Aside from that, the input can obviously also be interpreted as a raw linked list using the std/List library:

:import std/List .

# reverse the input list
main [<~>0]

Typing

If you already looked at the standard library, you might have realised that bruijn seems to support type annotations.

While full type-checking is planned for the future (low priority, to be honest), the current implementation purely aids the searchability and readability of functions. The only check currently applied to type annotations is a basic syntax check.

They’re still useful for at least one thing: Similarly to Haskell’s search engine Hoogle, the Broogle script enables you to search functions by type, name or comment:

./broogle.sh -t "a -> a"
./broogle.sh -f "i"
./broogle.sh -c "idiot combinator"

Tools

A very important part of bruijn I didn’t mention yet is its development style. Originally inspired by Racket, using the :test (...) (...) command enables rapid trial-and-error using test driven development (TDD). It also serves as continuous performance and correctness testing, as tests in libraries get executed on every import automatically.

Another great development tool of bruijn is its REPL. You can evaluate expressions directly instead of needing to write a main function everytime. Therefore we do actually need an = sign between an identifier and its definition. Other than that it works just like any other REPL but with several cool features.

You can use :watch <path> to watch and re-test a file on every save, :time <exp> to measure the reduction time of an expression, :blc <exp> to view the compiled version of the unreduced and reduced expressions, or :length <exp> to see the length of the corresponding compiled code.

Compilation

Bruijn can be compiled to John Tromp’s binary lambda calculus (BLC). The bruijn executable supports reading and writing of bit-wise as well as ASCII encodings of BLC. The resulting executables can be remarkably small, in many cases also remarkably big.

Using an expression multiple times just repeats the expressions in the compiled BLC. This clearly results in huge redundancy – therefore I have plans to implement an optimizer/compressor that combines duplicate expressions.

Performance

It’s obvious that a language based on pure lambda calculus without using primitive functions can’t be fast – that is, in comparison with other functional languages.

However, it’s probably not as slow as you think. Especially optimized functions are very performant. For example, bruijn uses the results of an investigation by Torben Mogensen to implement very efficient operations on balanced ternary numbers.

We can use the :time command in bruijn’s REPL to get some performance statistics:

# calculates 2^142 (big)
# > 0.49 seconds
:time (iterate (mul (+2)) (+1)) !! (+100)

# calculates 42! (huge)
# > 0.58 seconds
:time [∏ (+1) → 0 | i] (+42)

Bruijn uses the RKNL abstract machine to implement a “call-by-need” reduction strategy. This results in very fast reduction times while keeping the memory usage comparatively low. Bruijn also utilizes Haskell’s optimizations regarding laziness and multi-threading.

Other functions like string/binary/unary operations are quite slow though. Many performance improvements are still needed – feel free to contribute!

Improvements

Comparing bruijn’s RKNL implementation with the reference data from the paper, I’ve realized some weird complexity deviation: Reducing expressions of the family [(+Nu) [0 0] 0], where N is an arbitrary integer, should consume

\mathcal{O}(N)

memory and time. However, the memory and time complexity is more like

\mathcal{O}(2^N)

– huh!

I’ve tried analyzing the Haskell code and there seems to be an issue with the way we use hashmaps. As this article explains, strict hashmaps in Haskell are not really strict. The memory “space leak” could therefore be a result of redundantly copying data in the reducer. The change in time complexity would then mainly be the result of redundant garbage collection. The reason could also very well be something else – I’m still investigating!

Space leaks in general are very common in bruijn – especially noticeable in its REPL. As debugging them is very annoying, I’ve actually tried writing the reducer in C here but its performance is even worse (although I have plans for it, so I’ll probably optimize it soon).

Why?

The language is slow, the syntax is hard, and coding in bruijn can make you quite angry – so why would anyone ever want to use it?

To be honest, I don’t completely know the answer. I can’t really explain why but, in the end, it’s actually really enjoyable playing around with the language. Finally getting something to work is really fulfilling and almost always elegantly beautiful.

I mean, it’s obvious that De Bruijn indices were never intended as a human-readable replacement for variables. But it’s still fun.

I hope I sparked your interest in bruijn or (at least) lambda calculus and functional programming in general.

Feel free to contribute on GitHub. For example, many improvements can be made regarding performance of the standard library and reduction strategies (start by grepping TODO).

If you want to learn more about bruijn or lambda calculus, I highly suggest visiting the following pages: