Skip to content

Commit

Permalink
Minor documentation fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@marvinborner
marvinborner committed Dec 15, 2023
1 parent b572418 commit d22c013
Show file tree
Hide file tree
Showing 14 changed files with 246 additions and 135 deletions.
2 changes: 1 addition & 1 deletion docs/code.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ const term = (t) =>
.replaceAll(/(\))(?!\<)/g, "<span class='right-app'>)</span>")
.replaceAll("[", "<span class='left-abs'>[</span>")
.replaceAll("]", "<span class='right-abs'>]</span>")
.replaceAll(/(?<![+-\d])([0-9])/g, "<span class='index'>$1</span>");
.replaceAll(/(?<!\([+-]\d*)([0-9])/g, "<span class='index'>$1</span>");

const highlightTerm = (elem) => {
elem.innerHTML = term(elem.innerHTML);
Expand Down
254 changes: 154 additions & 100 deletions docs/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,134 +1,188 @@
<!DOCTYPE html>
<!doctype html>
<html>
<head>
<meta charset="UTF-8" />
<meta name="viewport" content="width=device-width" />
<meta name="description" content="Functional programming language based on pure bruijn-indexed lambda calculus." />
<link rel="stylesheet" href="style.css" type="text/css" media="all">
<title>bruijn programming language</title>
</head>
<body>
<div class="header">
<img src="res/logo.png" />
<h1>bruijn</h1>
</div>

<div class="example">
<pre class="code">
<span class="def">pow</span> <span class="term">[<span class="symbol">…!!…</span> (<span class="symbol">iterate</span> (<span class="symbol">…⋅…</span> 0) <span class="ternary">(+1)</span>)]</span>
<head>
<meta charset="UTF-8" />
<meta name="viewport" content="width=device-width" />
<meta
name="description"
content="Functional programming language based on pure De Bruijn indexed lambda calculus."
/>
<link rel="stylesheet" href="style.css" type="text/css" media="all" />
<title>bruijn programming language</title>
</head>
<body>
<div class="header">
<img src="res/logo.png" />
<h1>bruijn</h1>
</div>

<div class="example">
<div class="left">
<pre class="code">
<span class="def">pow</span> <span class="term">[<span class="symbol">index</span> (<span class="symbol">iterate</span> (<span class="symbol">mul</span> 0) <span class="ternary">(+1)</span>)]</span>

<span class="def">…**…</span> <span class="symbol">pow</span>

<span class="com">:test</span> <span class="test">(<span class="term"><span class="ternary">(+2)</span> <span class="mixfix">**</span> <span class="ternary">(+3)</span> <span class="mixfix">=?</span> <span class="ternary">(+8)</span></span>)</span> <span class="test">(<span class="symbol">true</span>)</span></pre>

<p>
Functional language based on pure bruijn-indexed lambda calculus.
</p>
</div>

<div class="bar small">
<b>Hint</b>: Click on anything you don't understand.
</div>

<div class="example">
<p>
Lambdas all the way down.<br>
No primitive functions.
</p>
<pre class="code">
</div>

<div class="right">
<p>
Functional programming language based on pure De Bruijn indexed lambda
calculus.
</p>
</div>
</div>

<div class="bar small">
<b>Hint</b>: Click on anything you don't understand.
</div>

<div class="example">
<div class="left">
<p>
Lambdas all the way down.<br />
No primitive functions.
</p>
</div>
<div class="right">
<pre class="code">
<span class="repl">></span> <span class="ternary">(+5)</span>
<span class="term">[[[[2 (2 (1 3))]]]]</span>
<span class="repl">></span> <span class="char">'a'</span>
<span class="term">[[[1 (0 (0 (0 (0 (1 (1 (0 2)))))))]]]</span>
<span class="repl">></span> <span class="symbol">add</span>
<span class="term">[[(([([[1 0 [[0]]]] ((((0 [[(((0...</span></pre>
</div>
</div>

<div class="example">
<pre class="code">
<div class="left">
<pre class="code">
<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+30)</span>
<span class="time">0.15 seconds</span></pre>
<p>
Efficient call-by-need reduction using abstract machines.
</p>
</div>

<div class="example">
<p>
Substantial standard library.<br>
<a href="std/">Source</a>
</p>
<pre class="code">
</div>
<div class="right">
<p>Efficient call-by-need reduction using abstract machines.</p>
</div>

<div class="left">
<p>
Substantial standard library.<br />
<a href="std/">Source</a>
</p>
</div>
<div class="right">
<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>
<span class="repl">></span> <span class="symbol">number!</span> <span class="mixfix"><$></span> <span class="left-app">(</span><span class="symbol">lines</span> <span class="string">"42\n25"</span><span class="right-app">)</span>
<span class="repl">></span> <span class="term"><span class="symbol">sum</span> (<span class="symbol">take</span> <span class="ternary">(+3)</span> (<span class="symbol">repeat</span> <span class="ternary">(+4)</span>))</span>
<span class="repl">></span> <span class="binary">(+10b)</span> <span class="mixfix">⋀!</span> <span class="binary">(+12b)</span></pre>
</div>
</div>

<div class="example">
<pre class="code">
<div class="left">
<pre class="code">
$ echo "main [0]" > echo.bruijn
$ bruijn -b echo.bruijn > echo
$ wc -c echo
2 echo
$ echo "hello world!" | bruijn -e echo
hello world!</pre>
<p>
Compilation to Tromp's binary lambda calculus.<br>
Support for byte and ASCII encoding.
</p>
</div>

<div class="bar big">
Learn more: <a href="wiki/">Wiki</a>, <a href="std/">Std</a>
</div>

<div class="instructions">
<h1>Installation</h1>
<pre class="code">
hello world!</pre
>
</div>
<div class="right">
<p>
Compilation to Tromp's binary lambda calculus.<br />
Support for byte and ASCII encoding.
</p>
</div>
</div>

<div class="bar big">
Learn more: <a href="wiki/">Wiki</a>, <a href="std/">Std</a>
</div>

<div class="instructions">
<h1>Installation</h1>
<pre class="code">
$ git clone https://github.com/marvinborner/bruijn.git && cd bruijn
$ <span class="stack">stack</span> run # for playing around
$ <span class="stack">stack</span> install
$ bruijn</pre>
</div>
$ bruijn</pre>
</div>

<div class="instructions">
<h1>Broogle</h1>
<pre class="code">
<div class="instructions">
<h1>Broogle</h1>
<pre class="code">
$ ./broogle.sh -f add
<span class="def">add</span> ⧗ Unary → Unary → Unary
also known as <span class="def">…+…</span>
in std/Number/Unary.bruijn:35
# adds two unary numbers
...</pre>
</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>
<li>Exploring different encodings of data as function abstractions is fascinating.</li>
<li>Pure lambda calculus can be very beautiful. You will understand if you try to have some fun with it.</li>
<li>I don't like naming parameters of functions. Using bruijn indices is a universal reference independent of the function and can actually help readability if you're familiar enough.</li>
<li>Really, <a href="https://justforfunnoreally.dev/">just for fun</a>.</li>
</ul>
</div>

<div class="instructions">
<h1>Articles</h1>
<ul>
<!-- 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">
Open-source: <a href="https://github.com/marvinborner/bruijn">GitHub</a>
</div>

<script src="script.js" charset="utf-8"></script>
</body>
...</pre>
</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>
<li>
Exploring different encodings of data as function abstractions is
fascinating.
</li>
<li>
Pure lambda calculus can be very beautiful. You will understand if you
try to have some fun with it.
</li>
<li>
The use of De Bruijn indices creates a clear distinction between
references to arguments and references to identifiers/functions.
</li>
<li>
I don't like naming parameters of functions. De Bruijn indices are a
universal reference independent of the function and can actually help
readability if you're familiar enough.
</li>
<li>
Really, <a href="https://justforfunnoreally.dev/">just for fun</a>.
</li>
</ul>
</div>

<div class="instructions">
<h1>Articles</h1>
<ul>
<!-- 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"
>Metaprogramming and self interpretation</a
>
</li>
</ul>
</div>

<div class="bar big">
Open-source: <a href="https://github.com/marvinborner/bruijn">GitHub</a>
</div>

<script src="script.js" charset="utf-8"></script>
</body>
</html>
8 changes: 4 additions & 4 deletions docs/script.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,12 @@ const describe = (c, d) => {
[...document.getElementsByClassName(c)].forEach(el => el.addEventListener("click", e => notify(d, e)));
}

describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices");
describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices");
describe("char", "Syntactic sugar for a binary representation of characters using abstractions as data.");
describe("com", "This indicates a command to the interpreter. The most common commands are :test (verifying α-equivalency) and :import (importing definitions from other files).");
describe("def", "This defines a new term substitution.");
describe("def", "This defines a new term substitution. Using this identifier will substitute the term on its right side.");
describe("header", "[0] is the identity operation. It returns the first argument it gets. Nothing more.");
describe("index", "These numbers reference the nth abstraction, starting counting from the inside. These 'bruijn indices' replace the concept of variables in lambda calculus.");
describe("index", "This number references the nth abstraction, starting counting from the inside. These 'De Bruijn indices' replace the concept of variables in lambda calculus.");
describe("left-abs", "The opening bracket of a function abstraction. It's basically the equivalent of the λ in lambda calculus.");
describe("left-app", "The opening bracket of a function application.");
describe("mixfix", "This is a mixfix operator. They can be defined like …*… where the … can then be any other term. You can use them without the … as a notation of function application.");
Expand All @@ -44,7 +44,7 @@ describe("right-app", "The closing bracket of a function application.");
describe("stack", "Stack is a dependency manager for Haskell. Install it using the corresponding instructions for your operating system.")
describe("string", "Syntactic sugar for a list of binary encoded chars.")
describe("symbol", "This substitutes a previously defined term (for example from the standard library).");
describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices.");
describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices.");
describe("time", "Incredibly fast for lambda calculus standards.");

document.body.addEventListener("click", clearPopups, true)
Loading

0 comments on commit d22c013

Please sign in to comment.