Static type inference for JavaScript.

Inside every big ugly language there is a small beautiful language trying to come out.

MOTHBALLED

I have little time for this project, and don't use JS at work anymore so I'm less motivated to continue. But I still believe it's the right way to go with type safety in JS.

Features

• It's just JavaScript: runs as-is in your browser. No transpilation or compilation required for running.
• Full type inference: no type annotations necessary.
• Safety: a strict type system with no workarounds sets a high bar for code correctness. So you can sleep at night!
• Work in progress: it can set your computer on fire!

Type System

• Parametric polymorphism (aka "generics"), based on Hindley-Milner type inference.
• Row-type polymorphism, otherwise known as "static duck typing".
• Simple type classes (which allow for example correct support of JS + and [] operators).
• Recursive types for true representation of object-oriented methods.
• Correct handling of JS's this dynamic scoping rules.

For more information see Infernu's Type System.

Also see the intro blog post for a short discussion comparing infernu to other type checkers.

Installation

Quick and Dirty

First, install haskell stack.

Then use stack to install infernu:

git clone git@github.com:sinelaw/infernu.git
cd infernu/
stack setup
stack install

Usage: see infernu --help

Quick example usage:

echo 'function getLength(x) { return x.length; }' > getLength.js

infernu getLength.js

Output:

    //       getLength : a.({length: b, ..c} -> b)
    function getLength(x) { return x.length; }

A bit more detailed instructions

1. Install Haskell stack.
2. Clone this repository.

Then run:

cd infernu/
stack setup
stack install

The infernu executable will be installed to your ~/.local/bin. You may want to add it to your PATH.

Running tests

cd infernu
stack setup
stack build
cd test
./test.sh

Currently there are still a few failing tests due to unclosed issues in the type system.

The file test/fail.txt records the test failures and is kept in git. This makes it easier to track progress on outstanding bugs.

Examples

Basic

JavaScript:

var num = 2;
var arrNums = [num, num];

Infernu infers:

//  num : Number
//  arrNums : [Number]

That is, an array of numbers.

Objects:

var obj = { something: 'hi', value: num };

Inferred type:

//  obj : {something: String,
           value: Number}

That is, an object with two properties: 'something', of type string, and 'value' of type number.

Functions and this

In JS, this is one truly awful part. this is a dynamically scoped variable that takes on values depending on how the current function was invoked. Infernu knows about this (pun intended) and infers types for functions indicating what this must be.

For example:

function useThisData() {
	return this.data + 3;
}

Infernu infers:

//       useThisData : {data: Number, ..a}.(() -> Number)

In words: a function which expects this to be an object with at least one property, "data" of type Number. It takes no arguments (hence the empty ()). It returns a Number.

If we call a function that needs this incorrectly, Infernu will be angry:

Error: Could not unify:
    {data: Number, ..a}
  With:
    Undefined

Because we called useThisData without a preceding object property access (e.g. obj.useThisData), it will get undefined for this. Infernu is telling us that our expected type for this is not unifiable with the type undefined.

Polymorphism

Given the following function:

function makeData(x) {
    return {data: x};
}

Infernu infers the following type:

a.(b -> {data: b})

In words: A function that takes anything for its this, and an argument of any type b. It returns an object containing a single field, data of the same type b as the argument.

Row-type polymorphism (static duck typing)

Given the following function:

function getData(obj) {
	return obj.data;
}

Infernu infers:

h.({data: i, ..j} -> i)

In words: a function taking any type h for this, and a parameter that contains at least one property, named "data" that has some type i (could be any type). The function returns the same type i as the data property.

Type Classes

See here for more about Infernu's type classes.

The basic example is for the + operator:

function add(x,y) { return x + y; }

The type for add is inferred to be:

//       add : Plus b => a.((b, b) -> b)

Meaning: given any type a that is an instance of the Plus type class, the function takes two as and returns an a.

The two instances of Plus currently defined are the types Number and String.

---

Author

Noam Lewis - @noam_lewis

Road map

The following needs to be done to make infernu reasonably usable:

• Finish support for basic builtin JS apis.
• Add support for browser / DOM / web apis.
• Add ability to declare types for, or wrap external libraries.
• Add support for some kind of module system.
• Better error messages.

Pending discussion

Things that could be done, but may not be so important:

• Allow empty var decls (use first assignment as starting point for types) - how to prevent uninitialized variable issues? General approach should be to add a translation pass that moves var decls down to the first assignment, but care must be taken to avoid escaping usage-before-assignment to an otherwise shadowed name.
• When concluding that two recursive types are equivalent, use that information to simplify the resulting types (perhaps using the simpler of the two everywhere) - nice to have, because currently recursive types are displayed opaquely anyway.

More important but also more complicated or impossible to implement:

• Find a reasonable solution for optional parameters - perhaps using an implicit "Maybe"-like type or implicit type unions, and require guards?
• An (implicitly inferred) maybe type, for better safety of things like array access at index. Unfortunately because the maybe wrap/unwrap will have to implicit, this isn't easy to solve. See branch maybe.
• Sum types with guards as pattern matchers. Required because some functions, like array index access, can return 'undefined' (e.g. if index is out of range) - breaks parametricity and complicates the inference greatly.
• Allow defining constructor-object properties using the notation obj.prototype.something = ... - requires non-local context to deteremine the type of a constructor function.
• support arguments (a tuple?) and function bind
• Should we treat functions as objects with properties? the only properties they have are: length (very weird! we might as well leave it out), and call/bind/apply (which need special handling)

Future

• Type annotations
• Add support for CommonJS modules

p.s. (Formerly known as Inferno / Safe JS / SJS)