#lang scribble/doc @(require scribble/manual (planet cce/scheme:4:1/planet)) @(require (for-label scheme (this-package-in main))) @title[#:tag "top"]{Affine Contracts} by @author+email["Jesse Tov" "tov@ccs.neu.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 @link["http://www.ccs.neu.edu/home/tov/pubs/affinecontracts09/"]{ http://www.ccs.neu.edu/home/tov/pubs/affinecontracts09/ } for more information. @itemize{ @item{For license information, please see the file @tt{LICENSE}.} @item{For examples, please see @tt{examples.ss}.} } @section[#:tag "concept"]{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 @scheme[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. @section[#:tag "procedures"]{Affine Procedures} @defmodule/this-package[main] @defthing[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 @scheme[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 @scheme[require]d the abused procedure. } @defform/subs[#:id -o (-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 @scheme[->]. } @defform[#:id -o* (-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 @scheme[->*]. } @section[#:tag "boxes"]{Affine Boxes} @defmodule/this-package[main] We provide facilities for defining new affine box types. @defform*/subs[#:id define-affine-box [(define-affine-box box-name) (define-affine-box box-name contract?)] ([box-name identifier])]{ The first form defines a new type of affine box, by defining four values whose names is derived from the @scheme[box-name]. If @scheme[box-name] is @scheme[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: @schemeblock[ 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 @scheme[X/c] contract has been applied to a value, then accessing it more than once by @scheme[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: @schemeblock[ X/c : contract? ] } @defproc*[([(make-affine-box-type [X symbol?]) (values (All (A) (A -> (X/c A))) (any/c -> boolean?) (All (A) ((X/c A) -> A)) (contract? -> contract?))] [(make-affine-box-type [X symbol?] [c contract?]) (values (c -> X/c) (any/c -> boolean?) (X/c -> c) contract?)] )]{ This is the procedural form of @scheme[define-affine-box]. Rather than define constructor, predicate, selector, and contract, it returns them. } @subsection[#:tag "predefined"]{The Predefined Affine Box Type} We predefine a generic affine box type: @schemeblock[ (define-affine-box affine-box) ] This defines four procedures: @defproc[(make-affine-box [v any/c]) affine-box?]{ Creates a new affine box containing @scheme[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 @scheme[affine-box/c].) } @defproc[(affine-box? [v any/c]) boolean?]{ Predicate for affine boxes. } @defproc[(affine-box-ref [b affine-box?]) any/c]{ Gets the value in an affine box. If the affine box has been wrapped by an affine box contract (say, using @scheme[provide/contract] and @scheme[affine-box/c]), then reading it more then once is a contract violation by the negative party. } @defproc[(affine-box/c [c contract?]) contract?]{ Produces a contract for an affine box, given a contract for the contents of the box. For example, to provide a function @scheme[f] that takes a string and returns a one-shot box containing a number, we could write: @schemeblock[ (provide/contract [f (string? . -> . (affine-box/c number?))]) ] }