• Stars
    star
    227
  • Rank 170,528 (Top 4 %)
  • Language
    JavaScript
  • License
    MIT License
  • Created about 7 years ago
  • Updated over 1 year 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

Interaction-Calculus

A programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
Rust
597
star
3

LJSON

JSON extended with pure functions.
JavaScript
500
star
4

Caramel

A modern syntax for the λ-calculus.
Haskell
405
star
5

PureState

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

abstract-algorithm

Optimal evaluator of λ-calculus terms.
JavaScript
222
star
7

Cedille-Core

A minimal proof language.
JavaScript
193
star
8

optlam

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

calculus-of-constructions

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

Interaction-Type-Theory

Rust
88
star
11

Bitspeak

JavaScript
80
star
12

articles

Thoughts and stuff
JavaScript
65
star
13

ChatSH

Chat with GPT from the terminal, with the ability to execute shell scripts.
JavaScript
63
star
14

ESCoC

A nano "theorem prover".
JavaScript
61
star
15

absal-ex

Absal ex
53
star
16

eth-lib

Lightweight Ethereum libraries
JavaScript
52
star
17

UrnaCripto

Referendos criptograficamente incorruptíveis.
JavaScript
51
star
18

lrs

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

swarm-js

JavaScript
45
star
20

lambda-calculus

A simple, clean and fast implementation of the λ-calculus on JavaScript.
JavaScript
44
star
21

heart

heart
JavaScript
41
star
22

AIEMU

Simple AI-based (Claude-3) game emulator
JavaScript
39
star
23

nano-ethereum-signer

Very small Ethereum signer and verifier
JavaScript
37
star
24

absal-rs

Rust
36
star
25

Moonad-web-legacy

A Peer-to-Peer Operating System
JavaScript
35
star
26

Formality

JavaScript
35
star
27

ultimate-calculus

TypeScript
35
star
28

HOC

C
32
star
29

interaction-calculus-of-constructions

A minimal proof checker.
TypeScript
31
star
30

nano-json-stream-parser

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

servify

Microservices in the simplest way conceivable.
JavaScript
28
star
32

ab_challenge_eval

Evaluator for the A::B Prompting Challenge
JavaScript
24
star
33

kind-ai

23
star
34

optimul

Multiplication on optimal λ-calculus reducers
JavaScript
22
star
35

parallel_lambda_computer_tests

learning cuda
Cuda
18
star
36

Navim

Navigates files on the terminal with the minimal amount of keystrokes.
JavaScript
18
star
37

Elementary-Affine-Core-legacy

A simple, untyped, terminating functional language that is fully compatible with optimal reductions.
JavaScript
17
star
38

formality-agda-lib-legacy

Agda libraries relevant to Moonad
Agda
15
star
39

nano-ipfs-store

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

Elementary-Affine-Type-Theory-legacy

Minimal, efficient proof language
JavaScript
14
star
41

Taelang

my personal lang
TypeScript
13
star
42

unknown_halting_status

Small programs with unknown halting status.
JavaScript
12
star
43

lsign

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

AI-scripts

Some handy AI scripts
JavaScript
10
star
45

diagonalize

Searches through infinite branches
JavaScript
9
star
46

escoc-libs-legacy

Base Formality libraries
JavaScript
9
star
47

MiniPaper

shorten long papers with GPT-4
JavaScript
9
star
48

Elementary-Affine-Net-legacy

JavaScript
8
star
49

Formality-Net-legacy

C
7
star
50

run_solidity

Runs a Solidity file. That's all.
JavaScript
6
star
51

OpenLegends

An open-source MOBA in Rust
6
star
52

formality-document

Rust
6
star
53

coc-with-math-prims

JavaScript
5
star
54

Nasic-legacy

N-Ary Symmetric Interaction Combinators
JavaScript
5
star
55

idris-mergesort-benchmark

Benchmark of the new Idris JS backend
JavaScript
5
star
56

taemoba

4
star
57

LPU

JavaScript
4
star
58

Formality-Web-legacy

JavaScript
4
star
59

uwuchat

chat based messaging and rollback state computer
JavaScript
4
star
60

ethereum-offline-signer

Signs an Ethereum transaction from the command line.
JavaScript
4
star
61

LambdaIO-Formality-Talk

JavaScript
3
star
62

Vote

3
star
63

Formality-to-Nasic-legacy

Compiles a Formality term to a Nasic graph
JavaScript
3
star
64

Treeduce

C
3
star
65

clifun

3D clifford algebras visualization
JavaScript
3
star
66

Formality-IO-legacy

JavaScript
3
star
67

nano-persistent-memoizer

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

nano-sha256

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

ReflexScreenWidget

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

OSX

Vim script
3
star
71

EthFP

3
star
72

freeform-wpm-test

A simple WPM test that allows you to type anything you want.
HTML
2
star
73

ethereum-rpc

JavaScript
2
star
74

ethereum-publisher-dapp

JavaScript
2
star
75

symmetric-interaction-calculus-benchmarks

SIC benchmarks
JavaScript
2
star
76

NeoTaelin

2
star
77

shared-state-machine

JavaScript
2
star
78

Trabalho-IC-UFRJ-2

Python
2
star
79

eth-web-tools

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

VictorTaelin

2
star
81

MiniPapers

Papers and books minified to fit given LLMs context lengths.
2
star
82

gpt

2
star
83

hvm2

Cuda
2
star
84

Formality-sugars-legacy

Default syntax sugars for Formality
JavaScript
2
star
85

talks

C
2
star
86

PongFromScratch

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

kind-react-component

Renders a Kind app as a React component
1
star
88

fineorder

1
star
89

PotS

JavaScript
1
star
90

piramidex

JavaScript
1
star
91

LamBolt

The ultimate compile target for functional languages
1
star
92

sketch_bros

Super Sketch Bros!
JavaScript
1
star
93

StupidMinimalistHash

C
1
star
94

MaiaVictor.github.io

HTML
1
star
95

haelin

HTML
1
star
96

cuda_rewrite_tests

learning cuda
Cuda
1
star
97

luna-lang-old-abandoned-repo

Typed version of Moon-lang
JavaScript
1
star
98

Kind2

Kind refactor based on HVM
1
star
99

inferno-hello-world

Inferno Hello World with Hyperscript
JavaScript
1
star
100

posts

1
star