Laurel User Guide

3.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 type
Strata.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

TVoid : Strata.Laurel.HighType

The void type, used for statements that produce no value.

TBool : Strata.Laurel.HighType

Boolean type.

TInt : Strata.Laurel.HighType

Arbitrary-precision integer type.

TFloat64 : Strata.Laurel.HighType

64-bit floating point type. Required for JavaScript (number), also used by Python (float) and Java (double).

TReal : Strata.Laurel.HighType

Mathematical real type. Maps to Core's real type.

TString : Strata.Laurel.HighType

String type for text data.

TSet
  (elementType :
    Strata.Laurel.AstNode Strata.Laurel.HighType) :
  Strata.Laurel.HighType

Set type, e.g. Set int.

TMap
  (keyType valueType :
    Strata.Laurel.AstNode Strata.Laurel.HighType) :
  Strata.Laurel.HighType

Map type.

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.

Applied
  (base : Strata.Laurel.AstNode Strata.Laurel.HighType)
  (typeArguments :
    List (Strata.Laurel.AstNode Strata.Laurel.HighType)) :
  Strata.Laurel.HighType

A generic type application, e.g. List<Int>.

Intersection
  (types :
    List (Strata.Laurel.AstNode Strata.Laurel.HighType)) :
  Strata.Laurel.HighType

An intersection of types. Used for implicit intersection types, e.g. Scientist & Scandinavian.

TBv (size : Nat) : Strata.Laurel.HighType

Bitvector type of a given width.

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

MultiValuedExpr
  (types :
    List (Strata.Laurel.AstNode Strata.Laurel.HighType)) :
  Strata.Laurel.HighType

An internal-only type produced by computeExprType for multi-output procedure calls. Consumed by the resolution arity check and highEq. Should never appear in a serialized program.

3.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.

🔗structure
Strata.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

Strata.Laurel.CompositeType.mk

Fields

name : Strata.Laurel.Identifier

The type name.

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.

fields : List Strata.Laurel.Field

The fields of this type.

instanceProcedures : List Strata.Laurel.Procedure

Instance procedures (methods) defined on this type.

🔗structure
Strata.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

Strata.Laurel.Field.mk

Fields

name : Strata.Laurel.Identifier

The field name.

isMutable : Bool

Whether the field is mutable. Mutable fields require write permission.

type : Strata.Laurel.HighTypeMd

The field's type.

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.

🔗structure
Strata.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

Strata.Laurel.ConstrainedType.mk

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 type
Strata.Laurel.TypeDefinition : Type
Strata.Laurel.TypeDefinition : Type

A user-defined type, either a composite type, a constrained type, an algebraic datatype, 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

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

A composite (class-like) type with fields and methods.

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

A constrained (refinement) type with a base type and predicate.

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

An algebriac datatype.

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

A type alias (e.g. MyInt = int). Eliminated before Core translation.