Section 41: Interfaces, Traits, and Behavioral Contracts¶
TECHSPEC-41 — Section 41 · Version 0.1 · Status: Initial Draft
Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.
1. Purpose¶
Interfaces and traits define capabilities that a type promises to provide. They allow functions to work with different concrete types through a shared, explicit contract.
An interface declaration is not proof that an implementation behaves correctly. The compiler must distinguish structural compatibility, contract checking, runtime evidence, and formal proof.
2. Interface Declaration¶
An interface declares required functions, associated types where supported, and behavioral requirements.
Rules: - Interface members must have explicit signatures. - Required effects and failure types must be declared. - Visibility and generic constraints follow the ordinary module and type rules. - An interface cannot silently grant permissions to an implementation.
3. Implementation¶
A type implements an interface explicitly.
TYPE MemoryBuffer IMPLEMENTS Readable:
FUNCTION read(count: Integer) -> Result<ByteList, ReadError>
...
The compiler checks: - Required members exist. - Signatures are compatible. - Parameter and return types satisfy the interface. - Effects do not exceed permitted interface limits. - Required preconditions and postconditions are compatible. - Required associated types and constraints are satisfied.
Implicit interface implementation is excluded from the initial version.
4. Behavioral Compatibility¶
Matching signatures alone is insufficient.
An implementation must not: - Require stronger preconditions than callers are entitled to assume. - Provide weaker postconditions than the interface promises. - Introduce undeclared effects. - Introduce undocumented failure modes that violate the interface contract. - Break invariants required by the interface.
The formal rules for contract refinement must be specified precisely before interfaces are considered fully verified.
5. Traits and Capabilities¶
Traits may describe reusable capabilities, such as equality, ordering, iteration, serialization, or resource cleanup.
Rules: - A trait declares the operations and constraints it requires. - Generic code may rely only on declared trait guarantees. - Trait implementation must be explicit. - Conflicting implementations must be rejected unless a deterministic coherence rule is later defined. - A trait name is not evidence of security, correctness, or performance.
6. Subtyping and Substitutability¶
The initial language should prefer explicit interface implementation over unrestricted inheritance.
Where subtyping is supported: - A subtype must remain usable wherever its declared supertype is expected. - Mutable positions must not permit unsafe type substitution. - Variance rules must be explicit. - Runtime dispatch must preserve the selected implementation's contracts and effects. - The compiler must reject ambiguous dispatch.
Behavioral substitutability is a stronger property than signature compatibility and may require formal reasoning or tests.
7. Default Implementations¶
Default interface or trait implementations may be considered after the basic model is stable.
If supported: - The selected implementation must be deterministic. - Overrides must satisfy the same behavioral requirements. - Default code must declare effects and failures. - Version changes to defaults must be treated as potentially behavior-changing.
8. Verification¶
Reports must distinguish: - Interface signature checked. - Required members found. - Type compatibility checked. - Contract compatibility checked. - Runtime dispatch target resolved. - Behavioral properties tested. - Behavioral properties formally proven. - Properties remaining unknown.
9. MVP Scope¶
The MVP should support explicit interfaces with signatures and basic type checking. Advanced trait composition, inheritance, default implementations, and formal behavioral-subtyping proofs are deferred.
10. Design Goal¶
Interfaces must communicate reliable capabilities, not merely provide names that agents can claim to implement.
Source and related sections¶
Source file: TECHSPEC-41.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.