The refreshing simplicity of compiling Formality to anything
Formality is a new programming language featuring theorem proving that, unlike most in the category, is designed to have a familiar syntax and run efficiently. I often associate it with “optimal interaction-net runtimes” that outperform Haskell, Ocaml, Clojure and other functional languages in some very high-order algorithms.
While that is cool, it isn’t mandatory: one of its charms is how it is flexible to different compilation needs. For example, it has a every performant Ethereum backend, where 1 function call uses only 200 gas. Here, I’ll show you how to easily convert its libraries to fast and small CommonJS or ES6 modules, and how refreshingly simple the FFI (Foreign Function Interface, i.e., calling functions from other languages) is.
A brief review of Formality
Let’s first explain the language by writing a small module which we will later compile to JS. Formality is a pure functional language highly inspired in Haskell, but featuring “first-class theorem proving” like Idris and Agda, and a more traditional syntax. This is how we define a datatype:
T Bit
| b0
| b1This syntax indicates that Bit is a type with two possible values, b0 or b1. Formality functions look like TypeScript ones, except with less ifs and fors and more cases and recursion. Here is an algorithm that negates a boolean N times:
flip_once(bit: Bit) : Bit
case bit
| b0 => b1
| b1 => b0flip_times(times: Number, bit: Bit) : Bit
if times === 0 then
bit
else
flip_times(times - 1, flip_once(bit))
Here, flip_times works by recursively flipping bit and decreasing times until it reaches 0, essentially emulating a for loop with recursion. Formality also features dependent types and theorem proving, which is nothing but a fancy way to say that you can write down some property (“theorem”) such as "flipping a bool twice always returns itself”, and prove it is true by checking it case by case. For example, this is how we prove the property we just wrote:
// For any bit, flipping it twice returns itself
MyTheorem(bit: Bit) : Type
flip_times(2, bit) == bit// Proof of the statement above
my_proof(bit: Bit) : MyTheorem(bit)
case bit
| b0 => equal(__)
| b1 => equal(__)
: MyTheorem(bit)
And that’s the essence of it. Formality programming is all about defining datatypes to model your data, recursive functions to transform it, and mathematically proving properties by case analysis.
PS1: To understand in what sense this is a “mathematical proof” and how it differs from a unit test, check this Reddit answer, as well as the section of the documentation linked on it.
PS2: I picked this syntax for two reasons. First, it is more familiar to non-functional programmers, as it satisfies the principle of least astonishment. Second, it avoids the redundancy you see in some functional languages, as you don’t need to repeat some names. This annoys me, so I avoided it.
-- Notice how, in Agda, you name the same var in many places
flip_times : (times : Number) -> (bool : Bool) -> Bool
flip_times 0 bool = bool
flip_times (succ pred) bool = flip_times pred (flip_once bool)Compiling Formality to Javascript
What makes Formality so easy to compile to anything is that the entire language, all of it, ends up desugared to a series of lambdas, numbers and nothing else. This gives us a quick and dirty way to compile Formality to any language featuring high-order functions: just transpile them directly! For example, let’s compile the module we just made. Here is the complete file:
Save it as flipper.fm, install Formality and type this in the same directory:
fm -J flipper/@The console will output the following JavaScript module:
Notice how flip_times, got transpiled directly. This file has less than 1KB and is ready to be imported and used in other JavaScript programs! Compared to, say, GHCJS, which generates files of several megabytes, that is a huge relief, specially for those who lived “The JavaScript problem”. To use the compiled module, we just export it as flipper.js and import in any JS file as usual. There is only one caveat: since Formality datatypes get compiled to raw functions, you need encode/decode them if you want to use familiar JS types. In the case above, you’d do something like this:
var flipper = require("./flipper.js");// Encode/decode booleans as functions
var encode_bool = bool => True => False => bool ? True : False;
var decode_bool = bool => bool(true)(false);// Tests our algorithm
var times = 101;
var bool = encode(true);
var result = flipper.flip_n_times(times)(bool);
var output = decode(result);
console.log(output);
The program above will output false, which is true flipped 101 times. That’s all, really. Our JavaScript compiler is a 125 LOC file, thus the same idea could be used to quickly compile it to Python, Clojure, Ruby and so on. Using Formality inside other languages is so easy it feels wrong, but it just works. Builds won’t get bloated because the files are so small. There is even a Webpack module that allows you to import .fm files directly:
import {flipper} from "./flipper.fm"Thanks g-guimaraes for this!
How efficient that approach is?
Sure, files are small, but what about efficiency? Won’t all those curried lambdas slow things considerably? Somewhat. As far as my test goes, in most cases, seems like JS engines are capable of optimizing lambda-encoded datatypes quite decently. Let’s benchmark!
Finding a representative way to test it is hard, so I’ve decided to go with IntMap, a container implemented with Patricia Trees. I found it to be very representative, since it is a non-trivial algorithm that requires a lot of pattern matches and recursion, and is the best attempt to emulate C arrays as a pure functional data structure.
My test consisted of 3 cases: first, an IntMap module implemented in Formality and compiled to JavaScript with no modifications. Second, the exact same algorithm re-implemented using non-curried native JavaScript functions and objects. Third, Immutable.js, which is one of the fastest IntMap implementations in JavaScript and the current market standard.
My test was simple: I just inserted a lot of numbers to create a huge map, then retrieved them one by one and outputted the sum. Here is the result:
elems | Immutable.js | JavaScript | FormalityJS
----- | ------------ | ---------- | -----------
100k | 0.156s | 0.285s | 2.343s
200k | 0.213s | 0.597s | 5.794s
300k | 0.299s | 1.089s | 8.917s
400k | 0.425s | 1.362s | 11.794s
500k | 0.528s | 1.725s | 15.712s
600k | 0.688s | 2.113s | 21.486s
700k | 0.849s | 2.533s | 25.975s
800k | 0.971s | 3.351s | 30.355s
900k | 1.098s | 3.934s | 33.508s
1m | 1.275s | 4.231s | 40.952sAs you can see, inserting and reading 1 million elements on the compiled Formality module took about 10x more time than the hand-written JS one, and 34x more than the industry standard. This is not stellar, but is practical, and is not far behind other lang-to-JS compilers. If you want more performance, you could pick other compilation methods, but given the immense convenience of this FFI, this isn’t a bad way to convert formally verified code into CommonJS libraries that you can use today. The code to reproduce this benchmark is available here.
If you like my contents, please follow my very unpopular Twitter (sobs) as I’m using this exact compilation strategy to develop a very charming online web game in Formality, and will be posting updates of the process there.
Thanks for reading!
