4.8. Constrained types🔗

A constrained type (a refinement type) is a base type narrowed by a predicate. It is introduced with the constrained keyword and has four parts: a name, a value binder together with its base type, a where predicate that values of the type must satisfy, and a witness value that proves the type is inhabited.

constrained nat = x: int where x >= 0 witness 0

This declares nat as the integers that are at least zero. The binder x ranges over the base type int, x >= 0 is the constraint, and 0 is the witness — a concrete value Laurel checks against the predicate to be sure the type is not empty. A witness that fails its own predicate is rejected:

constrained bad = x: int where x > 0 witness -1
// error: the witness -1 does not satisfy x > 0

A constrained type is checked at every point where a value acquires the type, and it is available as an assumption at every point where a value is known to have the type. The rest of this section walks through those points.

4.8.1. Inputs🔗

A parameter of constrained type contributes a precondition. Callers must prove the argument satisfies the constraint, and in exchange the body may assume it.

constrained nat = x: int where x >= 0 witness 0

procedure inputAssumed(n: nat)
  opaque
{
  assert n >= 0   // holds: the nat constraint is assumed for inputs
};

Passing an argument that cannot be shown to satisfy the constraint fails at the call site, exactly like any other precondition.

4.8.2. Outputs🔗

An output of constrained type contributes a postcondition. The procedure must establish the constraint on its result, and callers may then assume it.

constrained nat = x: int where x >= 0 witness 0

procedure outputValid() returns (r: nat)
  opaque
{
  r := 3          // ok: 3 satisfies x >= 0
};

Returning a value that violates the constraint fails as a postcondition:

constrained nat = x: int where x >= 0 witness 0

procedure outputInvalid() returns (r: nat)
  opaque
{
  r := -1         // error: postcondition does not hold (-1 is not a nat)
};

Because the constraint travels with the output, a caller of an opaque procedure learns it from the contract alone, without seeing the body:

constrained nat = x: int where x >= 0 witness 0

procedure opaqueNat() returns (r: nat)
  opaque;

procedure callerAssumes()
  opaque
{
  var v: int := opaqueNat();
  assert v >= 0   // holds: opaqueNat's result is a nat
};

4.8.3. Local variables🔗

Initializing or assigning to a constrained-typed local asserts the constraint on the assigned value. Both the initial value and every later reassignment are checked.

constrained nat = x: int where x >= 0 witness 0

procedure assignLocal()
  opaque
{
  var y: nat := 5;   // ok
  y := -1            // error: assignment violates the nat constraint
};

A constrained-typed local that is declared without an initializer is treated as an arbitrary value that satisfies the constraint: the constraint is assumed, but nothing more. In particular you cannot assume it holds the witness value.

constrained nat = x: int where x >= 0 witness 0

procedure uninitialized()
  opaque
{
  var y: nat;
  assert y >= 0   // holds: the constraint is assumed
};

4.8.4. Quantifiers🔗

When a quantifier binds a variable of constrained type, the constraint is injected into the body so the bound variable ranges only over values of the type. For forall the constraint becomes an antecedent; for exists it becomes a conjunct.

constrained nat = x: int where x >= 0 witness 0

procedure quantifiedNat()
  opaque
{
  // provable only because n >= 0 is injected: false over all integers
  assert forall(n: nat) => n + 1 > 0;
  // 42 witnesses the existential and satisfies n >= 0
  assert exists(n: nat) => n == 42
};

4.8.5. Nested constrained types🔗

A constrained type may refine another constrained type. The constraints then compose: a value of the inner type must satisfy its own predicate and every predicate up the chain.

constrained even = x: int where x % 2 == 0 witness 0
constrained evenpos = x: even where x > 0 witness 2

procedure nested(x: evenpos)
  opaque
{
  assert x > 0;      // evenpos's own constraint
  assert x % 2 == 0  // inherited from even
};

Because algebraic datatypes can be encoded as constrained types over a base type, this composition is what lets a value carry several layers of invariant at once.