Types

Verum has a single type-definition form: type T is .... What follows the is determines what kind of type you get.

Primitives

Type	Description
Bool	true or false (1 byte)
Int	canonical 64-bit signed integer
Int8, Int16, Int32, Int64, Int128	sized signed
UInt8..UInt128	sized unsigned
ISize, USize	platform-pointer-sized
Float / Float64	canonical 64-bit IEEE 754
Float32	32-bit IEEE 754
Char	Unicode scalar value (4 bytes, U+0000..U+10FFFF)
Text	UTF-8 string (heap-backed, in core.text)
Byte	alias for UInt8
()	unit (0 bytes)
! / Never	never (uninhabited bottom)
unknown	top

Records (product types)

type Point is { x: Float, y: Float };
type User  is { id: UserId, email: EmailAddr, age: Int { 0 <= self && self <= 150 } };

Record literals:

let p = Point { x: 1.0, y: 2.0 };
let u = User   { id: my_id, email: em, age: 28 };

Struct update:

let p2 = Point { x: 3.0, ..p };    // same y as p

Row polymorphism

Record types can be extensible — specify some fields, leave the rest open via a trailing row variable. Row-polymorphic functions work with any record that has at least the listed fields:

// Accepts any record with an `x: Int` field, regardless of what else
// it contains. The row variable `r` captures the remaining fields.
fn get_x<r>(p: { x: Int | r }) -> Int { p.x }

let p2d = Point   { x: 1, y: 2 };
let p3d = Point3D { x: 1, y: 2, z: 3 };

get_x(p2d);  // OK — r unifies with {y: Int}
get_x(p3d);  // OK — r unifies with {y: Int, z: Int}

Multiple known fields + a row variable:

fn greet<r>(u: { name: Text, age: Int | r }) -> Text {
    f"Hello, {u.name}!"
}

Nested row polymorphism — each inner record can carry its own row variable:

fn get_inner_name<r, s>(n: { inner: { name: Text | s } | r }) -> Text {
    n.inner.name
}

A closed record — no row variable — requires an exact match on the field set; row-polymorphic code is strictly more permissive.

Sum types (variants)

type Color is Red | Green | Blue;

type Shape is
    | Circle   { radius: Float }
    | Square   { side:   Float }
    | Triangle (Float, Float, Float);

Variants with no data, with named fields, or with tuple payloads are all supported in the same declaration.

Constructors are namespaced under the type name:

let s = Shape.Circle { radius: 1.5 };
let c = Color.Red;

Tuples

let pair: (Int, Text) = (42, "hello");
let (n, s) = pair;
let triple: (Int, Int, Int) = (1, 2, 3);
let unit: () = ();

Single-element tuples: (x,) — the trailing comma distinguishes them from parenthesised expressions.

Arrays and slices

let xs: [Int; 5]     = [1, 2, 3, 4, 5];        // fixed-size array
let zeros: [Int; 10] = [0; 10];                // repeated element
let ys: &[Int]       = &xs[..];                // slice (length-carrying reference)

Function types

type Pred<T>      is fn(T) -> Bool;
type Reducer<A,R> is fn(R, A) -> R;
type AsyncHandler is async fn(Request) -> Response using [Http];

Function types include:

• parameter types,
• return type,
• using [...] context clause,
• throws(E) (if any),
• rank-2 / universal quantification for higher-rank types: fn<R>(Reducer<B, R>) -> Reducer<A, R> (the caller does not choose R — the function must work for every R).

Type aliases

type UserId  is Int { self > 0 };
type UserMap is Map<UserId, User>;

Aliases are transparent — the compiler treats UserId and the underlying refined Int as the same type for unification.

Note: Top-level type definitions use is, not =. The = form is reserved for associated-type bindings inside implement / protocol blocks (e.g. type Item = WatchEvent<T>; inside an implement Iterator for Watch { … }). See the Grammar reference — Type definitions for the full rules.

Newtypes

A newtype is a distinct nominal type over a single payload:

type Celsius    is (Float);
type Fahrenheit is (Float);

fn boil() -> Celsius { Celsius(100.0) }
// `Celsius(100.0)` is NOT assignable to `Fahrenheit` without a conversion.

Newtypes cost nothing at runtime; they exist purely for the type checker's benefit.

Unit type

type Marker is ();
let m: Marker = Marker;

Existential (opaque) types

fn make_iter() -> some I: Iterator<Item = Int> { 0..100 }

The caller sees some type implementing Iterator<Item = Int> without the concrete type leaking into the signature.

Dynamic (trait) objects

let shapes: List<dyn Drawable> = [Circle(1.0), Square(2.0)];

dyn P is a runtime-polymorphic pointer. List<T> is constructed from a literal array with the canonical [a, b, c] syntax — no list! macro, no List.from_array; the compiler coerces the array literal at the let-binding boundary. See Protocols for when to prefer impl P.

Generics

type Pair<A, B> is { first: A, second: B };
type Identity<T: Clone + Eq> is (T);

Bounds are written with : and combined with +. Negative bounds use !:

fn send_to<T: Send + !Sync>(x: T) { ... }

See Generics for full type-parameter syntax.

Refinement types (preview)

type Positive<T: Numeric> is T { self > T.zero() };
type SortedList<T: Ord>   is List<T> { self.is_sorted() };

Covered in Refinement types.

Dependent types (preview)

// Sigma type — length-indexed vector
type Vec is n: Int, data: [Int; n];

// Path type constructor (cubical HoTT): the type of paths
// from `a` to `b` in carrier `A`.
mount core.math.hott.Path;
type SelfLoop<A> is fn(x: A) -> Path<A>(x, x);

Covered in Dependent types.

Where clauses

Constraints that are more natural at the end:

type Grid<T> is { cells: List<List<T>> }
    where self.cells.all(|row| row.len() == self.cells[0].len());

Affine types

type affine Resource is { handle: Int, ... };
// A `Resource` value must be used exactly zero or one times — never
// duplicated. The compiler enforces this.

Capability-restricted types

CBGR references carry a monotonically-attenuating capability set drawn from the eight bits READ | WRITE | EXECUTE | DELEGATE | REVOKE | BORROWED | MUTABLE | NO_ESCAPE. A capability-restricted reference declares which subset it carries:

type Database.ReadOnly is Database with [READ];
type Database.Full     is Database with [READ, WRITE];

fn analyse(db: Database with [READ]) -> Stats { ... }

A capability set restricts which methods are callable on the value; reducing the set (db.readonly()) is always allowed, but expanding it is not — the compiler enforces monotonic attenuation across every conversion. See architecture → CBGR internals for the full 8-bit table.