Affine Contracts
by Jesse Tov <tov at ccs dot neu dot edu>
This package provides affine contracts, based on the paper “Affine Contracts for Affine Types” by Jesse A. Tov and Riccardo Pucella, as submitted to ICFP’09. See http://www.ccs.neu.edu/home/tov/pubs/affinecontracts09/ for more information.
For license information, please see the file LICENSE.
For examples, please see examples.ss.
1 The Main Idea
This package allows library authors to protect affine values provided from their libraries from multiple uses. We assume that the author of a library is responsible for correct single-threading within the modules that they write (or for whatever must be done to preserve invariants). The contract combinators exported by this package allow imposing affine constraints on other modules by way of provide/contract, but they do nothing to enforce affinity within a module. We believe this is the appropriate way to do things in the context of the PLT Scheme contract system.
The package supports two kinds of affine contracts: for procedures, and for general values. Because procedures have behavior when applied, it is possible to wrap them to get additional behavior, such as checking that they have not been applied before. Arbitrary values, however, do not necessary have a way to add behavior for when they are “used.” Thus, we support affine contracts for non-procedural values by wrapping them in opaque boxes which may be unboxed (dereferenced) only once. Obviously this does nothing to protect the value once unboxed. However, a library may provide functions that both produce and consume affine boxes, and a client of that library will then be responsible not to alias those boxes before passing them back; otherwise, the library responsible for the aliasing will be blamed.
2 Affine Procedures
| (require (planet tov/affine-contracts:2:0/main)) |
| affine-procedure/c : contract? |
A contract for a function that can be applied at most once. The contract checks immediately that the value is a procedure?, and allows the procedure to be applied once. If it is applied further times, a contract error blames the negative party — that is, the module that required the abused procedure.
| (-o dom range) | ||||||||||||||||||||||||||||||
|
Produces a contract for a one-shot function with the given domain and range in the style of ->.
| (-o* (mandatory-dom ) (optional-dom ) rest range) |
Produces a contract for a one-shot function with the given domain and range in the style of ->*.
3 Affine Boxes
| (require (planet tov/affine-contracts:2:0/main)) |
We provide facilities for defining new affine box types.
| (define-affine-box box-name) | |||||
| (define-affine-box box-name contract?) | |||||
|
The first form defines a new type of affine box, by defining four values whose names is derived from the box-name. If box-name is X, then it defines a constructor, a predicate, an accessor, and a “contract maker” that takes as an argument a contract for the contents of the box:
| make-X : All (A) (A -> (X/c A)) |
| X? : any/c -> boolean? |
| X-ref : All (A) ((X/c A) -> A) |
| X/c : contract? -> contract? |
If an X/c contract has been applied to a value, then accessing it more than once by X-ref is a contract violation.
The second form allows for providing a contract for the contents of the box, in which case the new box contract is no longer parameterized, and uses the provided contract for the contents of the box:
X/c : contract?
| |||||||||
| X : symbol? | |||||||||
| |||||||||
| X : symbol? | |||||||||
| c : contract? |
This is the procedural form of define-affine-box. Rather than define constructor, predicate, selector, and contract, it returns them.
3.1 The Predefined Affine Box Type
We predefine a generic affine box type:
(define-affine-type affine-box)
This defines four procedures:
| (make-affine-box v) → affine-box? |
| v : any/c |
Creates a new affine box containing v. (Note that an affine box may be unboxed an unlimited amount of time until it has been wrapped by an affine box contract by affine-box/c.)
| (affine-box? v) → boolean? |
| v : any/c |
Predicate for affine boxes.
| (affine-box-ref b) → any/c |
| b : affine-box? |
Gets the value in an affine box. If the affine box has been wrapped by an affine box contract (say, using provide/contract and affine-box/c), then reading it more then once is a contract violation by the negative party.
| (affine-box/c c) → contract? |
| c : contract? |
Produces a contract for an affine box, given a contract for the contents of the box. For example, to provide a function f that takes a string and returns a one-shot box containing a number, we could write:
(provide/contract [f (string? . -> . (affine-box/c number?))])