Skip to content

Semantic Contracts

Accepted

Accepted for the V1 semantic contract model and public contract reflection helper names.

Catalyst separates structural constraints from semantic contracts. Structural constraints describe checkable shape. Semantic contracts describe explicit behavioral promises that the compiler can partly validate but cannot fully prove.

This document records the accepted V1 semantic contract model and the public helper names used by V1 contract reflection.

Type Values and Naming

Type is the type of a comptime expression that is valid wherever source expects a type expression. Type values may be concrete types or constraint types.

Semantic contract applications are Type values:

Sequence(f32) // Type, semantic contract constraint

Sequence(f32) represents the set of concrete types that explicitly implement that contract instance. dyn Sequence(f32) forms a concrete unsized erased type when the applied contract is dyn-safe. Concreteness, sizedness, structural-constraint status, and contract status are reflected properties of Type values.

Type-like names are capitalized. Comptime functions are lowercase:

Sequence(f32)
satisfies(.{ ... })
Buffer.implements(Sequence(f32))

See Naming Conventions.

Structural vs Semantic

Structural constraints use satisfies(...):

const ReaderLike: Type = satisfies(.{
  read: fn(self: *Self, buf: []u8) usize!
})

satisfies(...) returns a structural constraint Type. It means the type has a compatible shape. It does not imply a semantic promise, a vtable, a runtime interface, layout compatibility, or hidden dispatch.

Semantic contract applications such as Sequence(f32) are also Type values. They mean explicit semantic conformance, not structural matching.

Type values provide an implements(...) method as a comptime conformance predicate:

Buffer.implements(Sequence(f32)) // comptime query

Explicit conformance

A type never implements a semantic contract merely because it happens to have matching members.

Terminology:

  • implements in prose describes the semantic relationship between a type and a contract.
  • T.implements(...) in code is a lowercase comptime conformance predicate and narrowing operation.
  • impl Type as Contract { ... } is the accepted syntax for explicit semantic conformance declarations.

Contract Model

Contracts are ordinary comptime-visible values backed by compiler-provided reflection and introspection. V1 accepts contract as core source syntax for normal contract authoring, while lower-level Type and reflection primitives may support advanced metaprogramming and tooling.

contract(...) { ... } is accepted syntax for a semantic contract type expression, parallel to struct { ... } for concrete aggregate type expressions. It returns a constraint Type. The arguments are required/base contracts; the body declares required operations, default methods, docs, and laws.

The compiler-provided Type and reflection APIs should also be capable of constructing semantic contract Type values with inspectable metadata. Prelude declarations may build on those primitive APIs for advanced metaprogramming, but normal code uses the syntax. Tooling should inspect the resulting Type value.

The authoring model follows the same model as structs. Non-generic contracts are ordinary const bindings to Type values:

const RealtimeSafe = contract {
}

Generic contracts are ordinary comptime functions returning Type values:

fn Sequence(comptime T: Type) => contract(Indexable(T)) {
  fn len(self: *const Self) usize
}

An empty required-contract list may be spelled either contract { ... } or contract() { ... }; docs prefer contract { ... } to mirror struct { ... }. The important constraint is that Sequence(f32) remains an ordinary comptime call returning a semantic contract Type, while the body is ergonomic enough to read like a declaration instead of raw metadata construction.

A contract may define:

  • required functions
  • default methods
  • dependencies on other semantic contracts
  • documentation of semantic laws

Semantic contracts require operations, not fields, in V1. Field-shape requirements belong to structural constraints such as satisfies(...) and mutable_fields(...). Contracts should express field-like behavior through accessor operations such as len(self: *const Self) usize.

Contracts do not declare associated types or associated constants in the Catalyst contract model. Variation is expressed with explicit comptime parameters on the contract-producing function:

Iterator(Item)
Iterable(Item)
Sequence(T)
PartialEq(Other)

This keeps applied contracts as ordinary Type values and avoids a second type-member projection model such as Self.Item. If a later design discovers a concrete need for type members, it should be introduced as a new proposal rather than treated as an assumed future feature.

Contract bodies do not have private helper members in V1. Functions declared in a contract body are part of the contract surface: either required operations or default methods. Private helpers should be ordinary functions near the contract definition.

A function declaration without a body is a required operation. A function declaration with a body is a default method:

fn Sequence(comptime T: Type) => contract(Indexable(T)) {
  fn len(self: *const Self) usize

  fn is_empty(self: *const Self) bool {
    return self.len() == 0
  }
}

Required-operation versus default-method classification is decided by body attachment. A { ... } or => expr body opener attaches to the preceding signature only when it stays on the same logical line as the completed signature, so an operation is bodyless when no body opener is attached there. See Statement Separation.

Contract operation surfaces may not use default parameter values in V1. This applies to required operations and default methods. Defaults are source-level call metadata for ordinary function declarations; contract operation signatures stay complete for implementation checking, static dispatch, and dynamic dispatch. Use ordinary helper functions near the contract when a convenience default is needed.

Same-name operations with distinct callable shapes inside a single contract are blocked on CEP-0004: Function Overloading. Until that design is settled, a contract should use distinct operation names for distinct callable shapes.

Contract operation declarations may have declaration-level comptime guards:

fn contains(self: *const Self, value: *const T) bool
  if T.implements(PartialEq(T))
{
}

The if clause is a compile-time availability guard, not a runtime branch. The guard expression must be a comptime-known bool or Type.Predicate. Operation availability guards are evaluated as part of contract surface computation and may use the full V1 comptime predicate model.

A guarded required operation is required only when the condition is true. A guarded default method participates in the contract method surface only when the condition is true. If a caller tries to use the method when the condition is false, diagnostics should report the failed condition.

Predicate facts follow the model in Predicate Reflection.

Operation guards may reference contract parameters and Self. In a contract definition, Self means the eventual implementing type. During conformance checking and contract-surface computation, guards are evaluated after substituting Self with the concrete implementer type. Predicate values such as T.implements(PartialEq(T)) also provide conformance facts while checking the guarded declaration body.

Operation guards may also inspect the current contract surface being computed:

ContractSurface.current().is_static()
ContractSurface.current().is_dyn()

ContractSurface.current() is a comptime-only reflection context available while evaluating contract operation guards and contract surface metadata. It describes the current applied contract surface, not the contract definition itself. V1 accepts these public helper names:

ContractSurface.current().is_static()
ContractSurface.current().is_dyn()
ContractSurface.current().contract()
ContractSurface.current().implementer()
ContractSurface.current().scope()

Surface-mode guards are an advanced escape hatch. They are expected to be rare; repeated static/dyn surface guards in a public contract should trigger a design-review lint because the contract may be trying to be two unrelated interfaces at once.

ContractSurface.current().is_static() is true for ordinary static contract use and implementation checking. ContractSurface.current().is_dyn() is true while checking or forming a dynamic contract surface, such as a *dyn Contract vtable.

Static-only required operations are allowed when they are guarded out of the dynamic surface. They remain required for static conformance checking, but they are absent from the dynamic vtable and do not by themselves make the applied contract non-dyn-safe. The dynamic surface that remains must still be honest, complete, and non-empty.

Default method bodies are checked against the surface mode in which the default remains active. A default method that remains active in the dynamic surface must not unconditionally call an operation that is absent from that dynamic surface. If a default needs a static-only operation, guard the default method itself to the static surface or guard the call with a directly evaluated comptime surface predicate such as ContractSurface.current().is_static() or ContractSurface.current().is_dyn().

V1 dyn-safety does not require semantic analysis to prove arbitrary control-flow facts inside default method bodies. If the existing comptime evaluator cannot directly prove that the dynamic specialization avoids the static-only operation, the default method must be guarded out of the dynamic surface or the applied contract is not dyn-safe.

This narrow proof rule applies to default method body paths, not to operation availability guards. Operation guards remain ordinary comptime surface computation.

Conformance checking evaluates operation guards for the applied contract instance. If a guarded required operation's condition is false, the operation is absent and the impl does not need to provide it. If the condition is true, the operation is required like any other required operation.

An impl may only provide operations that are present in the applied contract instance's surface. Providing an operation whose guard is false is an error; define an inherent method instead if the concrete type needs that operation outside the contract.

Contracts should be introspectable by comptime code and tooling:

Sequence(f32).is_contract()
Sequence(f32).contract_required_functions()
Sequence(f32).contract_default_functions()
MutableSequence(f32).contract_dependencies()

These contract reflection helper names are frozen public V1 API. Tooling and comptime code that need conformance-specific operation mappings should use Conformance Reflection.

Trusted Semantic Promise

An implementation is a trusted semantic promise. The compiler checks mechanically knowable facts:

  • required operations exist
  • signatures are compatible
  • contract dependencies are satisfied
  • visible conformances are coherent
  • dyn-safety rules are satisfied when forming dyn objects

The compiler does not generally prove semantic laws.

Examples:

  • Eq can require eq, but the compiler cannot prove reflexivity, symmetry, or transitivity.
  • Hash can require hash, but the compiler cannot prove equal values hash equally.
  • Indexable can require at, but the compiler cannot prove every user implementation handles every index according to its documented semantics.

Public contracts should document their laws. Missing law documentation for public contracts should be a lint. Public implementation declarations may also carry docs for surprising or non-obvious behavior.