Types are used to constrain the structure and behavior (class invariant) of the values that a variable can be assigned, or that a constant can be defined as. The type system, being based on the culmination of many feature sets, is necessarily complex. However, by simply working in a familiar paradigm - among imperative, functional, or constraint based and among static typing, late binding, or duck typing - the type system applies the appropriate constraints and compile-time analyses.

Here, we declare x as a variable that can store an integer, and assign the value 10.

declare and assign a variable

<Int> x ← 10;

error caused by contradicting the invariant

<Int> x ← 10;
x ← 1.5; //error - can't assign a fractional number to an integer

To use a type in the declaration of a variable or in the definition of a constant, the type must be enclosed by angle brackets < > (see TYPE_DEREFERENCE).


<Int> x;
print(type_of(x).name);         //prints "Int"
print(type_of(Int).name);       //prints "Type"
print(type_of(Type).name);      //prints "Type"

Types can be elided in many cases, and can be used to create unquantified generic functions.


identity := (value) { return value; };

Type Constructors

Functions may construct and return Type objects. These functions may be invoked using the angle-bracket syntax. Further, any function that returns an angle-bracket invokable function may also be angle-bracket invoked.


<Type * Int → Type> Vector := (T, s) { return T^s; };  // Vector is a function that return a Type.
Float32x3 := Vector<Float32, 3>;                       // type def and a function call

<Float32x3> aVectorVariable;                           // make a variable
<Vector<Float32, 3>> anotherVectorVariable;            // same type as previous line
<type_of(aVectorVariable)> yetAnotherVectorVariable;   // contrived but doable

Despite the function-like definition, simple constructs (e.g. Vector from above) are recognized as parametric types and benefit from the generic features involving variance and deduction.


The angle-bracket syntax is not required, since parenthesis can be used also. The convention is to use the angle-bracket syntax when the intent is use as a parametric type (see INVOCATION).

Type inference

Type inference, a feature of static typing, extends beyond inference of elided types in "obvious" scenarios, instead using all logical tools available (specifically constraint propogation and constant folding) for deduction. Type checking benefits from the same sophistication. Consider the following:


getParamCount := (<Function<types, retType>> f) {
	<List<Type>> types;
	return types.length;

types is never defined or assigned to, and is therefore unbound, but must be a List of Types. Upon attempting to evaluate types.length, a value for types is computed. An example of implicitly quantified generic programming:


<(X * X → X) → Type> binary_op_type := (<X * X → X> f) { return X; }

X is unbound, so may take on any type.

Covariance and Contravariance

The inheritance graph and variance properties are modeled and can be tested programmatically.



Animal := type {
	<Void → Void> speak <- abstract;

Cat := type implementing Animal {
	<Void → Void> speak <- { Meow(); };

<List<Animal> → Void> choir := (animals) {
	for (animal in animals) {

<Cat> bernard;
<Cat> russel;
List<Cat> kittehs := [ bernard, russel ];



<Animal → Void> solo := (animal) { animal.speak(); } ;
<Cat → Void> cat_solo = solo;

Covariant method arguments

Function overloads are ordered. The | operator, which is used to create function overloads, preserves the order of the elements (functions) and dispatches to the first overload that can accept the parameters.


<Animal → Void> solo :=
	(<Cat> _ ) { /* cats never do what you want */ } | // overload
	(animal) { animal.speak(); }

Note that the semantics resemble pattern matching.

Partial Types

Types may be combined with the plus + operator to create a new type containing the elements from each. This operation is not associative, as the right hand side operator will override any elements from the left hand side.

Example (part 1 of 2)

SomeThing := type {
	<String> data;
	print_data := { print(data); };
} + DataProvider;

(part 2 of 2)

DataProvider := type {
	<String> data := """
         !...:!TVBBBRPFT||||||||||!!^^""'   ||||
         !.......:!?|||||!!^^""'            ||||
         !.........||||                     ||||
         !.........||||  #                  ||||
         !.........||||                     ||||
         !.........||||                     ||||
         !.........||||                     ||||
         !.........||||                     ||||
         `.........||||                    ,||||
          .;.......||||               _.-!!|||||
   .,uodWBBBBb.....||||       _.-!!|||||||||!:'
!..YBBBBBBBBBBBBBBb!!||||||||!iof68BBBBBBRPFT?!::   `.
!....YBBBBBBBBBBBBBBbaaitf68BBBBBBRPFT?!:::::::::     `.
!......YBBBBBBBBBBBBBBBBBBBRPFT?!::::::;:!^"`;:::       `.
!........YBBBBBBBBBBRPFT?!::::::::::^''...::::::;         iBBbo.
`..........YBRPFT?!::::::::::::::::::::::::;iof68bo.      WBBBBbo.
  `..........:::::::::::::::::::::::;iof688888888888b.     `YBBBP^'
    `........::::::::::::::::;iof688888888888888888888b.     `
            `' !!988888888888888888888888899fT|!^"'

Algebraic Types

Types may be combined with the or | operator to create a new type thats instances must be any one of those types. This operator is associative.


InteriorNode := type { <Int> value;  next; };
TerminalNode := type { <Int> value; };
LinkedListNode := InteriorNode | TerminalNode

Further, algebraic types are not limited to simple switching. Like all algebraic values, they may be defined through a system of constraints.

copyright © Brent Lewis 2017