diff --git a/collects/scheme/contract.ss b/collects/scheme/contract.ss index e4925763a8..3db9925075 100644 --- a/collects/scheme/contract.ss +++ b/collects/scheme/contract.ss @@ -27,6 +27,7 @@ differences from v3: check-procedure check-procedure/more) (except-out (all-from-out "private/contract.ss") + ∃? check-between/c check-unary-between/c)) diff --git a/collects/scheme/exists/lang.ss b/collects/scheme/exists/lang.ss new file mode 100644 index 0000000000..5867514509 --- /dev/null +++ b/collects/scheme/exists/lang.ss @@ -0,0 +1,255 @@ +#lang scheme + +(require "../private/contract.ss") + +;; this code builds the list of predicates (in case it changes, this may need to be re-run) +#; +(define predicates + (let ([fn (build-path (collection-path "scheme") + "compiled" + "main_ss.zo")]) + (let-values ([(vars stx) + (module-compiled-exports + (parameterize ([read-accept-compiled #t]) + (call-with-input-file fn read)))]) + + (filter (λ (sym) + (let ([str (symbol->string sym)]) + (and (not (equal? str "")) + (regexp-match #rx"[?]$" str) + (not (regexp-match #rx"[=<>][?]$" str))))) + (map car (cdr (assoc 0 vars))))))) + + +(define-for-syntax predicates + '(absolute-path? + arity-at-least? + bitwise-bit-set? + boolean? + box? + byte-pregexp? + byte-ready? + byte-regexp? + byte? + bytes-converter? + bytes? + channel? + char-alphabetic? + char-blank? + char-graphic? + char-iso-control? + char-lower-case? + char-numeric? + char-punctuation? + char-ready? + char-symbolic? + char-title-case? + char-upper-case? + char-whitespace? + char? + class? + compiled-expression? + compiled-module-expression? + complete-path? + complex? + cons? + continuation-mark-set? + continuation-prompt-available? + continuation-prompt-tag? + continuation? + contract-first-order-passes? + contract-stronger? + contract? + custodian-box? + custodian-memory-accounting-available? + custodian? + custom-write? + date-dst? + date? + dict-can-functional-set? + dict-can-remove-keys? + dict-mutable? + dict? + directory-exists? + empty? + eof-object? + ephemeron? + eq? + equal? + eqv? + even? + evt? + exact-integer? + exact-nonnegative-integer? + exact-positive-integer? + exact? + exn:break? + exn:fail:contract2? + exn:fail:contract:arity? + exn:fail:contract:continuation? + exn:fail:contract:divide-by-zero? + exn:fail:contract:variable? + exn:fail:contract? + exn:fail:filesystem:exists? + exn:fail:filesystem:version? + exn:fail:filesystem? + exn:fail:network? + exn:fail:object? + exn:fail:out-of-memory? + exn:fail:read:eof? + exn:fail:read:non-char? + exn:fail:read? + exn:fail:syntax? + exn:fail:unsupported? + exn:fail:user? + exn:fail? + exn:misc:match? + exn:srclocs? + exn? + false? + file-exists? + file-stream-port? + fixnum? + flat-contract? + flat-pred? + generic? + handle-evt? + hash-eq? + hash-eqv? + hash-has-key? + hash-placeholder? + hash-weak? + hash? + identifier? + immutable? + implementation? + inexact-real? + inexact? + input-port? + inspector? + integer? + interface-extension? + interface? + internal-definition-context? + is-a? + keyword? + link-exists? + list? + log-level? + log-receiver? + logger? + member-name-key? + method-in-interface? + module-path-index? + module-path? + module-provide-protected? + mpair? + name-pred? + namespace-anchor? + namespace? + negative? + null? + number? + object-method-arity-includes? + object? + odd? + output-port? + pair? + parameter? + parameterization? + path-for-some-system? + path-string? + path? + placeholder? + port-closed? + port-provides-progress-evts? + port-writes-atomic? + port-writes-special? + port? + positive? + pregexp? + pretty-print-style-table? + primitive-closure? + primitive? + procedure-arity-includes? + procedure-arity? + procedure-closure-contents-eq? + procedure-struct-type? + procedure? + proj-pred? + promise-forced? + promise-running? + promise? + pseudo-random-generator? + rational? + readtable? + real? + regexp-match-exact? + regexp-match? + regexp? + relative-path? + rename-transformer? + resolved-module-path? + security-guard? + semaphore-try-wait? + semaphore? + sequence? + set!-transformer? + special-comment? + srcloc? + string? + stronger-pred? + struct-accessor-procedure? + struct-constructor-procedure? + struct-mutator-procedure? + struct-predicate-procedure? + struct-type-property? + struct-type? + struct? + subclass? + subprocess? + symbol-interned? + symbol? + syntax-local-transforming-module-provides? + syntax-original? + syntax-transforming? + syntax? + system-big-endian? + tcp-accept-ready? + tcp-listener? + tcp-port? + terminal-port? + thread-cell? + thread-dead? + thread-group? + thread-running? + thread? + udp-bound? + udp-connected? + udp? + unit? + unknown? + variable-reference? + vector? + void? + weak-box? + will-executor? + zero?)) + +(define-syntax (predicates/provide stx) + (with-syntax ([(predicates ...) predicates] + [(-predicates ...) (map (λ (x) (string->symbol (format "-~a" x))) predicates)]) + #'(begin + (define -predicates + (let ([predicates (λ (x) + (if (∃? x) + (error 'predicates "supplied with a wrapped value ~e" x) + (predicates x)))]) + predicates)) + ... + (provide (rename-out (-predicates predicates) ...) + (except-out (all-from-out scheme) + define-struct + predicates ...))))) + +(predicates/provide) diff --git a/collects/scheme/exists/lang/reader.ss b/collects/scheme/exists/lang/reader.ss new file mode 100644 index 0000000000..ecc1919151 --- /dev/null +++ b/collects/scheme/exists/lang/reader.ss @@ -0,0 +1,2 @@ +#lang s-exp syntax/module-reader +scheme/exists/lang \ No newline at end of file diff --git a/collects/scheme/private/contract.ss b/collects/scheme/private/contract.ss index 3995cbc26b..3bb1ef893f 100644 --- a/collects/scheme/private/contract.ss +++ b/collects/scheme/private/contract.ss @@ -16,7 +16,8 @@ improve method arity mismatch contract violation error messages? define/contract with-contract current-contract-region - new-∃/c) + new-∃/c + ∃?) (require (for-syntax scheme/base) (for-syntax "contract-opt-guts.ss") @@ -2654,8 +2655,10 @@ improve method arity mismatch contract violation error messages? #:property stronger-prop (λ (this that) #f)) +(define-struct ∃ ()) + (define (new-∃/c raw-name) (define name (string->symbol (format "~a/∃" raw-name))) (define-values (struct-type constructor predicate accessor mutator) - (make-struct-type name #f 1 0)) + (make-struct-type name struct:∃ 1 0)) (make-∃/c constructor (λ (x) (accessor x 0)) predicate raw-name)) diff --git a/collects/scribblings/guide/contracts-exists.scrbl b/collects/scribblings/guide/contracts-exists.scrbl new file mode 100644 index 0000000000..7dc549ad05 --- /dev/null +++ b/collects/scribblings/guide/contracts-exists.scrbl @@ -0,0 +1,60 @@ +#lang scribble/doc +@(require scribble/manual + scribble/eval + "guide-utils.ss" + "contracts-utils.ss" + (for-label scheme/contract)) + +@title[#:tag "contracts-exists"]{Abstract Contracts using @scheme[#:exists] and @scheme[#:∃]} + +The contract system provides existential contracts that can +protect abstractions, ensuring that clients of your module +cannot depend on the precise representation choices you make +for your data structures. + +@ctc-section{Getting started, with a stack example} + +@margin-note{ + You can type @scheme[#:exists] instead of @scheme[#:∃] if you +cannot easily type unicode characters; in DrScheme, typing +@tt{\exists} followed by either alt-\ or control-\ (depending +on your platform) will produce @scheme[∃].}. +The @scheme[provide/contract] form allows you to write +@schemeblock[#:∃ name-of-a-new-contract] as one of its clauses. This declaration +introduces the variable @scheme[name-of-a-new-contract], binding it to a new +contract that hides information about the values it protects. + +As an example, consider this (simple) implementation of a stack datastructure: +@schememod[scheme + (define empty '()) + (define (enq top queue) (append queue (list top))) + (define (next queue) (car queue)) + (define (deq queue) (cdr queue)) + (define (empty? queue) (null? queue)) + + (provide/contract + [empty (listof integer?)] + [enq (-> integer? (listof integer?) (listof integer?))] + [next (-> (listof integer?) integer?)] + [deq (-> (listof integer?) (listof integer?))] + [empty? (-> (listof integer?) boolean?)])] +This code implements a queue purely in terms of lists, meaning that clients +of this data structure might use @scheme[car] and @scheme[cdr] directly on the +data structure (perhaps accidentally) and thus any change in the representation +(say to a more efficient representation that supports amortized constant time +enqueue and dequeue operations) might break client code. + +To ensure that the stack representation is abstact, we can use @scheme[#:∃] in the +@scheme[provide/contract] expression, like this: +@schemeblock[(provide/contract + #:∃ stack + [empty stack] + [enq (-> integer? stack stack)] + [next (-> stack integer?)] + [deq (-> stack (listof integer?))] + [empty? (-> stack boolean?)])] + +Now, if clients of the data structure try to use @scheme[car] and @scheme[cdr], they +receive an error, rather than mucking about with the internals of the queues. + +See also @ctc-link["exists-gotcha"]. diff --git a/collects/scribblings/guide/contracts-gotchas.scrbl b/collects/scribblings/guide/contracts-gotchas.scrbl index 3483a0912a..5eb5c91e06 100644 --- a/collects/scribblings/guide/contracts-gotchas.scrbl +++ b/collects/scribblings/guide/contracts-gotchas.scrbl @@ -52,6 +52,27 @@ the @scheme[eq?] call would return @scheme[#t]. Moral: do not use @scheme[eq?] on values that have contracts. +@ctc-section[#:tag "exists-gotcha"]{Exists contracts and predicates} + +Much like the @scheme[eq?] example above, @scheme[#:∃] contracts +can change the behavior of a program. + +Specifically, +the @scheme[null?] predicate (and many other predicates) return @scheme[#f] +for @scheme[#:∃] contracts, and changing one of those contracts to @scheme[any/c] +means that @scheme[null?] might now return @scheme[#t] instead, resulting in +arbitrarily different behavior depending on this boolean might flow around +in the program. + +@defmodulelang[scheme/exists] + +To work around the above problem, the +@schememodname[scheme/exists] library behaves just like the @schememodname[scheme], +but where predicates signal errors when given @scheme[#:∃] contracts. + +Moral: do not use predicates on @scheme[#:∃] contracts, but if you're not sure, use +@schememodname[scheme/exists] to be safe. + @ctc-section{Defining recursive contracts} When defining a self-referential contract, it is natural to use diff --git a/collects/scribblings/guide/contracts.scrbl b/collects/scribblings/guide/contracts.scrbl index b72183307b..27c0851f4b 100644 --- a/collects/scribblings/guide/contracts.scrbl +++ b/collects/scribblings/guide/contracts.scrbl @@ -40,5 +40,6 @@ update string-pad-center to show examples via REPL notation: @include-section["contracts-simple-function.scrbl"] @include-section["contracts-general-function.scrbl"] @include-section["contracts-structure.scrbl"] +@include-section["contracts-exists.scrbl"] @include-section["contracts-examples.scrbl"] @include-section["contracts-gotchas.scrbl"]