add docs
ober
ca395c24e62853775deede1ba8ecf93fdb823ff4
new file mode 100644 --- /dev/null +++ b/docs/gerbil-contracts.md @@ -0,0 +1,853 @@ +# Gerbil Contracts + +This note describes how contracts work in the Gerbil repository, based on the +implementation in `src/gerbil/core/contract.ss`, the runtime support in +`src/gerbil/runtime/interface.ss` and `src/gerbil/runtime/error.ss`, the public +facades in `src/std/contract.ss` and `src/std/interface.ss`, and the usage +patterns in the Gerbil standard library. + +## Short Answer + +Gerbil contracts are not a separate typed version of the language. They are a +gradual, macro-based contract and annotation layer built into the ordinary +Gerbil prelude. + +The same surface forms, `def`, `lambda`, `defclass`, `defstruct`, `defmethod`, +`let`, `do`, and `case-lambda`, are renamed by `src/gerbil/core.ss` to +contract-aware implementations from `src/gerbil/core/contract.ss`. If a form has +no contract syntax, it behaves like normal Gerbil. If it has type or predicate +annotations, the macros add runtime checks, interface casts, dotted access +expansion, and compiler-visible type annotations. + +So the right mental model is: + +- Gerbil remains dynamically typed. +- Contract annotations can check values at runtime. +- Type assertions can tell the compiler what the programmer knows without + checking it. +- Interface contracts are checked at interface method boundaries. +- The compiler consumes the generated type annotations for optimization and for + some static error detection. +- This is closer to gradual contracts plus optimizer type metadata than to a + sound static type system. + +## Where It Lives + +Important files: + +- `src/gerbil/core/contract.ss`: the main macro implementation. +- `src/gerbil/core.ss`: imports `core/contract` and renames contract-aware forms + into the normal prelude. +- `src/std/contract.ss`: compatibility/public shim exporting `using`, + `with-interface`, `with-class`, `with-contract`, and predicate combinators. +- `src/std/interface.ss`: public interface facade exporting `interface`, casts, + predicates, descriptors, and `interface-out`. +- `src/gerbil/runtime/interface.ss`: runtime interface instance machinery. +- `src/gerbil/runtime/error.ss`: `ContractViolation` error class and + `raise-contract-violation-error`. +- `src/gerbil/compiler/optimize-*.ss`: compiler passes that consume + `@type`, `@type.signature`, `@interface`, and MOP annotations. + +The Gerbil docs that match the implementation are: + +- `doc/reference/std/contract.md` +- `doc/reference/std/interface.md` +- `doc/guide/intro.md`, especially the sections on interfaces, contracts, and + type annotations. + +## Prelude Integration + +`src/gerbil/core.ss` imports `core/contract`, then exports the normal names as +renames of contract-aware variants: + +```scheme +(rename: lambda/c lambda) +(rename: case-lambda/c case-lambda) +(rename: let/c let) +(rename: def/c def) +(rename: def*/c def*) +(rename: defmethod/c defmethod) +(rename: defclass/c defclass) +(rename: defstruct/c defstruct) +(rename: do/c do) +(rename: do-while/c do-while) +``` + +That means code can write ordinary-looking Gerbil: + +```scheme +(def (deque-empty? (dq : deque)) + => :boolean + (zero? dq.length)) +``` + +and the prelude expands it through the contract-aware machinery. Plain +definitions without contract syntax still expand as ordinary definitions. + +## Contract Syntax + +The core contract operators are: + +```scheme +(: expr Type) ; checked type cast/check +(:? expr Type) ; checked type cast/check, allowing #f +(:- expr Type) ; unchecked type assertion +(:~ expr predicate) ; checked predicate contract +``` + +In signatures and `using`, the same markers appear attached to variables: + +```scheme +(x : Type) +(x :? Type) +(x :- Type) +(x :~ predicate) +(x :~ predicate :- Type) +(x :~ predicate : Type) +(x :~ predicate :? Type) +``` + +There is also `::-`, which is an internal/publicly visible mode used mainly for +"do not cast this interface value, but still use checked interface method +facades" and for unchecked receiver typing in generated method wrappers. + +Defaulted arguments use `:=`: + +```scheme +(start :~ (in-range? 0 len) :- :fixnum := 0) +``` + +Return types use `=>`: + +```scheme +(def (f (x : :fixnum)) => :fixnum + ...) +``` + +Gerbil's built-in and MOP types are exposed as type identifiers such as +`:t`, `:void`, `:fixnum`, `:procedure`, `:list`, `:vector`, `:string`, and user +class/interface identifiers. + +## Type References + +`deftype` creates a type-reference syntax binding: + +```scheme +(deftype @BufferedReader BufferedReader) +``` + +This is used for forward or recursive references. For example, the standard IO +interfaces create `@BufferedReader` before the `BufferedReader` interface is +fully available, and data structures like deques use `@node` for recursive +slots. + +Internally, the `TypeReference` module resolves type identifiers to either: + +- class metadata, +- interface metadata, or +- another type reference. + +If a type cannot be resolved, expansion raises a syntax error. + +## Checked Type Cast: `:` + +`(: expr Type)` is a checked operation. + +For class and struct types, it expands to a predicate check wrapped in a +`begin-annotation (@type ...)` form. If the value does not satisfy the class +predicate, it raises an error. Special broad types such as `:t` and `:void` do +not need a runtime check. + +For interface types, it expands to an interface cast: + +```scheme +(Interface expr) +``` + +The interface macro itself acts as a constructor/cast macro. The cast creates or +reuses an interface instance wrapper for the underlying object. + +## Maybe Type Cast: `:?` + +`(:? expr Type)` is the nullable variant. It accepts `#f` or a value satisfying +the type. + +For classes, it checks: + +```scheme +(or (not val) (predicate val)) +``` + +For interfaces, it returns `#f` for `#f`, otherwise casts: + +```scheme +(and val (Interface val)) +``` + +This is common for optional slots: + +```scheme +(defstruct conpool (... (max :? :fixnum))) +``` + +## Unchecked Type Assertion: `:-` + +`(:- expr Type)` does not check the value. It emits only a compiler annotation: + +```scheme +(begin-annotation (@type Type::t) expr) +``` + +This is used when the programmer knows the invariant already holds. It is very +common inside method bodies, after an interface has already checked/cast the +receiver, or in hot code where an earlier boundary has done the validation. + +Example from the style used throughout the stdlib: + +```scheme +(using (self :- ExtensibleVector) + (vector-length self.vector)) +``` + +The assertion enables dotted slot access and gives the optimizer type +information, but it does not protect against a wrong value. + +## Predicate Contract: `:~` + +`(:~ expr predicate)` evaluates the expression, applies the predicate, and +raises `ContractViolation` if the predicate returns false. + +It can be combined with type information: + +```scheme +(index :~ nonnegative-fixnum? :- :fixnum) +``` + +That means: + +- check `nonnegative-fixnum?` at runtime when in a checked context, +- then annotate/assert the value as a `:fixnum`. + +The predicate may depend on earlier arguments. Standard IO uses this heavily: + +```scheme +(read (u8v : :u8vector) + (start :~ (in-range? 0 (u8vector-length u8v)) :- :fixnum := 0) + (end :~ (in-range-inclusive? start (u8vector-length u8v)) + :- :fixnum + := (u8vector-length u8v))) +``` + +Here `start` depends on `u8v`, and `end` depends on both `start` and `u8v`. + +## The `using` Form + +`using` is the central local contract/type annotation form: + +```scheme +(using (declaration ...) body ...) +``` + +Declarations can bind an expression or annotate an existing variable: + +```scheme +(using (x expr : Type) body ...) +(using (x : Type) body ...) +(using (x expr :- Type) body ...) +(using (x :- Type) body ...) +(using (x :~ predicate) body ...) +``` + +`using` expands into `with-interface`, `with-class`, or `with-contract` +depending on the target type. + +Effects: + +- `:~` checks a predicate. +- `:` checks/casts the value. +- `:?` checks/casts the value and permits `#f`. +- `:-` only asserts and annotates. +- For classes and structs, the body gains dotted slot access. +- For interfaces, the body gains dotted method calls. +- The compiler receives local type information through a syntax-local + `type-env`. + +Example: + +```scheme +(using ((req : http-request) + (sock req.sock :- StreamSocket)) + ...) +``` + +This checks that `req` is an `http-request`, then asserts that `req.sock` is a +`StreamSocket`. + +## Dotted Access + +The contract layer implements dotted identifiers by rewriting core reference, +application, and assignment forms. + +Inside a typed `using` context: + +```scheme +obj.slot +(obj.method arg ...) +(set! obj.slot value) +``` + +are expanded using the type environment. + +For class or struct types: + +- `obj.slot` expands to the known accessor. +- `(set! obj.slot value)` expands to the known mutator. +- If the slot has a known type, chained dots continue with that type. + +For interface types: + +- `(obj.method arg ...)` expands to either the checked interface facade or the + unchecked `&` facade, depending on whether the local binding was checked. +- Interface dotted references are method calls only; interfaces do not expose + slots. + +The `deep-dots` compiler test demonstrates chained access: + +```scheme +(using (a :- A) + a.x + a.x.y + {a.x.y.do-it 1 2}) +``` + +The expansion can follow slot type metadata from `A.x` to `B.y` to `C`. + +There is also a nil-check convention in dotted names: a dotted part beginning +with `?` causes `check-nil!` to be inserted before dereferencing. + +## Interface Contracts + +Interfaces are a major consumer of contracts. + +An interface declares required methods and optional method contracts: + +```scheme +(interface Sequence + (ref (index :~ nonnegative-fixnum?)) + (set! (index :~ nonnegative-fixnum?) value) + (length)) +``` + +The `interface` macro generates: + +- an interface class/type descriptor, +- an interface runtime descriptor, +- a cast constructor such as `Sequence`, +- a try-cast constructor such as `try-Sequence`, +- an exact interface-instance predicate such as `Sequence?`, +- a satisfiability predicate such as `is-Sequence?`, +- checked method facades such as `Sequence-ref`, +- unchecked method facades such as `&Sequence-ref`, +- compile-time `interface-info` metadata. + +Checked interface method facades do contract checks and casts at the interface +boundary, then call the unchecked facade. The unchecked facade assumes the +receiver is an exact interface instance and that arguments satisfy the contract. + +This design makes method implementations simpler. The implementation can assume +that interface callers have crossed the contract boundary: + +```scheme +(defmethod {ref ExtensibleVector} + (lambda (self index) + (using (self :- ExtensibleVector) + ...))) +``` + +The method does not re-check `index` if `ref` is only called through the +contracted interface. + +## Interface Runtime Model + +The runtime implementation is in `src/gerbil/runtime/interface.ss`. + +An interface instance is a small wrapper containing: + +- the original object, +- resolved method implementations for the object's concrete class. + +When an object is cast to an interface: + +1. If it is already an exact instance of that interface, it is returned. +2. If it is another interface instance, the runtime unwraps the original object + and recasts it. +3. Otherwise, the runtime checks whether the object's class has all required + methods. +4. It creates a prototype interface instance for the pair + `(interface type, object class)`. +5. That prototype is cached in a table. +6. Future casts for the same interface/class pair clone the cached prototype. + +This is why interfaces are not just a type-checking feature. They are also a +dispatch optimization mechanism. Interface calls can avoid repeated dynamic +method lookup because the relevant method procedures are resolved when the +object crosses the interface boundary. + +## Interface Mixins + +Interfaces can mix in other interfaces: + +```scheme +(interface (Reader Closer) + ...) +``` + +The macro linearizes mixins, folds inherited method signatures, checks +signature compatibility for duplicate methods, and emits subtype method +facades. If interface `B` mixes `A`, a `B` instance also has `A` methods. + +The runtime method descriptor stores method-name alternatives so mixed-in +interfaces can resolve methods from the correct namespace. + +## Checked and Unchecked Facades + +Gerbil consistently generates checked and unchecked operations. + +For interfaces: + +- `Interface-method`: checked facade. +- `&Interface-method`: unchecked facade. + +For class/struct slots with contracts: + +- normal mutators may be checked, +- raw/unchecked mutators are generated for internal use, +- dotted assignment chooses checked or unchecked mutators depending on the + local `using` mode and slot contract metadata. + +For contracted functions: + +- the public function is checked, +- an internal `__name` function may hold the unchecked body, +- optimizer annotations can redirect known-safe calls to the unchecked + function. + +Unchecked paths are important for performance, but they are only correct after a +checked boundary or other trusted proof. + +## Contract-Aware Definitions + +The prelude's normal `def` is really `def/c`. + +With no contract syntax: + +```scheme +(def (f x) body ...) +``` + +it behaves like a normal definition. + +With argument or return contracts: + +```scheme +(def (f (x : :fixnum) (y :~ string?)) => :string + body ...) +``` + +it expands into a checked wrapper plus an unchecked implementation when possible. + +The wrapper: + +- carries an `@type.signature` annotation, +- checks argument contracts through `using`, +- calls the unchecked implementation, +- annotates/checks the return type. + +The unchecked implementation: + +- receives arguments after the checked wrapper has validated them, +- uses unchecked contract mode for its body, +- still carries return type metadata. + +For keyword signatures, Gerbil uses a single checked definition rather than the +same unchecked split, because keyword dispatch complicates the unchecked call +path. + +## Return Type Annotations + +Return annotations use: + +```scheme +(def (f args ...) => Type + body ...) +``` + +These annotations are not just documentation. They generate +`@type.signature` metadata and can be checked by compiler passes. + +For example, the compiler regression test `bad-return-type.ss` defines: + +```scheme +(def (bad x y) => :procedure + (cons x y)) +``` + +and expects compilation to fail because the body returns a pair where the +signature says `:procedure`. + +This is one place where the system behaves statically. But it is not a complete +static type checker; it is a compiler pass using available type annotations and +inference. + +## `lambda`, `case-lambda`, `let`, and Loops + +The same contract syntax works in lambdas: + +```scheme +(lambda ((x : :fixnum)) => :fixnum + ...) +``` + +`case-lambda/c` supports contracted clauses, with restrictions: optionals and +keywords are not allowed in case-lambda clause checking paths. + +Named `let` is contract-aware: + +```scheme +(let lp (((n :- node) dq.back) + ((r :- :list) [])) + => :list + ...) +``` + +`do` and `do-while` are similarly rewritten so loop variables can carry +contracts/type annotations. + +## Contracted Classes and Structs + +`defclass` and `defstruct` are renamed to contract-aware `defclass/c` and +`defstruct/c`. + +Slots can carry contracts: + +```scheme +(defstruct conpool ((connect :- :procedure) + (mx :- :mutex) + (cv :- :condvar) + (conns :- :list) + (out :- :list) + (max :? :fixnum)) + constructor: :init! + final: #t) +``` + +The macro records: + +- slot types, +- slot contracts, +- slot defaults, +- accessors, +- mutators, +- unchecked accessors, +- unchecked mutators. + +If slots have contracts and no custom constructor prevents synthesis, the macro +generates a constructor using `def/c`, so construction checks slot contracts. + +For contracted slots, mutators are also generated through `def/c`: + +```scheme +(def/c (slot-set! ($obj : type) (slot contract ...)) => :void + ...) +``` + +This means slot writes through checked mutators enforce the slot contract. +Unchecked mutators remain available for trusted internal expansion paths. + +Slot type metadata is also what makes dotted slot chaining work. + +## Contract Compatibility in Inheritance + +For classes and interfaces, inherited slot and method contracts are checked for +compatibility. + +The contract implementation computes class precedence lists and interface +precedence lists, then validates subtype relationships. It uses rules like: + +- a subclass slot type can refine a superclass slot type if it is compatible in + the class/interface precedence relation, +- incompatible slot contracts raise syntax errors, +- duplicate interface method signatures must be compatible, +- return types must agree after resolving type references. + +Predicate-only contracts are harder to prove statically, so Gerbil mostly +combines or preserves them as runtime checks. + +## Contracted Methods + +`defmethod` is renamed to `defmethod/c`. + +For class methods, a method body written as a lambda can use contracted +arguments: + +```scheme +(defmethod {:init! conpool} + (lambda (self (connect : :procedure) (max :? :fixnum := #f)) + ...)) +``` + +For interface methods, `defmethod/c` can use an `interface:` declaration. It +checks the implementation against the interface method signature, rewrites the +receiver, and generates a compatible lambda/c implementation. + +This is how Gerbil connects ordinary methods to interface method contracts while +keeping implementations efficient. + +## Mutable Bindings + +`defmutable` and `defmutable*` create mutable top-level bindings with checked +setters. + +Example shape: + +```scheme +(defmutable multicall-default 'help : :symbol) +``` + +The macro creates a hidden storage binding and a setter: + +```scheme +(def/c (multicall-default-set! (new-value : :symbol)) + ...) +``` + +`defmutable` also installs identifier syntax so ordinary `set!` goes through the +checked setter. `defmutable*` exposes accessor/setter procedures instead. + +## Predicate Combinators + +The contract layer defines small predicate-combinator macros: + +```scheme +(maybe pred) ; #f or pred +(in-range? start end) ; fixnum in [start, end) +(in-range-inclusive? s e) ; fixnum in [s, e] +(list-of? pred) ; list whose elements satisfy pred +``` + +These are used heavily in interface signatures, especially IO buffer bounds. + +## Runtime Errors + +Contract failures raise `ContractViolation`, defined in +`src/gerbil/runtime/error.ss`. + +The helper `raise-contract-violation-error` records: + +- a message, +- a source/context string, +- the contract expression, +- the offending value. + +The `contract-violation!` macro captures source location when possible and +emits an abort annotation so the compiler knows the path does not return. + +Nil dereference checks use the same error path with a distinct message. + +Interface cast failures raise `CastError`, defined in +`src/gerbil/runtime/interface.ss`. + +## Compiler Annotations + +Contracts emit annotations consumed by compiler optimization passes: + +```scheme +(@type Type) +(@type.signature ...) +(@interface Type methods) +(@mop.class ...) +(@mop.accessor ...) +(@mop.mutator ...) +(@abort) +``` + +The optimizer uses these annotations to: + +- collect top-level type information, +- record class and interface metadata, +- infer lambda signatures, +- check return types, +- check some call argument types, +- optimize predicate checks away when the expression type is already known, +- optimize accessors and mutators into direct structure operations, +- redirect checked calls to unchecked implementations when the arguments are + statically known to satisfy the signature. + +The compiler intentionally falls back to runtime checks when it lacks enough +information. In `optimize-call.ss`, if expression type information is missing, +too broad, or only maybe compatible, Gerbil does not reject the program; it lets +the runtime contract boundary handle it. + +That design confirms that contracts are gradual and opportunistic, not a fully +static typed dialect. + +## Static Behavior That Does Exist + +Although Gerbil contracts are not a full static type system, the compiler does +perform meaningful static checks when annotations make facts available. + +Examples: + +- incompatible return type annotations can fail compilation, +- calls to known non-procedures can fail compilation, +- calls to known procedures can be arity/type checked, +- class slot type conflicts can be syntax errors, +- interface duplicate method signatures must be compatible, +- dotted references fail at expansion time if the typed slot or method does not + exist, +- invalid type identifiers fail at expansion time. + +This is best described as "typed metadata plus runtime contracts" rather than +"Typed Gerbil". + +## How the Standard Library Uses Contracts + +Common patterns in `src/std`: + +1. Public boundaries use checked contracts. + + Example: IO interfaces check buffer types and bounds at the method boundary. + +2. Internal method bodies use `:-` after a boundary has already checked the + receiver. + + Example: + + ```scheme + (using (self :- websocket) + ...) + ``` + +3. Data structures annotate slots for optimizer and dotted access. + + Example: + + ```scheme + (defstruct deque ((front :- node) + (back :- node) + (length :- :fixnum))) + ``` + +4. Optional values use `:?`. + + Example: + + ```scheme + (max :? :fixnum) + ``` + +5. Recursive types use `deftype`. + + Example: + + ```scheme + (deftype @node node) + (defstruct node (e (prev :- @node) (next :- @node))) + ``` + +6. Interface-heavy code casts once and then uses dotted method calls. + + Example: + + ```scheme + (using (sock (tcp-listen laddr) : ServerSocket) + (using (client (sock.accept) : StreamSocket) + ...)) + ``` + +7. Hot loops use assertions after validation. + + Example: + + ```scheme + (:- cp.max :fixnum) + ``` + +## Performance Model + +Contracts cost runtime checks at checked boundaries. Gerbil reduces that cost +with three strategies: + +1. Put checks at interface/procedure boundaries, not repeatedly inside method + bodies. +2. Generate unchecked internal implementations and call them when safe. +3. Feed type metadata to the compiler so it can remove redundant checks and use + direct access operations. + +Interfaces add a second performance benefit: casting resolves the required +methods for the concrete class and caches an interface prototype. Subsequent +interface calls dispatch through slots in the interface instance rather than +doing dynamic method lookup each time. + +## Practical Semantics by Marker + +| Marker | Meaning | Runtime check? | Compiler info? | Typical use | +| --- | --- | --- | --- | --- | +| `:` | checked type/class/interface contract | yes | yes | public boundary, interface cast | +| `:?` | checked nullable type/class/interface contract | yes, unless `#f` | yes | optional slot or argument | +| `:-` | unchecked type assertion | no | yes | internal code after validation | +| `:~` | predicate contract | yes | no type unless combined | value refinements | +| `::-` | do not cast/assert receiver, but use checked method behavior where relevant | partial/contextual | yes | generated interface/class internals | +| `:=` | default argument value | n/a | n/a | optional and keyword args | + +## Not Racket-Style Blame Contracts + +Gerbil contracts are not Racket's full contract system. + +There is no evidence in the inspected implementation of full higher-order blame +tracking, positive/negative blame parties, or chaperone-style wrapping as the +central model. Gerbil's system is more direct: + +- macro expansion adds checks, +- failures raise `ContractViolation`, +- interface casts create optimized interface instances, +- compiler annotations carry type information. + +This matches Gerbil's performance-oriented object/interface system. + +## Answer to the Typed-Language Question + +Gerbil contracts are "typed" in the sense that they let ordinary Gerbil code +attach class, interface, primitive, and predicate constraints to variables, +slots, arguments, and return values. The compiler understands many of those +constraints. + +They are not a typed version of Gerbil in the sense of a separate, statically +checked language tier. They do not require every binding to have a type, they do +not reject every possible type mismatch at compile time, and the implementation +explicitly preserves runtime checks when static information is incomplete. + +A precise summary: + +> Gerbil contracts are a gradual contract and type-annotation system integrated +> into the normal language. Checked forms enforce contracts at runtime; +> unchecked assertions feed the compiler and dotted syntax; interfaces use +> contracts as optimized method-boundary checks. The compiler opportunistically +> uses the annotations for static diagnostics and optimization, but Gerbil +> remains dynamically typed. + +## Implications for Jerboa + +If Jerboa borrows this model, the key pieces to copy are: + +- contract-aware normal forms instead of a separate typed syntax island, +- a local `using` form that both checks/asserts and opens ergonomic field/method + access, +- clear checked versus unchecked paths, +- type metadata that the compiler can consume opportunistically, +- interface/protocol boundary checks rather than deep checks in hot methods, +- first-class runtime errors with source/context and offending value. + +If Jerboa wants a true typed tier, that is a different project. Gerbil's +contract system is a good bridge toward one, but it is not itself the same thing +as a sound static type system.