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. Types may be eschewed, but benefit from static checks by the type system. Forgoing stack checks, use late binding, or duck typing. Angle brackets dereference types.

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 a variable of type Int

Create types using the type keyword.

Color := type {


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

Elide types where type constraints are undesired.

The identity function

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

Type Constructors

Parametric types are functions returning Type values, and syntactically identical to functions. These functions should be invoked using the angle-bracket syntax, which performs type checking.


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

<Float32x3> x;                // a variable
<Vector<Float32, 3>> y; // all these variables are the same type
<type_of(x)> z;               // 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.

This website does not use cookies or javascript, excluding the Google search bar and Google analytics.
copyright © Brent Lewis 2013-2018