;; Affine contracts as in the paper "Affine Contracts for Affine ;; Types" by Jesse Tov and Riccardo Pucella, as submitted to ICFP'09. #lang scheme ;;;;; ;;;;; Affine procedures ;;;;; ;; affine-procedure/c : contract? ;; Contract for one-shot procedures -- checks that the procedure ;; is applied only once, but isn't concerned with the procedure's ;; domain and range. Can only produce *negative* blame. (define affine-procedure/c (make-proj-contract 'affine-procedure/c (lambda (pos neg src name) (lambda (f) (if (procedure? f) (let ([blessed #t]) (make-keyword-procedure (lambda (keys vals . args) (if blessed (begin (set! blessed #f) (keyword-apply f keys vals args)) (raise-contract-error f src neg name "affine function applied more than once"))))) (raise-contract-error f src pos name "expected affine procedure, given: ~e" f)))) procedure?)) ;; (-o dom ... range) ;; Contract for affine procedures, including domain and range ;; as in -> (define-syntax -o (syntax-rules () [(-o ARGS ...) (and/c (-> ARGS ...) affine-procedure/c)])) ;; (-o* (mandatory-dom ...) (optional-dom ...) rest range) ;; Contract for affine procedues, as in ->* (define-syntax -o* (syntax-rules () [(-o* ARGS ...) (and/c (->* ARGS ...) affine-procedure/c)])) ;;;;; ;;;;; Affine boxes ;;;;; ;; An affine box is represented as a struct containing ;; a thunk that either returns the boxed value or raises ;; a contract error. (define-struct affine-box (unbox)) ;; affine-box* : A -> (affine-box/c A) ;; To construct an affine box from a value. Upon construction, ;; affine boxes *do not check* for affine usage. This is because ;; a module that creates an affine box is responsible to handle ;; it properly. The affine-box/c contract (below) actually enforces ;; that an affine box is read only once. (define (affine-box* val) (make-affine-box (lambda () val))) ;; affine-unbox : (affine-box/c A) -> A ;; To read the value out of an affine box. (define (affine-unbox ab) ((affine-box-unbox ab))) ;; affine-box/c : contract? -> contract? ;; Contract for affine boxes, which takes as an argument a contract ;; for the contents of the box. A box so wrapped may be unboxed ;; at most once. (define (affine-box/c c) (let ([ctc (coerce-contract 'affine-box/c c)]) (make-proj-contract (build-compound-type-name 'affine-box/c c) (lambda (pos neg src name) (lambda (ab) (if (affine-box? ab) (let ([blessed #t]) (make-affine-box (lambda () (if blessed (begin (set! blessed #f) ((((proj-get ctc) ctc) pos neg src name) ((affine-box-unbox ab)))) (raise-contract-error ab src neg name "affine box unboxed more than once"))))) (raise-contract-error ab src pos name "expected affine box, given: ~e" ab)))) affine-box?))) (provide/contract [affine-procedure/c contract?] [affine-box/c (contract? . -> . contract?)] [affine-box? (any/c . -> . boolean?)] [rename affine-box* affine-box (any/c . -> . affine-box?)] [affine-unbox (affine-box? . -> . any/c)]) (provide -o -o*)