FormCoreJS

A pure JavaScript, dependency-free, 700-LOC implementation of FormCore, a minimal proof language featuring inductive reasoning. It is the kernel of Kind. It compiles to ultra-fast JavaScript and Haskell. Other back-ends coming soon.

Usage

Install with npm i -g formcore-js. Type fmc -h to see the available commands.

fmc file.fmc: checks all types in file.fmc
fmc file.fmc --js main: compiles main on file.fmc to JavaScript

As a library:

var {fmc} = require("formcore-js");
fmc.report(`
  id : @(A: *) @(x: A) A = #A #x x;
`);

What is FormCore?

FormCore is a minimal pure functional language based on self dependent types. It is, essentially, the simplest language capable of theorem proving via inductive reasoning. Its syntax is simple:

ctr	syntax	description
all	`@self(name: xtyp) rtyp`	function type
all	`%self(name: xtyp) rtyp`	like all, erased before compile
lam	`#var body`	pure, curried, anonymous, function
app	`(func argm)`	applies a lam to an argument
let	`!x = expr; body`	local definition
def	`$x = expr; body`	like let, erased before check/compile
ann	`{term : type}`	inline type annotation
nat	`+decimal`	natural number, unrolls to lambdas
chr	`'x'`	UTF-16 character, unrolls to lambdas
str	`"content"`	UTF-16 string, unrolls to lambdas

It has two main uses:

A minimal, auditable proof kernel

Proof assistants are used to verify software correctness, but who verifies the verifier? With FormCore, proofs in complex languages like Kind can be compiled to a minimal core and checked again, protecting against bugs on the proof language itself. As for FormCore itself, since it is very small, it can be audited manually by humans, ending the loop.

An intermediate format for functional compilation

FormCore can be used as an common intermediate format which other functional languages can target, in order to be transpiled to other languages. FormCore's purity and rich type information allows one to recover efficient programs from it. Right now, we use FormCore to compile Kind to JavaScript, but other source and target languages could be involved.

The JavaScript Compiler

This implementation includes a high-quality compiler from FormCore to JavaScript. That compiler uses type information to convert highly functional code into efficient JavaScript. For example, the compiler will convert these λ-encodings to native representations:

Kind	JavaScript
Unit	Number
Bool	Bool
Nat	BigInt
U8	Number
U16	Number
U32	Number
I32	Number
U64	BigInt
String	String
Bits	String

Moreover, it will also convert any suitable user-defined self-encoded datatype to trees of native objects, using switch to pattern-match. It will also swap known functions like Nat.mul to native *, String.concat to native + and so on. It also performs tail-call optimization and inlines certain functions, including converting List.for to inline loops, for example. The generated JS should be as fast as hand-written code in most cases.

Example

The program uses self dependent datatypes to implement booleans, propositional equality, the boolean negation function, and proves that double negation is the identity (∀ (b: Bool) -> not(not(b)) == b):

Bool : * =
  %self(P: @(self: Bool) *)
  @(true: (P true))
  @(false: (P false))
  (P self);

true : Bool =
  #P #t #f t;

false : Bool =
  #P #t #f f;

not : @(x: Bool) Bool =
  #x (((x #self Bool) false) true);

Equal : @(A: *) @(a: A) @(b: A) * =
  #A #a #b
  %self(P: @(b: A) @(self: (((Equal A) a) b)) *)
  @(refl: ((P a) ((refl A) a)))
  ((P b) self);

refl : %(A: *) %(a: A) (((Equal A) a) a) =
  #A #x #P #refl refl;

double_negation_theorem : @(b: Bool) (((Equal Bool) (not (not b))) b) =
  #b (((b #self (((Equal Bool) (not (not self))) self))
    ((refl Bool) true))
    ((refl Bool) false));

main : Bool =
  (not false);

It is equivalent to this Kind snippet:

// The boolean type
type Bool {
  true,
  false,
}

// Propositional equality
type Equal <A: Type> (a: A) ~ (b: A) {
  refl ~ (b: a)
}

// Boolean negation
not(b: Bool): Bool
  case b {
    true: false,
    false: true,
  }

// Proof that double negation is identity
theorem(b: Bool): Equal(Bool, not(not(b)), b)
  case b {
    true: refl
    false: refl
  }!