diff options
| -rw-r--r-- | docs/code.js | 2 | ||||
| -rw-r--r-- | docs/index.html | 254 | ||||
| -rw-r--r-- | docs/script.js | 8 | ||||
| -rw-r--r-- | docs/style.css | 72 | ||||
| -rw-r--r-- | docs/wiki_src/coding/data-structures.md | 4 | ||||
| -rw-r--r-- | docs/wiki_src/coding/mixfix.md | 3 | ||||
| -rw-r--r-- | docs/wiki_src/technical/performance.md | 2 | ||||
| -rw-r--r-- | readme.md | 21 | ||||
| -rw-r--r-- | std/List.bruijn | 4 | ||||
| -rw-r--r-- | std/Math.bruijn | 1 | ||||
| -rw-r--r-- | std/Number.bruijn | 2 | ||||
| -rw-r--r-- | std/Number/Binary.bruijn | 1 | ||||
| -rw-r--r-- | std/Number/Ternary.bruijn | 3 | ||||
| -rw-r--r-- | std/Tree/Rose.bruijn | 4 |
14 files changed, 246 insertions, 135 deletions
diff --git a/docs/code.js b/docs/code.js index 3a2a7bd..0384eca 100644 --- a/docs/code.js +++ b/docs/code.js @@ -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); diff --git a/docs/index.html b/docs/index.html index deb1d92..a66c96c 100644 --- a/docs/index.html +++ b/docs/index.html @@ -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> diff --git a/docs/script.js b/docs/script.js index 21f0cdf..5859c55 100644 --- a/docs/script.js +++ b/docs/script.js @@ -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."); @@ -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) diff --git a/docs/style.css b/docs/style.css index d986c71..1739f58 100644 --- a/docs/style.css +++ b/docs/style.css @@ -34,22 +34,31 @@ a { .example { display: flex; + flex-flow: row wrap; align-items: center; justify-content: center; - flex-flow: row wrap; - column-gap: 5vw; - max-width: 80%; margin: 0 auto; + width: 50%; +} + +.example > * { + display: flex; + flex-basis: 50%; + justify-content: center; +} + +.example .code { + width: fit-content; } .example p { font-size: 1.2em; - max-width: 80vw; + max-width: 80%; text-align: center; } .instructions { - max-width: 80%; + max-width: 70%; margin: 0 auto; } @@ -59,30 +68,54 @@ a { } } -@media(min-width: 768px) { - .example { - flex-flow: row nowrap; - max-width: 80%; +/* mobile */ +@media(max-width: 768px) { + .example > * { + flex-basis: 100%; } - .example p { - width: 30vw; + .example * { + max-width: 90% !important; + } + + .example { font-size: 1.3em; + width: 100% } .instructions { - max-width: 80%; + max-width: 90%; + font-size: 1.1em; } + + .instructions a { + line-height: 1.5em; + } + + .example :nth-child(8) { order: 7; } + .example :nth-child(7) { order: 8; } + .example :nth-child(6) { order: 6; } + .example :nth-child(5) { order: 5; } + .example :nth-child(4) { order: 3; } + .example :nth-child(3) { order: 4; } + .example :nth-child(2) { order: 2; } + .example :nth-child(1) { order: 1; } } -@media(min-width: 1800px) { +/* small desktop / tablet */ +@media(max-width: 1700px) { .example { - flex-flow: row nowrap; - max-width: 45%; + width: 80%; } - .instructions { - max-width: 35%; + .example .code { + font-size: 1em; + } +} + +@media(max-width: 1000px) { + .example { + width: 100%; } } @@ -124,10 +157,7 @@ a { padding: 15px; font-size: 1.2em; border-radius: 10px; -} - -.instructions .code { - overflow-x: scroll; + overflow: scroll; } .code .repl { diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md index 3d2a387..e59fa99 100644 --- a/docs/wiki_src/coding/data-structures.md +++ b/docs/wiki_src/coding/data-structures.md @@ -60,6 +60,10 @@ a-box <>'a' :test (store! a-box 'b') (<>'b') ``` +Options ([`std/Option`](/std/Option.bruijn.html)) use the same data +structure and have additional definitions to resemble Haskell's +`Maybe`{.haskell}. + ## Pairs [`std/Pair`](/std/Pair.bruijn.html) Pairs (tuples) can store any two terms. Pairs can be constructed using diff --git a/docs/wiki_src/coding/mixfix.md b/docs/wiki_src/coding/mixfix.md index d0838cf..43e2100 100644 --- a/docs/wiki_src/coding/mixfix.md +++ b/docs/wiki_src/coding/mixfix.md @@ -41,8 +41,7 @@ chain is not actually overwritten by *another* mixfix chain. ``` bruijn :test ((+8) + (-4) ⋅ (-2)) ((-8)) -# (don't do this) -…+…⋅… [[[(+16)]]] +…+…⋅… [[[2 + (1 ⋅ 0)]]] :test ((+8) + (-4) ⋅ (-2)) ((+16)) ``` diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md index 05fd683..002a6b8 100644 --- a/docs/wiki_src/technical/performance.md +++ b/docs/wiki_src/technical/performance.md @@ -6,7 +6,7 @@ an extension, bruijn also suffers from bad performance. Bruijn's interpreter works by substituting the entire program into one huge lambda calculus term that will then get reduced by the [reducer](reduction.md). As a result, many equivalent terms get -evaluated multiple times (although some of this get's solved by bruijn's +evaluated multiple times (although some of this is solved by bruijn's call-by-need reduction strategy). We currently work on a solution that reduces all equivalent terms as one, which turns out is not actually that trivial. Follow the [blog](https://text.marvinborner.de) to keep up @@ -33,3 +33,24 @@ Wiki, docs, articles, examples and more: Learn anything about bruijn in the [wiki](https://bruijn.marvinborner.de/wiki/) (also found in `docs/wiki_src/`). + +## References + +0. De Bruijn, Nicolaas Govert. “Lambda calculus notation with nameless + dummies, a tool for automatic formula manipulation, with application + to the Church-Rosser theorem.” Indagationes Mathematicae + (Proceedings). Vol. 75. No. 5. North-Holland, 1972. +1. Mogensen, Torben. “An investigation of compact and efficient number + representations in the pure lambda calculus.” International Andrei + Ershov Memorial Conference on Perspectives of System Informatics. + Springer, Berlin, Heidelberg, 2001. +2. Wadsworth, Christopher. “Some unusual λ-calculus numeral systems.” + (1980): 215-230. +3. Tromp, John. “Binary lambda calculus and combinatory logic.” + Randomness and Complexity, from Leibniz to Chaitin. 2007. 237-260. +4. Tromp, John. “Functional Bits: Lambda Calculus based Algorithmic + Information Theory.” (2022). +5. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and + efficient implementation of strong call by need by an abstract + machine. Proceedings of the ACM on Programming Languages, 6(ICFP), + 109-136. diff --git a/std/List.bruijn b/std/List.bruijn index 39aecf8..bb8bed3 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -1,7 +1,6 @@ # MIT License, Copyright (c) 2022 Marvin Borner # Lists in Church/Boehm-Berarducci encoding using pairs # implementations are generally lazy (except when they're broken) -# TODO: Replace fold/map/etc. with faster LC native logic :import std/Combinator . :import std/Pair P @@ -85,6 +84,9 @@ eval-r z [[rec]] :test (~!(inc : (inc : {}(+1)))) ((+3)) +# returns the element at unary index in list +index-unary [[P.fst (0 P.snd 1)]] ⧗ (List a) → Unary → a + # returns the element at index in list index z [[[rec]]] ⧗ (List a) → Number → a rec 0 [[[case-index]]] case-end diff --git a/std/Math.bruijn b/std/Math.bruijn index 07a9a9b..1737572 100644 --- a/std/Math.bruijn +++ b/std/Math.bruijn @@ -1,4 +1,5 @@ # MIT License, Copyright (c) 2022 Marvin Borner +# experimental functions, sometimes list-based :input std/Number diff --git a/std/Number.bruijn b/std/Number.bruijn index ffc2591..f74b7d4 100644 --- a/std/Number.bruijn +++ b/std/Number.bruijn @@ -1,6 +1,6 @@ # MIT License, Copyright (c) 2023 Marvin Borner # this is just a reference to the ternary implementation -# read the readme for the reasoning of using balanced ternary by default +# read the wiki for the reasoning of using balanced ternary by default :import std/List . diff --git a/std/Number/Binary.bruijn b/std/Number/Binary.bruijn index ea837e3..28a3f7f 100644 --- a/std/Number/Binary.bruijn +++ b/std/Number/Binary.bruijn @@ -1,4 +1,5 @@ # MIT License, Copyright (c) 2023 Marvin Borner +# binary implementation of T.Æ. Mogensen (see refs in README) # TODO: Use abstract representation for logic instead of listifying :import std/Combinator . diff --git a/std/Number/Ternary.bruijn b/std/Number/Ternary.bruijn index e9b402c..e1b3893 100644 --- a/std/Number/Ternary.bruijn +++ b/std/Number/Ternary.bruijn @@ -1,7 +1,6 @@ # MIT License, Copyright (c) 2022 Marvin Borner -# This file defines the most basic mathematical operations +# ternary implementation of T.Æ. Mogensen and Douglas W. Jones (see refs in README) # → refer to std/Math for more advanced functions -# Heavily inspired by the works of T.Æ. Mogensen and Douglas W. Jones (see refs in README) :import std/Box B :import std/Combinator . diff --git a/std/Tree/Rose.bruijn b/std/Tree/Rose.bruijn index 90abeec..1b1e319 100644 --- a/std/Tree/Rose.bruijn +++ b/std/Tree/Rose.bruijn @@ -34,7 +34,7 @@ empty? [L.empty? ~0] ⧗ (RoseTree a) → Boolean ∅?‣ empty? -:test (∅?({ 'a' : (({:}'b') : L.empty) })) (false) +:test (∅?({ 'a' : ({:}'b' : L.empty) })) (false) :test (∅?({:}'a')) (true) # applies a function to leaf and the leafs of all branches @@ -43,7 +43,7 @@ map z [[[rec]]] ⧗ (a → b) → (RoseTree a) → (RoseTree b) …<$>… map -:test (map ^‣ ({ "woo" : ({:}"oof" : (({ "aah" : (({:}"huh" : L.empty)) }) : L.empty)) })) ({ 'w' : ({:}'o' : (({ 'a' : ({:}'h' : L.empty) }) : L.empty)) }) +:test (map ^‣ ({ "woo" : ({:}"oof" : (({ "aah" : ({:}"huh" : L.empty) }) : L.empty)) })) ({ 'w' : ({:}'o' : (({ 'a' : ({:}'h' : L.empty) }) : L.empty)) }) # maps a function returning list of trees and concatenates concat-map L.concat ∘∘ map ⧗ ((RoseTree a) → (List (RoseTree b))) → (List (RoseTree a)) → (List (RoseTree b)) |