Types
Verum has a single type-definition form: type T is .... What
Refinement Types
A refinement type is a type together with a predicate that every
Dependent Types
Verum supports full dependent types — types that depend on values.
Linear & Affine types
Exactly-once and at-most-once resources at the type level, enforced at compile time with zero runtime cost.
Universes & proof irrelevance
The Type(n)/Prop hierarchy, predicativity, proof irrelevance, and universe polymorphism.
Row polymorphism
Extensible records with structural, inference-friendly "more fields allowed" typing.
Tensor types
Shape-typed multi-dimensional arrays with compile-time shape checking and zero runtime cost for shape errors.
Protocols
A protocol is Verum's interface mechanism — a set of method and
Generics
Type parameters, bounds, HKT, existentials, kind annotations, context polymorphism, universe polymorphism.
Type Properties
Compile-time type metadata via T.size, T.alignment, T.name, and friends.
Capability Types
Type-safe capability attenuation with `T with [Read, Write, ...]`.