Batteries Not Included

The title of this example is a pun on the Python motto "batteries included". LSTS is a type-checker. LSTS does nothing else.

LSTS may connect with a bunch of other software products that include batteries. However, LSTS by itself is very minimal. LSTS does not even define "if", although it is given special syntax.

In this example we define "if". An if statement has three arguments. One argument for the Boolean branching condition. Two arguments for each conditional branch. The if statement returns the value of one of the branches. All branches and the return type are parameterized. The shared parameter will become the greatest-common-denominator of both branches.

let $"if"(condition: Boolean, branch1: A, branch2: A): A;

The same lack of features applies to the type system as well. The Boolean type referenced above must be defined by the user. Boolean types are somewhat special in that they also have dependent types carried along with them. To denote this special relation, we mark the type as Constant by adding the constant keyword.

type constant Boolean = True | False;

Numbers are user defined as well.

type Number;
type constant Integer: Number = /^[0-9][_0-9]*([eE][_0-9]+)?$/;
type          Real   : Number = /^[0-9][_.0-9]*([eE][-]?[_0-9]+)?$/;