Skip to content
No description, website, or topics provided.
Branch: master
Clone or download
Latest commit e636f48 May 20, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
javascript Inf utility for non-termination May 17, 2019
README.md Update git repo location May 18, 2019
interaction-combinators.gif updating reduction gif on Readme May 16, 2019
main.fmc Inf utility for non-termination May 17, 2019

README.md

Formality-Core

An optimal compilation target for functional programming languages. It is:

  1. Optimal: compatible with interaction combinators, no bookkeeping/oracle needed.

  2. GC-free: memory is freed when values go out of scope.

  3. Parallel: can be evaluated in GPUs, FGPAs and similar.

  4. Efficient: 128 bits per lambda/pair, unboxed 32-bit ints, constant-time beta-reduction.

  5. Terminating: computations are guaranteed to halt in elementary time.

  6. Simple: the entire implementation (all included) takes about 1.5k lines of code.

It features affine lambdas, elementary duplication ("cloning"), 32-bit numeric primitives and pairs.

Example

This example computes the nth number of the Fibonacci sequence. It uses compact λ-encoded nats to emulate loops.

// Gets the nth number of the Fibonacci sequence
def fib: [n]
  let init = &(0,1)
  let loop = [state]
    get &(a, b) = state
    get &(x, y) = cpy b
    &(x, {a + y})
  let stop = [state]
    (snd state)
  (for n #init #loop #stop)

Here is a table showing how many graph rewrites it takes for it to compute fib(n):

n fib(n) % 2^32 graph rewrites
1000 1318412525 6116
2000 3779916130 12124
3000 628070097 18139
4000 45579869 24132
5000 2020817954 30133
6000 1434712737 36147
7000 1424409805 42147
8000 1154982114 48140
9000 4044733297 54141
10000 2132534333 60141
11000 1648091042 66162
12000 690383169 72155
13000 4244933805 78148
14000 1699985506 84155
15000 774935569 90155

As you can see, fib(n) is linear, and needs exactly 6 graph rewrites per iteration of the loop. This JS implementation performs roughly 3m rewrites/s. We expect this to increase a few orders of magnitude with compilers and hardware.

For more examples, check main.fmc.

Usage

  1. Install it with npm:
npm i -g formality-core
  1. Type fmc to see a list of options and test in our example:
git clone https://github.com/moonad/formality-core.git
cd formality-core
fmc -s main

Theory

Formality-Core is based on the Elementary Affine Calculus, extended with numeric primitives and pairs. It is compiled to a lightweight interaction net system based on Symmetric Interaction Combinators for evaluation, as shown below:

To learn more about optimal evaluators and how they relate to traditional functional languages, check this Reddit post.

You can’t perform that action at this time.