diff options
| -rw-r--r-- | app/Main.hs | 4 | ||||
| -rw-r--r-- | bruijn.cabal | 1 | ||||
| -rw-r--r-- | docs/index.html | 30 | ||||
| -rw-r--r-- | docs/script.js | 2 | ||||
| -rw-r--r-- | docs/style.css | 6 | ||||
| -rw-r--r-- | docs/wiki_src/introduction/philosophy.md | 8 | ||||
| -rw-r--r-- | docs/wiki_src/technical/performance.md | 36 | ||||
| -rw-r--r-- | docs/wiki_src/technical/reduction.md | 38 | ||||
| -rw-r--r-- | src/Eval.hs | 3 | ||||
| -rw-r--r-- | src/Reducer.hs | 14 | ||||
| -rw-r--r-- | src/Reducer/HigherOrder.hs | 40 | ||||
| -rw-r--r-- | src/Reducer/ION.hs | 3 | ||||
| -rw-r--r-- | src/Reducer/RKNL.hs | 8 |
13 files changed, 144 insertions, 49 deletions
diff --git a/app/Main.hs b/app/Main.hs index 7e8d6ec..bbaea6a 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -32,8 +32,8 @@ args = ( long "reducer" <> short 'r' <> metavar "REDUCER" - <> value "RKNL" - <> help "Reducer (currently RKNL or ION)" + <> value "HigherOrder" + <> help "Reducer (currently RKNL, ION, or HigherOrder)" ) <*> optional (argument str (metavar "PATH" <> help "Path to file")) diff --git a/bruijn.cabal b/bruijn.cabal index f53bfd2..16d9c30 100644 --- a/bruijn.cabal +++ b/bruijn.cabal @@ -55,6 +55,7 @@ library Optimizer Parser Reducer + Reducer.HigherOrder Reducer.ION Reducer.RKNL other-modules: diff --git a/docs/index.html b/docs/index.html index a66c96c..4b5bc6e 100644 --- a/docs/index.html +++ b/docs/index.html @@ -57,11 +57,14 @@ <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> +<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+42)</span> +<span class="time">0.01 seconds</span></pre> </div> <div class="right"> - <p>Efficient call-by-need reduction using abstract machines.</p> + <p> + <a href="wiki/technical/performance/">Efficient</a> reduction using + abstract machines and higher-order encodings. + </p> </div> <div class="left"> @@ -90,10 +93,29 @@ hello world!</pre </div> <div class="right"> <p> - Compilation to Tromp's binary lambda calculus.<br /> + <a href="wiki/coding/compilation/">Compilation</a> to Tromp's binary + lambda calculus.<br /> Support for byte and ASCII encoding. </p> </div> + + <div class="left"> + <p> + <a href="wiki/coding/meta-programming/">Meta-programming</a><br /> + and self-interpretation. + </p> + </div> + <div class="right"> + <pre class="code"> +<span class="repl">></span> <span class="symbol">length</span> <span class="meta">`</span><span class="symbol">factorial</span> +<span class="repl">></span> <span class="mixfix">!</span><span class="left-app">(</span><span class="symbol">swap</span> <span class="meta">`</span><span class="left-app">(</span><span class="unary">(+2u)</span> <span class="unary">(+3u)</span><span class="right-app">))</span> +<span class="repl">></span> <span class="symbol">lhs</span> <span class="left-app">(</span><span class="symbol">blc→meta</span> <span class="string">"010000100000110"</span><span class="right-app">)</span></span> +</pre> + <!-- <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="bar big"> diff --git a/docs/script.js b/docs/script.js index 5859c55..0b147f5 100644 --- a/docs/script.js +++ b/docs/script.js @@ -37,6 +37,7 @@ describe("header", "[0] is the identity operation. It returns the first argument 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("meta", "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code."); 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."); describe("repl", "This indicates a REPL input."); describe("right-abs", "The closing bracket of a function abstraction."); @@ -46,5 +47,6 @@ 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 De Bruijn indices."); describe("time", "Incredibly fast for lambda calculus standards."); +describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly also known as a Church numeral. Needs a sign and brackets to differentiate it from De Bruijn indices."); document.body.addEventListener("click", clearPopups, true) diff --git a/docs/style.css b/docs/style.css index 1739f58..60e8fe5 100644 --- a/docs/style.css +++ b/docs/style.css @@ -180,7 +180,7 @@ a { color: #ff64bd; } -.code .ternary, .code .binary { +.code .ternary, .code .binary, .code .unary { color: #b1ee13; } @@ -199,3 +199,7 @@ a { .code .index { color: #ff5050; } + +.code .meta { + color: #ff94ff; +} diff --git a/docs/wiki_src/introduction/philosophy.md b/docs/wiki_src/introduction/philosophy.md new file mode 100644 index 0000000..4c70a94 --- /dev/null +++ b/docs/wiki_src/introduction/philosophy.md @@ -0,0 +1,8 @@ +# Philosophy + +- minimal, proven core +- small, expressive functions +- style consistency +- API consistency +- implicit parallelisation +- shared evaluation diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md index 002a6b8..709affe 100644 --- a/docs/wiki_src/technical/performance.md +++ b/docs/wiki_src/technical/performance.md @@ -1,24 +1,18 @@ # Performance -The reduction of lambda calculus is (practically) not very efficient. As -an extension, bruijn also suffers from bad performance. +In general, the reduction of practical programs encoded in lambda +calculus is not very efficient when compared to traditional programming +languages. We do, however, work a lot on making the performance as +comparable as possible: -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 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 -to date with the development. - -Aside from that, bruijn is still much faster than most of the hobby -programming languages based on pure lambda calculus. This is because of -the [RKNL reducer](reduction.md) and our choice of default [number/byte -encodings](../coding/data-structures.md). - -``` bruijn -> :import std/Math . -> :time fac (+30) -0.15 seconds -``` +- We have different reducers and constantly benchmark and improve them + in order to find the most efficient method of reduction. Read more + about our [reducer choices](reduction.md). +- Bruijn uses efficient data structures by default. For example, for + nary numbers we use results of Torben Mogensens investigations (as + described in [number/byte encodings](../coding/data-structures.md)). +- The lambda calculus optimizers + [BLoC](https://github.com/marvinborner/bloc) and + [BLoCade](https://github.com/marvinborner/blocade) are directly + integrated into bruijn and can be enabled optionally (see + [compilation](../coding/compilation.md)) diff --git a/docs/wiki_src/technical/reduction.md b/docs/wiki_src/technical/reduction.md index 97bd78f..ef21180 100644 --- a/docs/wiki_src/technical/reduction.md +++ b/docs/wiki_src/technical/reduction.md @@ -1,10 +1,38 @@ # Reduction -Bruijn uses the RKNL abstract machine reducer[^1]. RKNL uses the -call-by-need reduction strategy, similar to Haskell and other functional -programming languages. For you this means that you have efficient -support for [laziness](../coding/laziness.md) with generally less -redundant reductions. +Bruijn supports several reducers that can be chosen using its +`--reducer` flag. + +## HigherOrder [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/HigherOrder.hs) + +HigherOrder reduction is one of the simplest reducers. By translating +the entire expression to a higher-order representation, we can abuse +Haskell's internal reduction implementation in our favour. Aside from +conversion from/to the higher-order encoding, this reducer does +basically nothing special. + +## RKNL [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/RKNL.hs) + +RKNL[^1] is an abstract machine for reducing lambda calculus. It uses +the call-by-need reduction strategy, similar to Haskell and other +functional programming languages. For you this means that you have +efficient support for [laziness](../coding/laziness.md) with generally +less redundant reductions. + +## ION [`(source)`](https://github.com/marvinborner/bruijn/blob/main/src/Reducer/ION.hs) + +[The ION machine](https://crypto.stanford.edu/~blynn/compiler/ION.html) +was created by Benn Lynn as a reducer for a hypothetical functional +stack machine computer. We convert the lambda calculus term to +combinatory logic using [Kiselyov +translation](https://crypto.stanford.edu/~blynn/lambda/kiselyov.html), +set up a "virtual" machine with the combinators, and let it run until +the stack has reached its end. + +Most of the work was done by John Tromp in his +[nf.c](https://github.com/tromp/AIT/commits/master/nf.c). The +translation to Haskell and its integration into bruijn was mainly done +as an experiment on performance. [^1]: [Biernacka, Małgorzata, Witold Charatonik, and Tomasz Drab. "A simple and efficient implementation of strong call by need by an diff --git a/src/Eval.hs b/src/Eval.hs index 2e9746d..5091b49 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -7,6 +7,7 @@ import Binary import Control.Concurrent import Control.DeepSeq ( deepseq ) import Control.Exception +import Control.Monad ( when ) import Control.Monad.State import qualified Control.Monad.State.Strict as StrictState import qualified Data.BitString as Bit @@ -148,7 +149,7 @@ evalQuote f sub = evalExp f sub >>= \case evalUnquote :: Expression -> Environment -> EvalState (Failable Expression) evalUnquote f sub = evalExp f sub >>= \case Left e -> pure $ Left e - Right f' -> pure $ Right $ Unquote $ unsafeReduce f' -- TODO: REMOVE UNSAFE + Right f' -> pure $ Right $ Unquote $ reduceNoIO f' evalExp :: Expression -> Environment -> EvalState (Failable Expression) evalExp idx@(Bruijn _ ) = const $ pure $ Right idx diff --git a/src/Reducer.hs b/src/Reducer.hs index 3be8306..31ed3da 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -1,18 +1,20 @@ -- MIT License, Copyright (c) 2024 Marvin Borner module Reducer ( reduce - , unsafeReduce + , reduceNoIO ) where import Helper +import qualified Reducer.HigherOrder as HigherOrder import qualified Reducer.ION as ION import qualified Reducer.RKNL as RKNL reduce :: EvalConf -> Expression -> IO Expression reduce conf e = case _reducer conf of - "RKNL" -> RKNL.reduce e - "ION" -> pure $ ION.reduce e - _ -> error "Invalid reducer" + "RKNL" -> RKNL.reduce e + "ION" -> pure $ ION.reduce e + "HigherOrder" -> pure $ HigherOrder.reduce e + _ -> error "Invalid reducer" -unsafeReduce :: Expression -> Expression -unsafeReduce = RKNL.unsafeReduce +reduceNoIO :: Expression -> Expression +reduceNoIO = HigherOrder.reduce diff --git a/src/Reducer/HigherOrder.hs b/src/Reducer/HigherOrder.hs new file mode 100644 index 0000000..91378b7 --- /dev/null +++ b/src/Reducer/HigherOrder.hs @@ -0,0 +1,40 @@ +-- MIT License, Copyright (c) 2024 Marvin Borner +-- Slightly modified version of Tromp's AIT/Lambda.lhs reducer implementation +module Reducer.HigherOrder + ( reduce + ) where + +import Helper + +data HigherOrder = HigherOrderBruijn Int | HigherOrderAbstraction (HigherOrder -> HigherOrder) | HigherOrderApplication HigherOrder HigherOrder +data NamedTerm = NamedVariable Int | NamedAbstraction Int NamedTerm | NamedApplication NamedTerm NamedTerm + +app :: HigherOrder -> HigherOrder -> HigherOrder +app (HigherOrderAbstraction f) = f +app f = HigherOrderApplication f + +eval :: Expression -> HigherOrder +eval = go [] + where + go env (Bruijn x ) = env !! x + go env (Abstraction e ) = HigherOrderAbstraction $ \x -> go (x : env) e + go env (Application e1 e2) = app (go env e1) (go env e2) + go _ _ = invalidProgramState + +toNamedTerm :: HigherOrder -> NamedTerm +toNamedTerm = go 0 + where + go _ (HigherOrderBruijn i) = NamedVariable i + go d (HigherOrderAbstraction f) = + NamedAbstraction d $ go (d + 1) (f (HigherOrderBruijn d)) + go d (HigherOrderApplication e1 e2) = NamedApplication (go d e1) (go d e2) + +resolveExpression :: NamedTerm -> Expression +resolveExpression = resolve [] + where + resolve vs (NamedVariable i ) = Bruijn $ vs !! i + resolve vs (NamedAbstraction v t) = Abstraction $ resolve (v : vs) t + resolve vs (NamedApplication l r) = Application (resolve vs l) (resolve vs r) + +reduce :: Expression -> Expression +reduce = resolveExpression . toNamedTerm . eval diff --git a/src/Reducer/ION.hs b/src/Reducer/ION.hs index 9154bd8..5eb959b 100644 --- a/src/Reducer/ION.hs +++ b/src/Reducer/ION.hs @@ -147,7 +147,8 @@ rules ch vm = case chr' ch of let parentVal = load (load (sp vm1 + 1) vm1 + 1) vm1 let (a, vm2) = app (ord 'f') (load (sp vm1) vm1) vm1 lazy 0 (wor a) (wor parentVal) (store (sp vm2) parentVal vm2) - _ -> error $ "invalid combinator " ++ show ch + '\0' -> store (sp vm) (arg' 1 vm) vm + _ -> error $ "invalid combinator " ++ show ch where lvm n f g = lazy n f g vm eval :: VM -> VM diff --git a/src/Reducer/RKNL.hs b/src/Reducer/RKNL.hs index 9513e38..5aa6ca1 100644 --- a/src/Reducer/RKNL.hs +++ b/src/Reducer/RKNL.hs @@ -2,7 +2,6 @@ -- based on the RKNL abstract machine module Reducer.RKNL ( reduce - , unsafeReduce ) where import Control.Concurrent.MVar @@ -11,7 +10,6 @@ import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as Map import Data.Maybe ( fromMaybe ) import Helper -import System.IO.Unsafe ( unsafePerformIO ) -- TODO: AAH type Store = Map Int Box type Stack = [Redex] @@ -109,9 +107,3 @@ reduce e = do forEachState (loadTerm redex) transition >>= \case Cconf _ [] v -> pure $ fromRedex v _ -> invalidProgramState - --- TODO: AAAAAAAAAAAAAAAAH remove this --- (probably not thaaat bad) -{-# NOINLINE unsafeReduce #-} -unsafeReduce :: Expression -> Expression -unsafeReduce = unsafePerformIO . reduce |