Type Invariants

Type invariants carry a lot of the weight of proofs in practice. Type invariants are sometimes call refinement types. A Refinement Type describes a subset of the values of a Total Type.

A Total Type describes all values that can be represented. UnsignedInteger32 would be a Total Type. UnsignedInteger32 can represent all 32-bit unsigned integers.

By comparison, a refinement type, or implicitly any type with invariants, would not be Total. Odd numbers are a subset of all Integers. Odd numbers might be represented as Integers, but not all Integers are Odd.

987654321 : Odd + Integer

Type Invariants are properties that are attached to a type definition. The definition of Odd is as follows:

type Odd: Integer
   where self%2 | 1

Multiple properties can be attached to the same type definition.

type Factor23: Integer
   where self%2 | 0
   and   self%3 | 0;

The self keyword represents some value of the declared type. The bar syntax indicates that the preceding expression produces the following expression. When a value is bound by a type that has invariants, each invariant is checked as a precondition to satisfy that type. If a bound value does not satisfy its type's preconditions, then an error will occur.

Postconditions are the properties that we know about any given value. We may not know the exact value of a term, however we may know some of its properties. When this happens, we can often use the postconditions of a type to complete a proof.

In the above example of Factor23, we know that any value of that type will divide evenly into 2 and 3. This can be used as part of a proof, or in a program it can be used for constant folding.

let x:Factor23;
if x%2 == 0 then {
   //yes, always this branch
} else {
   //no, never this branch
}