Uns☁und

An extensible and unsound programming languages framework

(This page might be a bit more readable if you enable 1st-party CSS.)

Unsound provides language extensions that build on each other.

Layers

Core

A minimal functional language. Everything is an expression:

let x = 42 in x
let f = (a, b) => a in f(1, 2)
if true then "yes" else "no"
[1, 2, 3][0]
{ x: 1, y: 2 }.x

Primitives: numbers, strings, booleans, null. Compound values: arrays and objects. Functions are lambdas with implicit return.

Meso

Adds infix and prefix operators using precedence climbing. Precedence (low to high): ||, &&, equality, comparison, +/-, *///%, prefix !/-.

1 + 2 * 3
x > 0 && x < 10
!done || count == 0

Operators compile to method calls: a + b becomes a["op+"](b). This lets values define their own operator behavior. The exceptions are ===/!==, which use primitive dispatch to handle null comparisons.

Thermo

Adds imperative features. Semicolons sequence expressions; in a sequence, let bindings scope over subsequent expressions:

let x = 1;
let y = 2;
x + y

Blocks group statements and evaluate to their last expression. Assignment mutates existing bindings:

let x = 1;
{
  x = x + 10;
  x * 2
}

Programmable Types

Exo adds type annotation syntax, along with typechecking semantics.

let x : Number = 42;
let f: (n: Number) => Number = (n) => n + 1;
f(x)

The interesting thing about Exo is how types and typechecking are implemented. Specifically, each type annotation is an Exo expression -- a value -- that is itself evaluated before performing type checking.

In addition, when interpreting a binding's value:

let x: T = value;

We first evaluate T using the default $interpret semantics to determine the type. Then we evaluate value using the $type semantics, and compare the results using op$= on T to determine whether value is assignable to x.

To learn more about Exo's type system see Type Semantics.


For more on writing your own languages, see Authoring Languages and Extensions.