4.1.1. User-Defined Types🔗

User-defined types come in two categories: composite types and constrained types.

Composite types have fields and procedures, and may extend other composite types. Fields declare whether they are mutable and specify their type.

Strata.Laurel.CompositeType : Type
Strata.Laurel.CompositeType : Type

Strata.Laurel.CompositeType.mk

name : Strata.Laurel.Identifier

typeArgs : List Strata.Laurel.Identifier

extending : List Strata.Laurel.HighTypeMd

fields : List Strata.Laurel.Field

instanceProcedures : List Strata.Laurel.Procedure

Strata.Laurel.Field : Type
Strata.Laurel.Field : Type

Strata.Laurel.Field.mk

name : Strata.Laurel.Identifier

isMutable : Bool

type : Strata.Laurel.HighTypeMd

initializer : Option Strata.Laurel.StmtExprMd

Constrained types are defined by a base type and a constraint over the values of the base type. Algebraic datatypes can be encoded using composite and constrained types.

Strata.Laurel.ConstrainedType : Type
Strata.Laurel.ConstrainedType : Type

Strata.Laurel.ConstrainedType.mk

name : Strata.Laurel.Identifier

base : Strata.Laurel.HighTypeMd

valueName : Strata.Laurel.Identifier

constraint : Strata.Laurel.StmtExprMd

witness : Strata.Laurel.StmtExprMd

free : Bool

Strata.Laurel.TypeDefinition : Type
Strata.Laurel.TypeDefinition : Type

Strata.Laurel.TypeDefinition.Composite
  (ty : Strata.Laurel.CompositeType) :
  Strata.Laurel.TypeDefinition

Strata.Laurel.TypeDefinition.Constrained
  (ty : Strata.Laurel.ConstrainedType) :
  Strata.Laurel.TypeDefinition

Strata.Laurel.TypeDefinition.Datatype
  (ty : Strata.Laurel.DatatypeDefinition) :
  Strata.Laurel.TypeDefinition

Strata.Laurel.TypeDefinition.Opaque
  (ty : Strata.Laurel.OpaqueTypeDefinition) :
  Strata.Laurel.TypeDefinition

Strata.Laurel.TypeDefinition.Alias
  (ty : Strata.Laurel.TypeAlias) :
  Strata.Laurel.TypeDefinition

4.1.2. Primitive types🔗

Laurel provides unbounded mathematical int and real types, a bool type, string, and fixed-width bitvectors bv N. Because int is unbounded, arithmetic in specifications behaves like ordinary mathematics: there is no overflow to reason around when you are stating what a procedure computes. Likewise real is an exact mathematical real, not a floating-point approximation — a decimal literal such as 3.1415 denotes exactly that rational value.

There is no writable void type; a procedure with no outputs is void. float64 is accepted by the parser as a statement of intent, but is not implemented, so it cannot be used in a program that has to be analysed.

4.1.3. Collections🔗

Laurel has four built-in collection types. They are declared in the always-on prelude rather than built into the grammar, so their operations are ordinary procedure calls and they can be used wherever a value can. None of them has literal syntax: build a collection from its empty value.

Map<K, V> is a partial map — a key may be absent — and is the one to reach for when modelling a source-language dictionary:

procedure mapDemo()
  opaque
{
  var m: Map<int, bool> := mapEmpty();
  m := mapSet(m, 1, true);
  assert mapContains(m, 1);
  assert mapGet(m, 1);
  m := mapRemove(m, 1);
  assert !mapContains(m, 1)
};

mapGet is total but unconstrained on an absent key, so it returns some value of the right type rather than failing. Test with mapContains when absence matters.

Set<T> is an immutable set, and Sequence<T> an immutable sequence:

procedure setDemo()
  opaque
{
  var s: Set<int> := setEmpty();
  s := setInsert(s, 3);
  assert setContains(s, 3);
  assert !setContains(setRemove(s, 3), 3)
};

procedure seqDemo()
  opaque
{
  var xs: Sequence<int> := seqEmpty();
  xs := seqBuild(xs, 7);
  assert seqLength(xs) == 1;
  assert seqSelect(xs, 0) == 7
};

seqSelect, seqUpdate, seqTake, and seqDrop carry bounds preconditions, so an in-range index is a proof obligation at the call site rather than an unchecked read.

Underneath all of these is TotalMap K V, a total map in which every key has a value. It is the low-level building block, and it is available directly when a producer wants exactly that:

procedure totalMapDemo()
  opaque
{
  var t: TotalMap int bool := mapConst(false);
  t := update(t, 1, true);
  assert select(t, 1);
  assert !select(t, 0)
};

Its three primitives are select(m, k), update(m, k, v), and mapConst(v), and they satisfy the expected law, select(update(m, k, v), k) == v.

Prefer the partial Map<K, V> in ordinary code: TotalMap cannot express absence, so a front end modelling a dictionary would have to encode key presence separately, which is exactly what Map<K, V> already does.

mapConst, mapEmpty, setEmpty, and seqEmpty take no argument that fixes their type, so their result type is read from the declared type of the binding they initialize. Always annotate that binding — every argument-less empty constructor needs it.

4.1.4. Named and generic types🔗

A bare identifier names a composite, a datatype, a constrained type, an opaque type, or a type alias. Generic types are applied with angle brackets:

datatype Option<T> {
  Nothing(),
  Some(value: T)
}

composite Box<T> {
  var item: T
}

procedure boxDemo()
  opaque
{
  var b: Box<int> := new Box<int>;
  b#item := 3;
  assert b#item == 3
};

Type parameters are first-order: a parameter cannot itself be applied to arguments, so there are no higher-kinded types. The resolver checks that the base is generic and that the number of arguments is exact.

Two further declarations name a type without giving it structure. A type alias introduces a second spelling for an existing type, and is expanded early, so it is interchangeable with its target:

type Ints = Map<int, int>

An opaque type introduces a named type with no constructors: its values can be passed, stored, and compared, but not taken apart. The operations come from procedures declared over it. This is how Set and Sequence themselves are declared, and it is the right tool for modelling a source-language type whose representation should stay hidden:

opaque Handle

4.1.5. Subtyping and gradual typing🔗

Composite inheritance defines nominal subtyping, so that Cat below is a subtype of Animal:

composite Animal {}
composite Cat extends Animal {}

A constrained type unfolds to its base type for subtyping purposes. There are no implicit numeric promotions of any kind: keep the operands of an arithmetic operator at a single concrete type.

Subtyping does not yet extend through a generic type's arguments. Generic types are invariant, so a Sequence<Circle> is not accepted where a Sequence<Shape> is expected even when Circle extends Shape, and the same applies to a Map, a Set, and a generic composite or datatype — both as a call argument and as a field. Variance is intended and not yet supported, so a front end for a language with covariant collections has to erase to a common element type, or convert element by element, for now.

Alongside these, resolution has an internal Unknown type. It is what an unannotated hole gets, and what a failed rule substitutes so that one error does not cascade. Unknown is consistent with every type, which is what makes it a gradual escape hatch, but it is not writable as a source type, and a program that still contains one cannot be analysed. Its rules are in Holes and Gradual typing above.