• Stars
    star
    227
  • Rank 175,900 (Top 4 %)
  • Language
    JavaScript
  • License
    MIT License
  • Created over 7 years ago
  • Updated almost 2 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Expressive static types and invariant checks for JavaScript.

Forall.js

Expressive static type and invariant checks for JavaScript. It is similar to TypeScript, but:

  1. Has very precise types such as the type of hex-encoded strings with an even number of characters (i.e., new Buffer()'s input), and can statically check all of them;

  2. Has invariants such as for any user and any item, purchase(user,item).balance >= 0, so that, if you forget to check the balance in your purchase(User,Item) implementation, it becomes a compile-time error;

  3. Requires no additional compilation step: it works like a macro on top of vanilla JS, using Node.js as the "compiler", and then erasing itself out.

Yes, it can check claims such as "this function can't produce negative balances" at compile time. Sounds magical, but it is actually simple: the catch is that it isn't doing classical (logical) type-checking, but, instead, it "type-checks" by inspecting with random samples. It can, thus, be wrong sometimes. The hypothesis, though, is that, in practice, if your code is wrong, it will almost always spot it; and being wrong sometimes is compensated by catching a much larger class of bugs.

In short, Forall.js attempts to give you some of the expressivity of Idris, with the ease-of-use of TypeScript, trading absolute for probabilistic correctness. You can see it as the fusion of a type system with automated tests.

Examples

Use-cases can be simple, such as statically checking that you implemented a function correctly (w.r.t specification):

const F = require("forall");

// Returns the largest element of an array, or 0
const maximum = F(
  F.Fn(F.Array(F.Uint32), F.Uint32), // function from Array<Uint32> to Uint32
  function(array) {
    let max = 0;
    for (let i = 0; i < array.length; ++i)
      max = Math.max(array[i], max);
    return max;
  });

// "the largest element of any array should be larger than or equal to any of its elements"
F.forall([F.Array(F.Uint32), F.Uint16], (array, i) => maximum(array) >= (array[i % array.length] || 0));

Or very complex, such as checking the second functor law on an implementation of .map:

const F = require("forall");

// Gives a static type to JavaScript's `.map` function
//   map :: βˆ€ a b -> (a -> b) -> [a] -> [b]
const map = (A, B) => F(
  F.Fn(F.Fn(A, B), F.Array(A), F.Array(B)),
  (f, array) => array.map(f));

// Statically checks the second functor law on `map`
//   βˆ€ (A : Type)   -> βˆ€ (B : Type)   -> βˆ€ (C : Type) ->
//   βˆ€ (f : B -> C) -> βˆ€ (g : A -> B) -> βˆ€ (a : Array<A>) ->
//   map<B,C>(f, map<A,B>(g, a)) == map<A,C>(f . g, a)
F.forall([F.Type, F.Type, F.Type], (A, B, C) => {
  const equal = (a, b) => JSON.stringify(a) === JSON.stringify(b);
  const mapAB = map(A,B), mapBC = map(B,C), mapAC = map(A,C);
  return F.forall([F.Fn(B,C), F.Fn(A,B), F.Array(A)], (f, g, a) => {
    return equal(mapBC(f, mapAB(g, a)), mapAC(x => f(g(x)), a))
  }, 32); 
}, 4);

Once the checking is done, your program behaves the same as if Forall.js wasn't there, except also doing additional runtime checks. You, then, have two options: you can export the original functions, allowing dead-code-elimination to erase all Forall.js code from your final bundles, or you can export the typed functions, allowing your library users to see informative error messages if they use your functions incorrectly.

Installing

npm i forall

Learning

The best way to learn Forall.js is by following the Forall.js game.

Disclaimer

This is still very new and immature. The code, although short, is very messy and there is a lot to improve.

More Repositories

1

WebMonkeys

Massively parallel GPU programming on JavaScript, simple and clean.
JavaScript
1,163
star
2

LJSON

JSON extended with pure functions.
JavaScript
500
star
3

Caramel

A modern syntax for the Ξ»-calculus.
Haskell
405
star
4

PureState

The stupidest state management library that works.
JavaScript
309
star
5

abstract-algorithm

Optimal evaluator of Ξ»-calculus terms.
JavaScript
222
star
6

Cedille-Core

A minimal proof language.
JavaScript
193
star
7

optlam

An optimal function evaluator written in JavaScript.
JavaScript
115
star
8

Interaction-Type-Theory

Rust
108
star
9

calculus-of-constructions

Minimal, fast, robust implementation of the Calculus of Constructions on JavaScript.
JavaScript
94
star
10

Bitspeak

JavaScript
80
star
11

articles

Thoughts and stuff
JavaScript
65
star
12

UrnaCripto

Referendos criptograficamente incorruptΓ­veis.
JavaScript
51
star
13

lrs

Linkable Ring Signatures on JavaScript and PureScript.
PureScript
46
star
14

lambda-calculus

A simple, clean and fast implementation of the Ξ»-calculus on JavaScript.
JavaScript
44
star
15

heart

heart
JavaScript
41
star
16

ultimate-calculus

TypeScript
36
star
17

absal-rs

Rust
36
star
18

HOC

C
32
star
19

nano-json-stream-parser

A complete, pure JavaScript, streamed JSON parser in less than 1kb.
JavaScript
29
star
20

servify

Microservices in the simplest way conceivable.
JavaScript
28
star
21

optimul

Multiplication on optimal Ξ»-calculus reducers
JavaScript
22
star
22

parallel_lambda_computer_tests

learning cuda
Cuda
18
star
23

nano-ipfs-store

Lightweight library to store and get data to/from IPFS
JavaScript
14
star
24

formality-agda-lib-legacy

Agda libraries relevant to Moonad
Agda
14
star
25

taemoba

13
star
26

unknown_halting_status

Small programs with unknown halting status.
JavaScript
12
star
27

lsign

Quantum-proof, 768-bit signatures for 1-bit messages
JavaScript
11
star
28

reasoning_evals

my reasoning evals
JavaScript
9
star
29

Elementary-Affine-Net-legacy

JavaScript
8
star
30

OpenLegends

An open-source MOBA in Rust
6
star
31

ethereum-offline-signer

Signs an Ethereum transaction from the command line.
JavaScript
6
star
32

coc-with-math-prims

JavaScript
5
star
33

idris-mergesort-benchmark

Benchmark of the new Idris JS backend
JavaScript
5
star
34

uwuchat2_demo

UwUChat2 demo game
TypeScript
5
star
35

LPU

JavaScript
4
star
36

Vote

3
star
37

nano-persistent-memoizer

Caches a function permanently on browser and node.
JavaScript
3
star
38

nano-sha256

Use native Sha256 on both browser and Node.js
JavaScript
3
star
39

ReflexScreenWidget

A widget for Haskell-Reflex that renders a dynamic image to a Canvas in realtime.
Haskell
3
star
40

OSX

Vim script
3
star
41

EthFP

3
star
42

VictorTaelin

3
star
43

ethereum-rpc

JavaScript
2
star
44

ethereum-publisher-dapp

JavaScript
2
star
45

shared-state-machine

JavaScript
2
star
46

Trabalho-IC-UFRJ-2

Python
2
star
47

NeoTaelin

2
star
48

eth-web-tools

Some web Ethereum tools that MyEtherWallet currently lacks
JavaScript
2
star
49

hvm2

Cuda
2
star
50

symmetric-interaction-calculus-benchmarks

SIC benchmarks
JavaScript
2
star
51

talks

C
2
star
52

gpt

2
star
53

agbook

AGDA
Agda
2
star
54

Kind2

Kind refactor based on HVM
2
star
55

kind-react-component

Renders a Kind app as a React component
1
star
56

PongFromScratch

A simple tutorial on how to create a ping-pong game from scratch
1
star
57

tsbook

TypeScript
1
star
58

sketch_bros

Super Sketch Bros!
JavaScript
1
star
59

StupidMinimalistHash

C
1
star
60

MaiaVictor.github.io

HTML
1
star
61

PotS

JavaScript
1
star
62

LamBolt

The ultimate compile target for functional languages
1
star
63

form-login

Um formulÑrio de Login feito com HTML e CSS usando transiçáes
CSS
1
star
64

who-loves-voxels

JavaScript
1
star
65

cuda_rewrite_tests

learning cuda
Cuda
1
star
66

luna-lang-old-abandoned-repo

Typed version of Moon-lang
JavaScript
1
star
67

posts

1
star
68

FPL

A collection of functional JavaScript modules.
JavaScript
1
star
69

PassRhyme

JavaScript
1
star
70

something_calculus

1
star
71

moon-bignum

Minimalistic bignum library compiled from Moon-lang.
JavaScript
1
star
72

see

See inside JS functions
JavaScript
1
star
73

Trabalho-IC-UFRJ

JavaScript
1
star
74

optimal_evaluation_examples

optimal evaluation examples (DUP nodes, SUP nodes)
Haskell
1
star
75

inferno-hello-world-component

JavaScript
1
star
76

inet

JavaScript
1
star