Generics

Generics in Verum parameterise items by types, const values, kinds, contexts, and (rarely) universe levels. This page walks through every form.

Type parameters

type Pair<A, B> is { first: A, second: B };

fn swap<A, B>(p: Pair<A, B>) -> Pair<B, A> {
    Pair { first: p.second, second: p.first }
}

Conventionally:

T, U, V — general-purpose element types.
K, V — map key / value.
A, B, C — curried composition (functors, transducers).
E — error type.
F<_>, G<_> — type constructors (HKT).
I — iterator; S — stream.

The compiler doesn't enforce these conventions; the standard library follows them.

Explicit type arguments

Verum uses the spaceless <T> form everywhere — both in type position and when supplying explicit type arguments to a generic call:

let xs: List<Int> = List.new();    // type position
let xs = List.new<Int>();          // explicit type arg on a generic call
let n  = size_of<Int>();           // explicit type arg on a free function

Verum has no Rust-style turbofish (<T>): :: is not a token in grammar/verum.ebnf. The grammar disambiguates foo<T>(args) from foo < T by lookahead — the parser knows whether the identifier names a generic-capable function in scope, and switches arms accordingly.

Bounds

fn max<T: Ord>(a: T, b: T) -> T {
    if a > b { a } else { b }
}

fn serialise<T: Serialize + Send + !Sync>(x: T) -> List<Byte> { ... }

Semantics:

T: Bound1 + Bound2 — intersection (both must hold).
T: !Bound — negative bound. The type must not implement Bound.
T: Protocol<A, B> — parameterised bound.
T: Protocol<Item = U> — bound with an associated-type binding.

Associated-type bounds

Constrain a protocol's associated type:

fn show_all<I: Iterator>(it: I)
    where I.Item: Display,
          I.Item: Clone
{
    for item in it { print(item); }
}

Conditional implementations

Implementations can themselves be generic over bounds:

implement<T: Display> Display for List<T> {
    fn fmt(&self, f: &mut Formatter) -> FmtResult {
        f.write("[");
        let mut first = true;
        for item in self.iter() {
            if !first { f.write(", "); }
            item.fmt(f)?;
            first = false;
        }
        f.write("]")
    }
}

List<T> implements Display only when T does.

Per-instantiation dispatch

When an inherent implement block pins one or more type parameters to a concrete type, the methods defined there are only reachable on matching instantiations. This is how the stdlib models access-tagged types like Register<T, MODE>:

// `read` only exists when MODE = ReadOnly / ReadWrite / WriteOneToClear.
implement<T: Copy> Register<T, ReadOnly>  { fn read(&self) -> T { … } }
implement<T: Copy> Register<T, ReadWrite> { fn read(&self) -> T { … } }

// `write` only exists when MODE = WriteOnly / ReadWrite / …
implement<T: Copy> Register<T, WriteOnly>  { fn write(&self, value: T) { … } }
implement<T: Copy> Register<T, ReadWrite>  { fn write(&self, value: T) { … } }

fn drive(status: Register<UInt32, ReadOnly>) {
    let v = status.read();       // ✓ ReadOnly has `read`
    status.write(0x0001);        // ✗ E400 at type check — ReadOnly has no `write`
}

Slot-matching rules:

An implement-level generic slot (T in implement<T: Copy> Register<T, ReadOnly>) matches any concrete argument at the same position.
A concrete slot (like ReadOnly) must match the receiver's corresponding argument structurally.
A receiver whose slot is still a type variable stays permissive so inference isn't pinned prematurely.

Where clauses

When bounds get complex, move them to where:

fn process<T, U>(xs: List<T>, f: fn(T) -> U) -> List<U>
    where T: Clone + Debug,
          U: Eq,
          type U.Item: Display      // associated-type bound
{
    xs.iter().map(|x| f(x.clone())).collect()
}

Four clause forms stack on one function — two under where (bounds / meta) and two as bare keywords on their own signature lines (contract clauses):

where T: Bound — generic constraints (after the where keyword).
where meta <expr> — compile-time predicates on generics.
requires <expr> — runtime precondition. Bare, on its own signature line; repeat the keyword for multiple preconditions (no comma-joining).
ensures <expr> — runtime postcondition. Bare; one keyword per clause (no comma-joining).

where requires / where ensures forms that combine a where prefix with the contract keyword do not parse today — use the bare forms.

See language/functions and verification → contracts for the full grammar.

Const generics

Parameters that are compile-time values:

type Matrix<const R: Int, const C: Int, T> is {
    data: [[T; C]; R],
};

fn identity<const N: Int, T: Numeric>() -> Matrix<N, N, T> {
    let mut m = Matrix { data: [[T.zero(); N]; N] };
    for i in 0..N { m.data[i][i] = T.one(); }
    m
}

// Usage:
let m3: Matrix<3, 3, Float> = identity<3, Float>();

This example is the intended shape, not working code today: for i in 0..N reads the parameter as a VALUE, and a const generic read as a value gives nil — see the measured warning at the end of this section.

Const generics can carry refinements:

type RingBuffer<const N: Int { self > 0 }, T> is {
    data: [T; N],
    head: Int { 0 <= self && self < N },
    len:  Int { 0 <= self && self <= N },
};

The refinement N > 0 is intended to be checked at every instantiation.

Measured 2026-09-03: not checkable with the syntax available

Two ways to reach it, both blocked:

identity<0, Float>(x)          // error<E408>: expects 1 explicit type
                               //   argument — a const generic cannot be
                               //   supplied positionally at a call site
fn take<const N: Int { self > 0 }>(buf: &[Byte; N]) -> Int { N }
take(&([] : [Byte; 0]))        // accepted — the refinement does not fire

and the second is not evidence either, because the parameter is not a usable value: the same function's body returns N, and printing it gives nil rather than the length. Until a const generic can be supplied explicitly and read as a value, a refinement on one documents an intention.

Const expressions in generic positions

fn double_sized<const N: Int>(xs: [Int; N]) -> [Int; N * 2] { ... }

type Concat<const A: Int, const B: Int, T> is [T; A + B];

The grammar restricts const expressions in type positions to a bounded arithmetic fragment — +, -, *, /, and references to other const generics. Anything more complex requires an explicit const fn evaluation.

Higher-kinded types (HKT)

Type constructors — types that take types — are first-class:

type Functor<F<_>> is protocol {
    fn map<A, B>(x: F<A>, f: fn(A) -> B) -> F<B>;
};

implement Functor<Maybe> for Maybe {
    fn map<A, B>(x: Maybe<A>, f: fn(A) -> B) -> Maybe<B> {
        match x {
            Maybe.Some(a) => Maybe.Some(f(a)),
            Maybe.None    => Maybe.None,
        }
    }
}

F<_> is a type constructor of kind Type -> Type. F<A> applies it.

Explicit kind annotations

Two equivalent syntaxes:

// Placeholder form:
type Functor<F<_>> is protocol { ... };

// Kind-annotation form:
type Functor<F: Type -> Type> is protocol { ... };

Higher kinds:

type Arr<F: Type -> Type, G: Type -> Type> is protocol {
    fn run<A>(x: F<A>) -> G<A>;
};

type HigherOrder<F: (Type -> Type) -> Type> is protocol { ... };

Existential types

Hide concrete type behind protocol bounds:

fn make_iter() -> some I: Iterator<Item = Int> {
    (0..10).filter(|n| n % 2 == 0)
}

The caller sees "some iterator of Int" — they can iterate, but they don't know the concrete type. Three related but distinct things:

some I: P (return position) — the existential itself: this function hides one concrete type behind the bound P, chosen by the function, opaque to the caller.
A plain generic bound, <T: P> (parameter position) — the caller chooses the concrete type; the function is monomorphised per type, same as Static vs dynamic dispatch. Verum has no impl Trait-in-argument-position sugar for this.
dyn T — runtime polymorphism via vtable; less efficient but heterogeneous collections work.

Existential type aliases:

type Plugin is some P: PluginInterface;

See language/types.

Type-level functions

Compute types from types at compile time:

type Apply<F<_>, A> = F<A>;

type ListOr<T> = List<Maybe<T>>;

The right side is a type expression using the parameters; there's no function body to run — the compiler substitutes at instantiation.

Meta parameters

A compile-time value, usable in types, and carrying a refinement the compiler checks where the argument is supplied.

public type Hash<N: meta USize { it == 32 || it == 64 }> is {
    bytes: [Byte; N],
};

Two separate guarantees come out of that one line.

The width is part of the type's identity. Hash<32> and Hash<64> are different types, so a function taking one cannot be handed the other:

error<E400>: Type mismatch: expected 'Hash<32>', found 'Hash<64>'

There is no length check to forget, because there is no comparison across widths to write. For a digest that matters: a 32-byte hash compared against the first 32 bytes of a 64-byte one is equal for as long as anyone looks.

The refinement says which values the parameter admits at all, and it is decided at compile time — which is the point of a compile-time parameter:

let sha1: Hash<20> = …;

error<E506>: meta argument 1 of `Hash` violates its refinement:
             `20` does not satisfy `it == 32 || it == 64`

The alternative in most languages is an assertion inside one constructor, which runs after the value exists and is absent from the next constructor someone adds.

Only arguments that evaluate at compile time are judged. A parameter passed through from an enclosing generic has no value yet, so nothing is concluded about it:

// Accepted: `N` is symbolic here, and a refusal has to be a fact
// about a value.
public fn width_of<N: meta USize>(h: &Hash<N>) -> Int { h.bytes.len() }

where meta <expr> is the other spelling, adding a constraint beside the signature rather than on the parameter:

fn statically_sized_vec<dim: meta Int>() -> Vector<dim>
    where meta dim > 0 && dim <= 4
{ ... }

Context parameters

A function can abstract over which context it uses:

fn forward<using C>(msg: Message) using [C, Logger]
    where C: MessageSink
{
    C.send(msg);
    Logger.info("forwarded");
}

// Callers specialise:
forward<Kafka>(msg);
forward<Redis>(msg);

Context polymorphism lets you write higher-order combinators that propagate contexts from callback to caller:

fn map_context<T, U, using C>(
    items: List<T>,
    f: fn(T) -> U using C,
) -> List<U>
    using [C]       // caller must provide C too
{
    items.iter().map(f).collect()
}

Rank-2 polymorphism

Some function types quantify internally — the caller cannot pick the inner type parameter:

type Transducer<A, B> is {
    transform: fn<R>(Reducer<B, R>) -> Reducer<A, R>,
};

fn<R>(...) -> ... reads "for every R, this function produces…" The caller supplies a Reducer for an R of its choice; the transducer does not know R in advance.

Rank-2 is how Verum expresses:

Transducers (data-independent stream transformers).
CPS combinators that work for any answer type.
Stream fusion primitives.

See cookbook/calc-proofs for a rank-2 example building a verified fold-combinator.

The record field does not survive the bake

Written exactly as above — a fn<R>(...) as a RECORD FIELD — the field bakes as Unit, so the transducer you get back is not the function you wrote. The type checker accepts the declaration; the value is lost between there and the archive. Tracked as T0997.

Rank-2 in a plain function signature is a separate question and is not covered by that measurement.

Lifetime / region parameters

The grammar accepts a lifetime wherever a type parameter may appear, so this parses:

fn longest<'r>(a: &'r Text, b: &'r Text) -> &'r Text {
    if a.len() >= b.len() { a } else { b }
}

It constrains nothing. Lifetime annotations are parsed and discarded: &'static Text and &Text check identically, and a signature whose annotations disagree with each other is accepted exactly like one whose annotations agree. Reference safety in Verum comes from CBGR and escape analysis, which read the code — not from the annotations.

Write them only as documentation, if at all, and never as a claim the compiler will hold you to. Region inference is where the guarantee lives; see References.

Universe polymorphism

For dependent-type-heavy code, universe polymorphism prevents "Type is too big for itself" paradoxes:

fn id<universe u, A: Type(u)>(x: A) -> A { x }

u is a universe level; Type(u) is the type of types at level u. A polymorphic id works for types in Type(0) (ordinary values), Type(1) (types themselves), or higher.

Alternative spelling using a Level bound:

fn id<u: Level, A: Type(u)>(x: A) -> A { x }

Most code never touches universes — only proof-heavy code and dependently-typed libraries need them. See language/dependent-types.

Defaults on generic parameters

type Config<T = DefaultConfig> is { ... };
type Map<K, V, H: Hasher = FxHasher> is { ... };

The default is used when the caller omits the type argument:

let m: Map<Text, Int> = Map.new();
// H is FxHasher by default

let m: Map<Text, Int, SipHasher> = Map.new();
// H explicitly SipHasher

Coherence and orphan rules

implement P for T is coherent only if either:

T is defined in the current cog, or
P is defined in the current cog.

This is the orphan rule: it keeps two cogs from implementing the same protocol for the same external type in incompatible ways.

Violations are currently reported as a [coherence] warning rather than rejected — the code compiles and runs. See Protocols → Coherence for the diagnostic and what to write instead.

A specialisation hierarchy allows more specific implement blocks to override less specific ones:

implement<T: Display> MyProto for T { ... }          // generic implement block
@specialize
implement MyProto for Text { ... }                    // wins when T = Text

See language/protocols.

Generic unification gotchas

`T: U` instead of `T = U`

T: U is a bound (T implements U). T = U is an equality constraint (T is the same type as U). They look similar but do different things:

where T: Into<U>     // T can be converted to U
where T = U          // T is literally U (restrictive)

Variance

Verum does not expose variance annotations on type parameters. Subtyping between Container<T> and Container<U> requires T = U except for a few standard-library types (&T covariant in T, fn(T) -> U contravariant in T + covariant in U). This keeps the type system simple; at the cost of a few conversions you'd otherwise get for free.

Type inference depth

Deeply nested generics can stall inference. Annotate intermediate types when the solver complains:

let processed: List<Result<Parsed, Error>> =
    raw.iter()
       .map(|x| parse(x))
       .collect();

Type parameters​

Explicit type arguments​

Bounds​

Associated-type bounds​

Conditional implementations​

Per-instantiation dispatch​

Where clauses​

Const generics​

Const expressions in generic positions​

Higher-kinded types (HKT)​

Explicit kind annotations​

Existential types​

Type-level functions​

Meta parameters​

Context parameters​

Rank-2 polymorphism​

Lifetime / region parameters​

Universe polymorphism​

Defaults on generic parameters​

Coherence and orphan rules​

Generic unification gotchas​

T: U instead of T = U​

Variance​

Type inference depth​

See also​