ch:object-calculi: ch:object-calculi
Problem, result, and invariant. Implement the chapter’s finite functional-object examples with late self, persistent override, and runtime minimum annotations. The result is the seven-case report in appendix E. Every evaluation begins only after the runtime method suite has passed its invariant signature check.
Representation. Represent method labels, invariant result signatures, annotated suites, method bodies, and creation strategies as nominal data. Keep the apparent static interface separate from the runtime minimum annotation. Use explicit fuel only to bound the named traces; exhaustion rejects the case.
First complete version. Implement method lookup and invocation so that the selected body receives the current object as self. Implement override by replacing one method while leaving the original suite unchanged. Recompute the receiver for every late- self call, then reproduce the
Remaining cases. Reject a missing method and covariant shared result components before update. Restore the runtime minimum annotation after overriding through a shorter apparent type. Add the iso-recursive fluent point and compare recursive creation with the deliberately frozen-self translation.
A failing version. Build an updated object whose self field still points to the old method suite. The program typechecks, but the recursive-creation case returns zero instead of one. Returning the apparent annotation or accepting any shared result type are independent controls for the static side of the implementation.
Acceptance test. Run the four gates in appendix E. Require seven exact PASS lines and audit output []. Replay the frozen-creation mutation, the wrong apparent annotation, and the covariance mutation. Each must remain type-correct and fail the named oracle case.
Mathematical boundary. The artifact executes the displayed finite typing and reduction calculations. It proves neither substitution, minimum typing, preservation, progress, recursive-object safety, translation simulation, nor full abstraction.