Protocols

A protocol is Verum's interface mechanism — a set of method and associated-type signatures that a type can implement. Protocols are the bridge between the static polymorphism you ask for and the dispatch the compiler arranges.

Defining a protocol

type Display is protocol {
    fn fmt(&self, f: &mut Formatter) -> Result<(), FormatError>;
};

type Debug is protocol {
    fn fmt_debug(&self, f: &mut Formatter) -> Result<(), FormatError>;
};

type Iterator is protocol {
    type Item;
    fn next(&mut self) -> Maybe<Self.Item>;
};

• type P is protocol { ... } declares the protocol.
• Method signatures use fn name(...) -> ReturnType with no body.
• Associated types (type Item;) let implementations supply type-level parameters.
• Self refers to the implementing type; Self.Item to its associated type.

warning

protocol P { ... } on its own is not the grammar

The grammar reaches protocol only through a type definition, so type P is protocol { ... } is the whole of the surface. Writing

public protocol P {           // not the grammar
    fn f(&self) -> Int;
}

is nonetheless accepted by the parser, and the file that contains it type-checks clean — which is what makes it worth a warning rather than a footnote. The two forms differ in whether the protocol is exported.

Measured in the standard library: of three protocols written the bare way, one was invisible to every module that mounted it while the other two exported normally. Each name was declared exactly once, so nothing was shadowing anything, and the protocol bodies explain nothing either — a canonical protocol with the same async fn and &mut self members exports fine. The failure surfaced three files away, as an import that could not find a symbol whose declaration was sitting right there in the source.

Use the type form. A source gate now enforces it across core/.

Implementing

implement Display for User {
    fn fmt(&self, f: &mut Formatter) -> Result<(), FormatError> {
        f.write_str(&f"User({self.id})")
    }
}

implement<T> Iterator for Range<T: Numeric + Ord> {
    type Item = T;
    fn next(&mut self) -> Maybe<T> {
        if self.current < self.end {
            let v = self.current;
            self.current = self.current + T.one();
            Maybe.Some(v)
        } else {
            Maybe.None
        }
    }
}

Protocol inheritance

Protocols can extend others:

type Clone is protocol {
    fn clone(&self) -> Self;
};

type Copy  is protocol extends Clone {
    // Marker: types are trivially copyable. No new methods.
};

Default methods

From the real core/base/protocols.vr definition:

type Eq is protocol {
    fn eq(&self, other: &Self) -> Bool;
    fn ne(&self, other: &Self) -> Bool { !self.eq(other) }
};

type Ord is protocol where Self: Eq {
    fn cmp(&self, other: &Self) -> Ordering;

    // Default methods — overridable in implementations.
    fn lt(&self, other: &Self) -> Bool { self.cmp(other) is Less }
    fn le(&self, other: &Self) -> Bool { !(self.cmp(other) is Greater) }
    fn gt(&self, other: &Self) -> Bool { self.cmp(other) is Greater }
    fn ge(&self, other: &Self) -> Bool { !(self.cmp(other) is Less) }
    fn max(self, other: Self) -> Self { if self.ge(&other) { self } else { other } }
    fn min(self, other: Self) -> Self { if self.le(&other) { self } else { other } }
    fn clamp(self, min: Self, max: Self) -> Self { self.max(min).min(max) }
};

A method with a body is a default: an implementation may take it as written or override it. A method without one is required — an implement block must provide it, and a bound T: Ord is a promise to every caller that cmp is there. So Eq asks an implementation for eq alone, and Ord for cmp alone; the other nine methods come for free and are worth overriding only when a type can answer them more directly than the default does.

Specialisation

A generic implementation can have a more specific override:

implement<T: Clone> List<T> {
    fn copy(&self) -> List<T> { ... }        // generic
}

@specialize
implement List<UInt8> {
    fn copy(&self) -> List<UInt8> {
        // memcpy fast path
        ...
    }
}

The compiler runs a coherence phase on every compile, governed by [protocols].coherence in verum.toml (strict by default, with lenient and unchecked available). It enforces three rules:

• Orphan rule — an implementation must live where either the protocol or the type is defined.
• Overlap — two implementations may not apply to the same (protocol, type) pair.
• Opt-in — an overlapping implementation must carry @specialize.

What it does not check is contract equivalence. Nothing verifies that the specialised body satisfies the same contracts as the generic one: the overlap detector, the specialisation lattice, and the SMT coherence verifier all exist, but no compilation phase discharges that metatheorem. A @specialize override that behaves differently from the generic implementation is accepted — keeping the two interchangeable is yours to guarantee.

Associated-type projections — Self.Item

When a protocol declares an associated type, you can project through it from inside any signature on the same protocol or implementation:

type IntoIter is protocol {
    type Item;
    type Iter;
    fn into_iter(self) -> Self.Iter;
};

type Iterator is protocol {
    type Item;
    fn next(&mut self) -> Maybe<Self.Item>;
    fn map<U, F: fn(Self.Item) -> U>(self, f: F) -> Map<Self, F>;
    fn collect<C: FromIter<Self.Item>>(self) -> C;
};

The projection Self.Item is resolved lazily against the implementing type, not against the protocol declaration. The implementer chooses the concrete type:

implement Iterator for Range<Int> {
    type Item = Int;            // Self.Item = Int for Range<Int>
    fn next(&mut self) -> Maybe<Int> { ... }
}

Method-local generics under projection

A protocol method may introduce its own generics, which compose with the protocol's associated types in the same signature:

type Iterator is protocol {
    type Item;
    fn fold<U>(self, init: U, f: fn(U, Self.Item) -> U) -> U;
}

Inside fold, U is method-local (each call site picks one) while Self.Item is implementation-fixed. The compiler keeps the two scopes distinct: a default-method body can mention both without ambiguity, and downstream call sites get the proper substitution chain (Self.Item → implementer's choice; U → caller's choice).

Default-method bodies

Default-method bodies are checked against the projection surface they declare, not the implementer's later refinement. A default body that returns Maybe<Self.Item> is type-checked once at protocol-declaration time and re-instantiated per implementation; the body cannot depend on a specific implementer's Item choice.

Generic associated types (GATs)

An associated type may carry type parameters of its own, so the implementer supplies a type constructor rather than a single type:

type Mapper is protocol {
    type Out<T>;
    fn run<T>(&self, x: T) -> Self.Out<T>;
};

type Box is { v: Int };

implement Mapper for Box {
    type Out<T> = T;

    public fn run<T>(&self, x: T) -> T { x }
}

The implementation must bind the associated type with the same number of parameters the protocol declared. Binding type Out = Int against a declared type Out<T> is a conformance error (E405), reported at the binding.

Lifetimes do not parameterise a GAT

The grammar accepts a lifetime wherever a type parameter may appear, so type Item<'a> parses. It does not mean what the same spelling means in Rust: lifetime annotations in Verum are parsed and discarded — &'static Text and &Text check identically — so an associated type parameterised only by a lifetime is, to the checker, parameterised by nothing. Write the type parameter you actually want to vary.

Static vs dynamic dispatch

Generic bound (static)

Verum has no impl Trait-in-argument-position sugar — write the type parameter and its bound explicitly:

fn draw_each<T: Drawable>(shapes: &[T]) { ... }

• Monomorphised per concrete type.
• Zero overhead.
• Different monomorphisations are different compiled functions.

dyn P (dynamic)

fn draw_each(shapes: &[dyn Drawable]) { ... }

• Single compiled function, virtual dispatch.
• Allows a heterogeneous collection.
• One pointer + one vtable pointer per value.

Rule of thumb: a generic bound unless you need runtime polymorphism.

Negative bounds

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

Reads "T must be Send but must not be Sync." Useful for single-owner-per-thread APIs.

Context protocols

A protocol can be declared as a context:

context protocol Logger {
    fn info(&self, msg: Text);
    fn error(&self, msg: Text);
};

Context protocols can be both required by functions (using [Logger]) and implemented by types that serve as logger backends. See Context system.

Coherence (orphan rule)

An implementation implement P for T is coherent only if either:

• The cog defining the protocol P also defines T, or
• The cog defining T also defines the implementation.

Two cogs both providing an implement P for T leaves downstream calls ambiguous, which is what the rule exists to prevent.

Today the check reports, it does not reject. An orphan implementation compiles and runs, with a diagnostic naming the three cogs involved and suggesting a newtype wrapper:

warning: [coherence] Orphan implementation: `implement Display for Text`
Protocol 'Display' is defined in cog 'Display'
Type 'Text' is defined in cog 'external'
Implementation is in cog 'private'

Write code as though the rule were enforced — a future release is expected to promote this to an error, and the newtype wrapper is the portable form either way.

Marker protocols

Protocols with no methods that communicate a fact to the type checker. From core/base/protocols.vr:

type Send  is protocol { };                       // safe to move across threads
type Sync  is protocol { };                       // safe to share across threads
type Copy  is protocol where Self: Clone { };     // trivial copy semantics
type Sized is protocol { };                       // statically sized
type Unpin is protocol { };                       // can be moved while pinned

The compiler auto-derives these where it can prove them; you can opt out with !Send, !Sync, etc.