4.1. Types🔗
Laurel's types come in two groups: those a user can write — primitives,
collections, and user-defined types — and a few internal constructors the
implementation introduces that have no surface syntax.
The HighType type enumerates every type Laurel
tracks. Alongside the user-writable types it also includes internal constructors
(such as Unknown and MultiValuedExpr) that the compiler introduces
during resolution and later passes; these have no surface syntax.
🔗inductive typeStrata.Laurel.HighType : Type
Strata.Laurel.HighType : Type
The type system for Laurel programs (each constructor is documented
individually below). Two constructors are internal, not surface types:
Unknown (resolution-error recovery / gradual wildcard) and MultiValuedExpr
(multi-output-call results).
Constructors
TFloat64 : Strata.Laurel.HighType
64-bit floating point type. Required for JavaScript (number), also used by Python (float) and Java (double).
TMap
(keyType valueType :
Strata.Laurel.AstNode Strata.Laurel.HighType) :
Strata.Laurel.HighType
The TOTAL map type, TotalMap K V — Core's Map sort, i.e. an SMT array. Every key
has a value and select is defined everywhere, so this cannot express key absence.
This is the low-level map the heap, the type-hierarchy tables and the
select/update/mapConst primitives are stated over. The user-facing PARTIAL map is
Map<K, V>, an opaque prelude type represented as TotalMap K ($MapEntry V); it is an
.Applied head, not this node.
UserDefined (name : Strata.Laurel.Identifier) :
Strata.Laurel.HighType
A Identifier to a user-defined composite or constrained type by name.
TVar (name : Strata.Laurel.Identifier) :
Strata.Laurel.HighType
A bound type variable, e.g. T in procedure f<T>(x: T). Introduced by
resolution when a name in type position matches an in-scope type parameter
(declared on a procedure, composite, or datatype). Distinct from UserDefined,
which names a concrete type.
Unknown : Strata.Laurel.HighType
Type used internally by the Laurel compilation pipeline.
This type is used when a resolution error occurs,
to continue compilation without producing superfluous errors
Any type can be assigned to unknown and unknown can be assigned to any type.
The unknown type can not be represented in Core so its occurence will abort compilation before evaluating Core
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.
🔗structureStrata.Laurel.CompositeType : Type
Strata.Laurel.CompositeType : Type
A composite defines a type with fields and instance procedures.
Composite types may extend other composite types, forming a type hierarchy
that affects the results of IsType and AsType operations.
Constructor
Fields
name : Strata.Laurel.Identifier
typeArgs : List Strata.Laurel.Identifier
Type parameters, e.g. T in composite Box<T> { ... }. Empty for
monomorphic composites (default keeps existing sites compiling).
extending : List Strata.Laurel.HighTypeMd
Composite types this type extends, as type references. Usually a bare name
(.UserDefined Base), but a generic composite may extend a generic parent at an
instantiation (Box<T> extends Base<T> → .Applied (UserDefined Base) [TVar T]).
Consumers that only need the parent NAME peel the base via highBaseName?.
The type hierarchy affects IsType/AsType results.
🔗structureStrata.Laurel.Field : Type
Strata.Laurel.Field : Type
A field in a composite type, also used for file-scope globals (which resolution
registers as fields of the reserved $static owner). Fields declare their
name, mutability, and type.
Mutability affects what permissions are needed to access the field.
Constructor
Fields
name : Strata.Laurel.Identifier
isMutable : Bool
Whether the field is mutable. Mutable fields require write permission.
type : Strata.Laurel.HighTypeMd
initializer : Option Strata.Laurel.StmtExprMd
An optional initializer expression evaluated to produce the field's initial value.
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.
🔗structureStrata.Laurel.ConstrainedType : Type
Strata.Laurel.ConstrainedType : Type
A constrained (refinement) type defined by a base type and a predicate.
Algebraic datatypes can be encoded using composite and constrained types.
For example, Option<T> can be defined as a constrained type over Dynamic
with the constraint value is Some<T> || value is Unit.
Constructor
Fields
name : Strata.Laurel.Identifier
The constrained type's name.
base : Strata.Laurel.HighTypeMd
The base type being refined.
valueName : Strata.Laurel.Identifier
The name bound to the value in the constraint expression.
constraint : Strata.Laurel.StmtExprMd
The predicate that values of this type must satisfy.
witness : Strata.Laurel.StmtExprMd
A witness value proving the type is inhabited.
🔗inductive typeStrata.Laurel.TypeDefinition : Type
Strata.Laurel.TypeDefinition : Type
A user-defined type, either a composite type, a constrained type, an algebraic datatype,
an opaque (natively implemented) type, or a type alias.
Algebriac datatypes can also be encoded uses composite and constrained types. Here are two examples:
Example 1:
composite Some<T> { value: T }
constrained Option<T> = value: Dynamic | value is Some<T> || value is Unit
Example 2:
composite Cons<T> { head: T, tail: List<T> }
constrained List<T> = value: Dynamic | value is Cons<T> || value is Unit
Constructors
Opaque (ty : Strata.Laurel.OpaqueTypeDefinition) :
Strata.Laurel.TypeDefinition
An opaque type with a native implementation (e.g. opaque Set<T>;).
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.