FormCore.js port to Dart.

So far only the parser and typechecker have been
ported i.e. the FormCore.js file in the original
repo.

(Original readme from https://github.com/moonad/FormCoreJS)

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:

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:

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
  }!

The GitHub Link:

https://github.com/modulovalue/FormCore.dart