1 The Main Idea
2 Affine Procedures
affine-procedure/ c
3 Affine Boxes
affine-box/ c

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.

For license information, please see the file LICENSE.

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

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)
dom = dom-expr
  | (keyword dom-expr)
range = range-expr
  | (values range-expr ...)
  | any

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)


3 Affine Boxes

(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-unbox 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?))])