more rackty guide, through the contracts section
This commit is contained in:
parent
7ed0d4e00a
commit
2f5b166073
|
@ -6,7 +6,7 @@
|
||||||
(for-label racket/contract)
|
(for-label racket/contract)
|
||||||
(for-label racket/gui))
|
(for-label racket/gui))
|
||||||
|
|
||||||
@title[#:tag "contracts-examples"]{Examples}
|
@title[#:tag "contracts-examples"]{Additional Examples}
|
||||||
|
|
||||||
This section illustrates the current state of Racket's contract
|
This section illustrates the current state of Racket's contract
|
||||||
implementation with a series of examples from @italic{Design by
|
implementation with a series of examples from @italic{Design by
|
||||||
|
@ -59,7 +59,7 @@ Note: To mimic Mitchell and McKim's informal notion of parametericity
|
||||||
places, this use of first-class contracts improves on Mitchell and McKim's
|
places, this use of first-class contracts improves on Mitchell and McKim's
|
||||||
design (see comments in interfaces).
|
design (see comments in interfaces).
|
||||||
|
|
||||||
@section{A Customer Manager Component for Managing Customer Relationships}
|
@section{A Customer-Manager Component}
|
||||||
|
|
||||||
This first module contains some struct definitions in a
|
This first module contains some struct definitions in a
|
||||||
separate module in order to better track bugs.
|
separate module in order to better track bugs.
|
||||||
|
|
|
@ -3,29 +3,29 @@
|
||||||
scribble/eval
|
scribble/eval
|
||||||
"guide-utils.ss"
|
"guide-utils.ss"
|
||||||
"contracts-utils.ss"
|
"contracts-utils.ss"
|
||||||
(for-label scheme/contract))
|
(for-label racket/contract))
|
||||||
|
|
||||||
@title[#:tag "contracts-exists"]{Abstract Contracts using @scheme[#:exists] and @scheme[#:∃]}
|
@title[#:tag "contracts-exists"]{Abstract Contracts using @racket[#:exists] and @racket[#:∃]}
|
||||||
|
|
||||||
The contract system provides existential contracts that can
|
The contract system provides existential contracts that can
|
||||||
protect abstractions, ensuring that clients of your module
|
protect abstractions, ensuring that clients of your module
|
||||||
cannot depend on the precise representation choices you make
|
cannot depend on the precise representation choices you make
|
||||||
for your data structures.
|
for your data structures.
|
||||||
|
|
||||||
@ctc-section{Getting Started, with a Stack Example}
|
#; @ctc-section{Getting Started, with a Stack Example}
|
||||||
|
|
||||||
@margin-note{
|
@margin-note{
|
||||||
You can type @scheme[#:exists] instead of @scheme[#:∃] if you
|
You can type @racket[#:exists] instead of @racket[#:∃] if you
|
||||||
cannot easily type unicode characters; in DrScheme, typing
|
cannot easily type unicode characters; in DrRacket, typing
|
||||||
@tt{\exists} followed by either alt-\ or control-\ (depending
|
@tt{\exists} followed by either alt-\ or control-\ (depending
|
||||||
on your platform) will produce @scheme[∃].}
|
on your platform) will produce @racket[∃].}
|
||||||
The @scheme[provide/contract] form allows you to write
|
The @racket[provide/contract] form allows you to write
|
||||||
@schemeblock[#:∃ _name-of-a-new-contract] as one of its clauses. This declaration
|
@racketblock[#:∃ _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
|
introduces the variable @racket[_name-of-a-new-contract], binding it to a new
|
||||||
contract that hides information about the values it protects.
|
contract that hides information about the values it protects.
|
||||||
|
|
||||||
As an example, consider this (simple) implementation of a stack datastructure:
|
As an example, consider this (simple) implementation of a stack datastructure:
|
||||||
@schememod[scheme
|
@racketmod[racket
|
||||||
(define empty '())
|
(define empty '())
|
||||||
(define (enq top queue) (append queue (list top)))
|
(define (enq top queue) (append queue (list top)))
|
||||||
(define (next queue) (car queue))
|
(define (next queue) (car queue))
|
||||||
|
@ -39,14 +39,14 @@ As an example, consider this (simple) implementation of a stack datastructure:
|
||||||
[deq (-> (listof integer?) (listof integer?))]
|
[deq (-> (listof integer?) (listof integer?))]
|
||||||
[empty? (-> (listof integer?) boolean?)])]
|
[empty? (-> (listof integer?) boolean?)])]
|
||||||
This code implements a queue purely in terms of lists, meaning that clients
|
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
|
of this data structure might use @racket[car] and @racket[cdr] directly on the
|
||||||
data structure (perhaps accidentally) and thus any change in the representation
|
data structure (perhaps accidentally) and thus any change in the representation
|
||||||
(say to a more efficient representation that supports amortized constant time
|
(say to a more efficient representation that supports amortized constant time
|
||||||
enqueue and dequeue operations) might break client code.
|
enqueue and dequeue operations) might break client code.
|
||||||
|
|
||||||
To ensure that the stack representation is abstact, we can use @scheme[#:∃] in the
|
To ensure that the stack representation is abstact, we can use @racket[#:∃] in the
|
||||||
@scheme[provide/contract] expression, like this:
|
@racket[provide/contract] expression, like this:
|
||||||
@schemeblock[(provide/contract
|
@racketblock[(provide/contract
|
||||||
#:∃ stack
|
#:∃ stack
|
||||||
[empty stack]
|
[empty stack]
|
||||||
[enq (-> integer? stack stack)]
|
[enq (-> integer? stack stack)]
|
||||||
|
@ -54,7 +54,7 @@ To ensure that the stack representation is abstact, we can use @scheme[#:∃] in
|
||||||
[deq (-> stack (listof integer?))]
|
[deq (-> stack (listof integer?))]
|
||||||
[empty? (-> stack boolean?)])]
|
[empty? (-> stack boolean?)])]
|
||||||
|
|
||||||
Now, if clients of the data structure try to use @scheme[car] and @scheme[cdr], they
|
Now, if clients of the data structure try to use @racket[car] and @racket[cdr], they
|
||||||
receive an error, rather than mucking about with the internals of the queues.
|
receive an error, rather than mucking about with the internals of the queues.
|
||||||
|
|
||||||
See also @ctc-link["exists-gotcha"].
|
See also @ctc-link["exists-gotcha"].
|
||||||
|
|
|
@ -9,66 +9,15 @@
|
||||||
|
|
||||||
@title[#:tag "contracts-general-functions"]{Contracts on Functions in General}
|
@title[#:tag "contracts-general-functions"]{Contracts on Functions in General}
|
||||||
|
|
||||||
@ctc-section[#:tag "flat-named-contracts"]{Contract Error Messages that Contain ``???''}
|
The @racket[->] contract constructor works for functions that take a
|
||||||
|
fixed number of arguments and where the result contract is independent
|
||||||
You wrote your module. You added contracts. You put them into the interface
|
of the input arguments. To support other kinds of functions, Racket
|
||||||
so that client programmers have all the information from interfaces. It's a
|
supplies additional contract constructors, notable @racket[->].
|
||||||
piece of art:
|
|
||||||
@racketmod[
|
|
||||||
racket
|
|
||||||
|
|
||||||
(provide/contract
|
|
||||||
[deposit (-> (lambda (x)
|
|
||||||
(and (number? x) (integer? x) (>= x 0)))
|
|
||||||
any)])
|
|
||||||
|
|
||||||
(define this 0)
|
|
||||||
(define (deposit a) ...)
|
|
||||||
]
|
|
||||||
|
|
||||||
Several clients used your module. Others used their
|
|
||||||
modules in turn. And all of a sudden one of them sees this error
|
|
||||||
message:
|
|
||||||
|
|
||||||
@inset-flow{@racketerror{bank-client broke the contract (-> ??? any)
|
|
||||||
it had with myaccount on deposit; expected <???>, given: -10}}
|
|
||||||
|
|
||||||
Clearly, @racket[bank-client] is a module that uses @racket[myaccount]
|
|
||||||
but what is the @racketerror{???} doing there? Wouldn't it be nice if
|
|
||||||
we had a name for this class of data much like we have string, number,
|
|
||||||
and so on?
|
|
||||||
|
|
||||||
For this situation, Racket provides @deftech{flat named
|
|
||||||
contracts}. The use of ``contract'' in this term shows that contracts
|
|
||||||
are first-class values. The ``flat'' means that the collection of data
|
|
||||||
is a subset of the built-in atomic classes of data; they are described
|
|
||||||
by a predicate that consumes all Racket values and produces a
|
|
||||||
boolean. The ``named'' part says what we want to do, which is to name
|
|
||||||
the contract so that error messages become intelligible:
|
|
||||||
|
|
||||||
@racketmod[
|
|
||||||
racket
|
|
||||||
|
|
||||||
(define (amount? x) (and (number? x) (integer? x) (>= x 0)))
|
|
||||||
(define amount (flat-named-contract 'amount amount?))
|
|
||||||
|
|
||||||
(provide/contract
|
|
||||||
[deposit (amount . -> . any)])
|
|
||||||
|
|
||||||
(define this 0)
|
|
||||||
(define (deposit a) ...)
|
|
||||||
]
|
|
||||||
|
|
||||||
With this little change, the error message becomes all of the
|
|
||||||
sudden quite readable:
|
|
||||||
|
|
||||||
@inset-flow{@racketerror{bank-client broke the contract (-> amount
|
|
||||||
any) it had with myaccount on deposit; expected <amount>, given: -10}}
|
|
||||||
|
|
||||||
@ctc-section[#:tag "optional"]{Optional Arguments}
|
@ctc-section[#:tag "optional"]{Optional Arguments}
|
||||||
|
|
||||||
Take a look at this excerpt from a string-processing module, inspired by the
|
Take a look at this excerpt from a string-processing module, inspired by the
|
||||||
@link["http://racketcookbook.org"]{Racket cookbook}:
|
@link["http://schemecookbook.org"]{Scheme cookbook}:
|
||||||
|
|
||||||
@racketmod[
|
@racketmod[
|
||||||
racket
|
racket
|
||||||
|
@ -104,6 +53,7 @@ point here is the formulation of the contract for the
|
||||||
|
|
||||||
|
|
||||||
The contract combinator @racket[->*], demands several groups of contracts:
|
The contract combinator @racket[->*], demands several groups of contracts:
|
||||||
|
|
||||||
@itemize[
|
@itemize[
|
||||||
@item{The first one is a parenthesized group of contracts for all required
|
@item{The first one is a parenthesized group of contracts for all required
|
||||||
arguments. In this example, we see two: @racket[string?] and
|
arguments. In this example, we see two: @racket[string?] and
|
||||||
|
@ -115,64 +65,57 @@ arguments: @racket[char?]. }
|
||||||
@item{The last one is a single contract: the result of the function.}
|
@item{The last one is a single contract: the result of the function.}
|
||||||
]
|
]
|
||||||
|
|
||||||
Note if a default value does not satisfy a contract, you
|
Note if a default value does not satisfy a contract, you won't get a
|
||||||
won't get a contract error for this interface. In contrast
|
contract error for this interface. If you can't trust yourself to get
|
||||||
to type systems, we do trust you; if you can't trust
|
the initial value right, you need to communicate the initial value
|
||||||
yourself, you need to communicate across boundaries for
|
across a boundary.
|
||||||
everything you write.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "rest-args"]{Rest Arguments}
|
@ctc-section[#:tag "rest-args"]{Rest Arguments}
|
||||||
|
|
||||||
We all know that @racket[+] in Beginner Racket is a function
|
The @racket[max] operator consumes at least one real number, but it
|
||||||
that consumes at least two numbers but, in principle,
|
accepts any number of additional arguments. You can write other such
|
||||||
arbitrarily many more. Defining the function is easy:
|
functions using a ``rest'' argument, such as in @racket[max-abs]:
|
||||||
@racketblock[
|
|
||||||
(define (plus fst snd . rst)
|
@margin-note{See @secref["rest-args"] for an introduction to rest
|
||||||
(foldr + (+ fst snd) rst))
|
arguments.}
|
||||||
]
|
|
||||||
Describing this function via a contract is difficult because of the rest
|
@racketblock[
|
||||||
argument (@racket[rst]).
|
(define (max-abs n . rst)
|
||||||
|
(foldr (lambda (n m) (max (abs n) m)) (abs n) rst))
|
||||||
|
]
|
||||||
|
|
||||||
|
Describing this function through a contract requires a further
|
||||||
|
extension of @racket[->*]: a @racket[#:rest] keyword specifies a
|
||||||
|
contract on a list of arguments after the required and optional
|
||||||
|
arguments:
|
||||||
|
|
||||||
Here is the contract:
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[plus (->* (number? number?) () #:rest (listof number?) number?)])
|
[max-abs (->* (real?) () #:rest (listof real?) real?)])
|
||||||
]
|
|
||||||
The @racket[->*] contract combinator empowers you to specify
|
|
||||||
functions that consume a variable number of arguments or functions like
|
|
||||||
@racket[plus], which consume ``at least this number'' of arguments but
|
|
||||||
an arbitrary number of additional arguments.
|
|
||||||
|
|
||||||
The contracts for the required arguments are enclosed in the first
|
|
||||||
pair of parentheses:
|
|
||||||
@racketblock[
|
|
||||||
(number? number?)
|
|
||||||
]
|
]
|
||||||
|
|
||||||
For @racket[plus] they demand two numbers. The empty pair of
|
As always for @racket[->*], the contracts for the required arguments
|
||||||
parenthesis indicates that there are no optional arguments
|
are enclosed in the first pair of parentheses, which in this case is a
|
||||||
(not counting the rest arguments) and the contract for the
|
single real number. The empty pair of parenthesis indicates that there
|
||||||
rest argument follows @racket[#:rest]
|
are no optional arguments (not counting the rest arguments). The
|
||||||
@racketblock[
|
contract for the rest argument follows @racket[#:rest]; since all
|
||||||
(listof number?)
|
additional arguments must be real numbers, the list of rest arguments
|
||||||
]
|
must satisfy the contract @racket[(listof real?)].
|
||||||
Since the remainder of the actual arguments are collected
|
|
||||||
in a list for a rest parameter such as @racket[rst], the
|
|
||||||
contract demands a list of values; in this specific
|
|
||||||
examples, these values must be numbers.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "keywords"]{Keyword Arguments}
|
@ctc-section[#:tag "keywords"]{Keyword Arguments}
|
||||||
|
|
||||||
Sometimes, a function accepts many arguments and remembering
|
It turns out that the @racket[->] contract constructor also contains
|
||||||
their order can be a nightmare. To help with such functions,
|
support for keyword arguments. For example, consider this function,
|
||||||
Racket has @seclink["lambda-keywords"]{keyword} arguments.
|
which creates a simple GUI and asks the user a yes-or-no question:
|
||||||
|
|
||||||
|
@margin-note{See @secref["lambda-keywords"] for an introduction to
|
||||||
|
keyword arguments.}
|
||||||
|
|
||||||
For example, consider this function that creates a simple
|
|
||||||
GUI and asks the user a yes-or-no question:
|
|
||||||
@racketmod[
|
@racketmod[
|
||||||
racket/gui
|
racket/gui
|
||||||
|
|
||||||
(define (ask-yes-or-no-question #:question question
|
(define (ask-yes-or-no-question question
|
||||||
#:default answer
|
#:default answer
|
||||||
#:title title
|
#:title title
|
||||||
#:width w
|
#:width w
|
||||||
|
@ -194,41 +137,43 @@ racket/gui
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[ask-yes-or-no-question
|
[ask-yes-or-no-question
|
||||||
(-> #:question string?
|
(-> string?
|
||||||
#:default boolean?
|
#:default boolean?
|
||||||
#:title string?
|
#:title string?
|
||||||
#:width exact-integer?
|
#:width exact-integer?
|
||||||
#:height exact-integer?
|
#:height exact-integer?
|
||||||
boolean?)])
|
boolean?)])
|
||||||
]
|
]
|
||||||
@margin-note{Note that if you really want to ask a yes-or-no
|
|
||||||
question via a GUI, you should use
|
|
||||||
@racket[message-box/custom] (and generally speaking,
|
|
||||||
avoiding the responses ``yes'' and ``no'' in your dialog is a
|
|
||||||
good idea, too ...).}
|
|
||||||
|
|
||||||
The contract for @racket[ask-yes-or-no-question] uses our
|
@margin-note{If you really want to ask a yes-or-no question
|
||||||
old friend the @racket[->] contract combinator. Just like
|
via a GUI, you should use @racket[message-box/custom]. For that
|
||||||
@racket[lambda] (or @racket[define]-based functions) use
|
matter, it's usually better to provide buttons with more specific
|
||||||
keywords for specifying keyword arguments, it uses keywords
|
answers than ``yes'' and ``no.''}
|
||||||
for specifying contracts on keyword arguments. In this case,
|
|
||||||
it says that @racket[ask-yes-or-no-question] must receive
|
The contract for @racket[ask-yes-or-no-question] uses @racket[->], and
|
||||||
five keyword arguments, one for each of the keywords
|
in the same way that @racket[lambda] (or @racket[define]-based
|
||||||
@racket[#:question],
|
functions) allows a keyword to precede a functions formal argument,
|
||||||
|
@racket[->] allows a keyword to precede a function contract's argument
|
||||||
|
contract. In this case,
|
||||||
|
the contract says that @racket[ask-yes-or-no-question] must receive four keyword
|
||||||
|
arguments, one for each of the keywords
|
||||||
@racket[#:default],
|
@racket[#:default],
|
||||||
@racket[#:title],
|
@racket[#:title],
|
||||||
@racket[#:width], and
|
@racket[#:width], and
|
||||||
@racket[#:height].
|
@racket[#:height].
|
||||||
Also, just like in a function definition, the keywords in
|
As in a function definition, the order of the keywords in @racket[->]
|
||||||
the @racket[->] may appear in any order.
|
relative to each other does not matter for clients of the function;
|
||||||
|
only the relative order of argument contracts without keywords
|
||||||
|
matters.
|
||||||
|
|
||||||
@ctc-section[#:tag "optional-keywords"]{Optional Keyword Arguments}
|
@ctc-section[#:tag "optional-keywords"]{Optional Keyword Arguments}
|
||||||
|
|
||||||
Of course, many of the parameters in
|
Of course, many of the parameters in
|
||||||
@racket[ask-yes-or-no-question] (from the previous question)
|
@racket[ask-yes-or-no-question] (from the previous question)
|
||||||
have reasonable defaults, and should be made optional:
|
have reasonable defaults and should be made optional:
|
||||||
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(define (ask-yes-or-no-question #:question question
|
(define (ask-yes-or-no-question question
|
||||||
#:default answer
|
#:default answer
|
||||||
#:title [title "Yes or No?"]
|
#:title [title "Yes or No?"]
|
||||||
#:width [w 400]
|
#:width [w 400]
|
||||||
|
@ -237,17 +182,18 @@ have reasonable defaults, and should be made optional:
|
||||||
]
|
]
|
||||||
|
|
||||||
To specify this function's contract, we need to use
|
To specify this function's contract, we need to use
|
||||||
@racket[->*]. It too supports keywords just as you might
|
@racket[->*] again. It supports keywords just as you might
|
||||||
expect, in both the optional and mandatory argument
|
expect in both the optional and mandatory argument
|
||||||
sections. In this case, we have mandatory keywords
|
sections. In this case, we have the mandatory keyword
|
||||||
@racket[#:question] and @racket[#:default], and optional keywords
|
@racket[#:default] and optional keywords
|
||||||
@racket[#:title],
|
@racket[#:title],
|
||||||
@racket[#:width], and
|
@racket[#:width], and
|
||||||
@racket[#:height]. So, we write the contract like this:
|
@racket[#:height]. So, we write the contract like this:
|
||||||
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[ask-yes-or-no-question
|
[ask-yes-or-no-question
|
||||||
(->* (#:question string?
|
(->* (string?
|
||||||
#:default boolean?)
|
#:default boolean?)
|
||||||
|
|
||||||
(#:title string?
|
(#:title string?
|
||||||
|
@ -256,71 +202,182 @@ sections. In this case, we have mandatory keywords
|
||||||
|
|
||||||
boolean?)])
|
boolean?)])
|
||||||
]
|
]
|
||||||
putting the mandatory keywords in the first section and the
|
|
||||||
optional ones in the second section.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "arrow-d"]{When a Function's Result Depends on its Arguments}
|
That is, we put the mandatory keywords in the first section, and we
|
||||||
|
put the optional ones in the second section.
|
||||||
|
|
||||||
Here is an excerpt from an imaginary (pardon the pun) numerics module:
|
|
||||||
|
|
||||||
@racketmod[
|
@ctc-section[#:tag "case-lambda"]{Contracts for @racket[case-lambda]}
|
||||||
racket
|
|
||||||
(provide/contract
|
A function defined with @racket[case-lambda] might impose different
|
||||||
[sqrt.v1 (->d ([argument (>=/c 1)])
|
constraints on its arguments depending on how many are provided. For
|
||||||
()
|
example, a @racket[report-cost] function might convert either a pair
|
||||||
[result (<=/c argument)])])
|
or numbers or a string into a new string:
|
||||||
...
|
|
||||||
|
@margin-note{See @secref["case-lambda"] for an introduction to
|
||||||
|
@racket[case-lambda].}
|
||||||
|
|
||||||
|
@def+int[
|
||||||
|
(define report-cost
|
||||||
|
(case-lambda
|
||||||
|
[(lo hi) (format "between $~a and $~a" lo hi)]
|
||||||
|
[(desc) (format "~a of dollars" desc)]))
|
||||||
|
(report-cost 5 8)
|
||||||
|
(report-cost "millions")
|
||||||
]
|
]
|
||||||
|
|
||||||
The contract for the exported function @racket[sqrt.v1] uses the
|
The contract for such a function is formed with the @racket[case->]
|
||||||
@racket[->d] rather than @racket[->] function contract. The ``d''
|
combinator, which combines as many functional contracts as needed:
|
||||||
stands for @italic{dependent} contract, meaning the contract for the
|
@racketblock[
|
||||||
function range depends on the value of the argument.
|
(provide/contract
|
||||||
|
[report-cost
|
||||||
|
(case->
|
||||||
|
(integer? integer? . -> . string?)
|
||||||
|
(string? . -> . string?))])
|
||||||
|
]
|
||||||
|
As you can see, the contract for @racket[report-cost] combines two
|
||||||
|
function contracts, which is just as many clauses as the explanation
|
||||||
|
of its functionality required.
|
||||||
|
|
||||||
In this particular case, the argument of @racket[sqrt.v1] is greater
|
@;{
|
||||||
or equal to 1. Hence a very basic correctness check is that the result is
|
This isn't supported anymore (yet...?). -robby
|
||||||
smaller than the argument. (Naturally, if this function is critical, one
|
|
||||||
could strengthen this check with additional clauses.)
|
In the case of @racket[substring1], we also know that the indices
|
||||||
|
that it consumes ought to be natural numbers less than the length of the
|
||||||
|
given string. Since @racket[case->] just combines arrow contracts,
|
||||||
|
adding such constraints is just a matter of strengthening the individual
|
||||||
|
contracts:
|
||||||
|
<racket>
|
||||||
|
(provide/contract
|
||||||
|
[substring1 (case->
|
||||||
|
(string? . -> . string?)
|
||||||
|
(->r ([s string?]
|
||||||
|
[_ (and/c natural-number/c (</c (string-length s)))])
|
||||||
|
string?)
|
||||||
|
(->r ([s string?]
|
||||||
|
[a (and/c natural-number/c (</c (string-length s)))]
|
||||||
|
[o (and/c natural-number/c
|
||||||
|
(>=/c a)
|
||||||
|
(</c (string-length s)))])
|
||||||
|
string?))])
|
||||||
|
</racket>
|
||||||
|
Here we used @racket[->r] to name the parameters and express the
|
||||||
|
numeric constraints on them.
|
||||||
|
}
|
||||||
|
|
||||||
|
@ctc-section[#:tag "arrow-d"]{Argument and Result Dependencies}
|
||||||
|
|
||||||
|
The following is an excerpt from an imaginary numerics module:
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(provide/contract
|
||||||
|
[real-sqrt (->d ([argument (>=/c 1)])
|
||||||
|
()
|
||||||
|
[result (<=/c argument)])])
|
||||||
|
]
|
||||||
|
|
||||||
|
The contract for the exported function @racket[real-sqrt] uses the
|
||||||
|
@racket[->d] rather than @racket[->*] function contract. The ``d''
|
||||||
|
stands for a @italic{dependent} contract, meaning the contract for the
|
||||||
|
function range depends on the value of the argument. In this
|
||||||
|
particular case, the argument of @racket[real-sqrt] is greater or
|
||||||
|
equal to 1, so a very basic correctness check is that the result is
|
||||||
|
smaller than the argument.
|
||||||
|
|
||||||
In general, a dependent function contract looks just like
|
In general, a dependent function contract looks just like
|
||||||
the more general @racket[->*] contract, but with names added
|
the more general @racket[->*] contract, but with names added
|
||||||
that can be used elsewhere in the contract.
|
that can be used elsewhere in the contract.
|
||||||
|
|
||||||
|
@;{
|
||||||
Yes, there are many other contract combinators such as @racket[<=/c]
|
Yes, there are many other contract combinators such as @racket[<=/c]
|
||||||
and @racket[>=/c], and it pays off to look them up in the contract
|
and @racket[>=/c], and it pays off to look them up in the contract
|
||||||
section of the reference manual. They simplify contracts tremendously
|
section of the reference manual. They simplify contracts tremendously
|
||||||
and make them more accessible to potential clients.
|
and make them more accessible to potential clients.
|
||||||
|
}
|
||||||
|
|
||||||
@ctc-section[#:tag "arrow-d-args"]{When Contract Arguments Depend on Each Other}
|
Going back to the back-account example, suppose that we generalize the
|
||||||
|
module to support multiple accounts and that we also include a
|
||||||
|
withdrawal operation. The improved bank-account module includes a
|
||||||
|
@racket[account] structure type and the following functions:
|
||||||
|
|
||||||
Eventually bank customers want their money back. Hence, a module that
|
|
||||||
implements a bank account must include a method for withdrawing money. Of
|
|
||||||
course, ordinary accounts don't let customers withdraw an arbitrary amount of
|
|
||||||
money but only as much as they have in the account.
|
|
||||||
|
|
||||||
Suppose the account module provides the following two functions:
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
balance : (-> account amount)
|
(provide/contract
|
||||||
withdraw : (-> account amount account)
|
[balance (-> account? amount/c)]
|
||||||
|
[withdraw (-> account? amount/c account?)]
|
||||||
|
[deposit (-> account? amount/c account?)])
|
||||||
]
|
]
|
||||||
Then, informally, the proper precondition for @racket[withdraw] is that
|
|
||||||
``the balance of the given account is greater than or equal to the given (withdrawal) amount.''
|
|
||||||
The postcondition is similar to the one for
|
|
||||||
@ctc-link["flat-named-contracts"]{@racket[deposit]}:
|
|
||||||
``the balance of the resulting account is larger than (or equal to) the one of the
|
|
||||||
given account.''
|
|
||||||
You could of course also formulate a full-fledged correctness condition, namely,
|
|
||||||
that the balance of the resulting account is equal to the balance of the given
|
|
||||||
one, plus the given amount.
|
|
||||||
|
|
||||||
The following module implements accounts imperatively and specifies the
|
Besides requiring that a client provide a valid amount for a
|
||||||
conditions we just discussed:
|
withdrawal, however, the amount should be less than the specified
|
||||||
|
account's balance, and the resulting account will have less money than
|
||||||
|
it started with. Similarly, the module might promise that a deposit
|
||||||
|
produces an account with money added to the account. The following
|
||||||
|
implementation enforces those constraints and guarantees through
|
||||||
|
contracts:
|
||||||
|
|
||||||
@racketmod[
|
@racketmod[
|
||||||
racket
|
racket
|
||||||
|
|
||||||
(code:comment "section 1: the contract definitions")
|
(code:comment "section 1: the contract definitions")
|
||||||
(define-struct account (balance) #:mutable)
|
(struct account (balance))
|
||||||
(define amount natural-number/c)
|
(define amount/c natural-number/c)
|
||||||
|
|
||||||
|
(code:comment "section 2: the exports")
|
||||||
|
(provide/contract
|
||||||
|
[create (amount/c . -> . account?)]
|
||||||
|
[balance (account? . -> . amount/c)]
|
||||||
|
[withdraw (->d ([acc account?]
|
||||||
|
[amt (and/c amount/c (<=/c (balance acc)))])
|
||||||
|
()
|
||||||
|
[result (and/c account?
|
||||||
|
(lambda (res)
|
||||||
|
(>= (balance res)
|
||||||
|
(- (balance acc) amt))))])]
|
||||||
|
[deposit (->d ([acc account?]
|
||||||
|
[amt amount/c])
|
||||||
|
()
|
||||||
|
[result (and/c account?
|
||||||
|
(lambda (res)
|
||||||
|
(>= (balance res)
|
||||||
|
(+ (balance acc) amt))))])])
|
||||||
|
|
||||||
|
(code:comment "section 3: the function definitions")
|
||||||
|
(define balance account-balance)
|
||||||
|
|
||||||
|
(define (create amt) (account amt))
|
||||||
|
|
||||||
|
(define (withdraw a amt)
|
||||||
|
(account (- (account-balance a) amt)))
|
||||||
|
|
||||||
|
(define (deposit a amt)
|
||||||
|
(account (+ (account-balance a) amt)))
|
||||||
|
]
|
||||||
|
|
||||||
|
The contracts in section 2 provide typical type-like guarantees for
|
||||||
|
@racket[create] and @racket[balance]. For @racket[withdraw] and
|
||||||
|
@racket[deposit], however, the contracts check and guarantee the more
|
||||||
|
complicated constraints on @racket[balance] and @racket[deposit]. The
|
||||||
|
contract on the second argument to @racket[withdraw] uses
|
||||||
|
@racket[(balance acc)] to check whether the supplied withdrawal amount
|
||||||
|
is small enough, where @racket[acc] is the name given within
|
||||||
|
@racket[->d] to the function's first argument. The contract on the
|
||||||
|
result of @racket[withdraw] uses both @racket[acc] and @racket[amt] to
|
||||||
|
guarantee that no more than that requested amount was withdrawn. The
|
||||||
|
contract on @racket[deposit] similarly uses @racket[acc] and
|
||||||
|
@racket[amount] in the result contract to guarantee that at least as
|
||||||
|
much money as provided was deposited into the account.
|
||||||
|
|
||||||
|
As written above, when a contract check fails, the error message is
|
||||||
|
not great. The following revision uses @racket[flat-named-contract]
|
||||||
|
within a helper function @racket[mk-account-contract] to provide
|
||||||
|
better error messages.
|
||||||
|
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
|
(code:comment "section 1: the contract definitions")
|
||||||
|
(struct account (balance))
|
||||||
|
(define amount/c natural-number/c)
|
||||||
|
|
||||||
(define msg> "account a with balance larger than ~a expected")
|
(define msg> "account a with balance larger than ~a expected")
|
||||||
(define msg< "account a with balance less than ~a expected")
|
(define msg< "account a with balance less than ~a expected")
|
||||||
|
@ -333,70 +390,30 @@ racket
|
||||||
|
|
||||||
(code:comment "section 2: the exports")
|
(code:comment "section 2: the exports")
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[create (amount . -> . account?)]
|
[create (amount/c . -> . account?)]
|
||||||
[balance (account? . -> . amount)]
|
[balance (account? . -> . amount/c)]
|
||||||
[withdraw (->d ([acc account?]
|
[withdraw (->d ([acc account?]
|
||||||
[amt (and/c amount (<=/c (balance acc)))])
|
[amt (and/c amount/c (<=/c (balance acc)))])
|
||||||
()
|
()
|
||||||
[result (mk-account-contract acc amt >= msg>)])]
|
[result (mk-account-contract acc amt >= msg>)])]
|
||||||
[deposit (->d ([acc account?]
|
[deposit (->d ([acc account?]
|
||||||
[amt amount])
|
[amt amount/c])
|
||||||
()
|
()
|
||||||
[result (mk-account-contract acc amt <= msg<)])])
|
[result (mk-account-contract acc amt <= msg<)])])
|
||||||
|
|
||||||
(code:comment "section 3: the function definitions")
|
(code:comment "section 3: the function definitions")
|
||||||
(define balance account-balance)
|
(define balance account-balance)
|
||||||
|
|
||||||
(define (create amt) (make-account amt))
|
(define (create amt) (account amt))
|
||||||
|
|
||||||
(define (withdraw acc amt)
|
(define (withdraw a amt)
|
||||||
(set-account-balance! acc (- (balance acc) amt))
|
(account (- (account-balance a) amt)))
|
||||||
acc)
|
|
||||||
|
|
||||||
(define (deposit acc amt)
|
(define (deposit a amt)
|
||||||
(set-account-balance! acc (+ (balance acc) amt))
|
(account (+ (account-balance a) amt)))
|
||||||
acc)
|
|
||||||
]
|
]
|
||||||
|
|
||||||
The second section is the export interface: @itemize[
|
@ctc-section[#:tag "arrow-d-eval-order"]{Checking State Changes}
|
||||||
@item{@racket[create] consumes an initial deposit and
|
|
||||||
produces an account. This kind of contract is just like a
|
|
||||||
type in a statically typed language, except that statically
|
|
||||||
typed languages usually don't support the type ``natural
|
|
||||||
numbers'' (as a full-fledged subtype of numbers). }
|
|
||||||
|
|
||||||
@item{@racket[balance] consumes an account and computes its current balance.}
|
|
||||||
|
|
||||||
@item{@racket[withdraw] consumes an account, named @racket[acc], and an
|
|
||||||
amount, @racket[amt]. In addition to being an @racket[amount], the
|
|
||||||
latter must also be less than @racket[(balance acc)], i.e., the balance of
|
|
||||||
the given account. That is, the contract for @racket[amt] depends on the
|
|
||||||
value of @racket[acc], which is what the @racket[->d]
|
|
||||||
contract combinator expresses.
|
|
||||||
|
|
||||||
The result contract is formed on the fly:
|
|
||||||
@racket[(mk-account-contract acc amt > msg>)].
|
|
||||||
It is an application of a contract-producing function that
|
|
||||||
consumes an account, an amount, a comparison operator, and an error message (a
|
|
||||||
format string). The result is a contract.
|
|
||||||
}
|
|
||||||
|
|
||||||
@item{@racket[deposit]'s contract has been reformulated using the
|
|
||||||
@racket[->d] combinator. }
|
|
||||||
]
|
|
||||||
|
|
||||||
The code in the first section defines all those pieces that
|
|
||||||
are needed for the formulation of the export contracts:
|
|
||||||
@racket[account?], @racket[amount], error messages (format
|
|
||||||
strings), and @racket[mk-account-contract]. The latter is a
|
|
||||||
function that extracts the current balance from the given
|
|
||||||
account and then returns a named contract, whose error
|
|
||||||
message (contract name) is a string that refers to this
|
|
||||||
balance. The resulting contract checks whether an account
|
|
||||||
has a balance that is larger or smaller, depending on the
|
|
||||||
given comparison operator, than the original balance.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "arrow-d-eval-order"]{Ensuring that a Function Properly Modifies State}
|
|
||||||
|
|
||||||
The @racket[->d] contract combinator can also ensure that a
|
The @racket[->d] contract combinator can also ensure that a
|
||||||
function only modifies state according to certain
|
function only modifies state according to certain
|
||||||
|
@ -451,70 +468,6 @@ contrast, if the contract for @racket[f] were
|
||||||
(only changing the underscore to @racket[res]), then
|
(only changing the underscore to @racket[res]), then
|
||||||
the result of @racket[get-x] would be @racket['(ctc f)].
|
the result of @racket[get-x] would be @racket['(ctc f)].
|
||||||
|
|
||||||
@ctc-section[#:tag "case-lambda"]{Contracts for @racket[case-lambda]}
|
|
||||||
|
|
||||||
Dybvig, in Chapter 5 of the
|
|
||||||
@link["http://www.racket.com/csug/"]{Chez Racket User's Guide},
|
|
||||||
explains the meaning and pragmatics of
|
|
||||||
@racket[case-lambda] with the following example (among
|
|
||||||
others):
|
|
||||||
|
|
||||||
@racketblock[
|
|
||||||
(define substring1
|
|
||||||
(case-lambda
|
|
||||||
[(s) (substring1 s 0 (string-length s))]
|
|
||||||
[(s start) (substring1 s start (string-length s))]
|
|
||||||
[(s start end) (substring s start end)]))
|
|
||||||
]
|
|
||||||
This version of @racket[substring] has one of the following signature:
|
|
||||||
@itemize[
|
|
||||||
@item{just a string, in which case it copies the string;}
|
|
||||||
@item{a string and an index into the string, in which case it extracts the
|
|
||||||
suffix of the string starting at the index; or }
|
|
||||||
@item{a string a start index and an end index, in which case it extracts the
|
|
||||||
fragment of the string between the two indices. }
|
|
||||||
]
|
|
||||||
|
|
||||||
The contract for such a function is formed with the @racket[case->]
|
|
||||||
combinator, which combines as many functional contracts as needed:
|
|
||||||
@racketblock[
|
|
||||||
(provide/contract
|
|
||||||
[substring1
|
|
||||||
(case->
|
|
||||||
(string? . -> . string?)
|
|
||||||
(string? natural-number/c . -> . string?)
|
|
||||||
(string? natural-number/c natural-number/c . -> . string?))])
|
|
||||||
]
|
|
||||||
As you can see, the contract for @racket[substring1] combines three
|
|
||||||
function contracts, just as many clauses as the explanation of its
|
|
||||||
functionality required.
|
|
||||||
|
|
||||||
@;{
|
|
||||||
This isn't supported anymore (yet...?). -robby
|
|
||||||
|
|
||||||
In the case of @racket[substring1], we also know that the indices
|
|
||||||
that it consumes ought to be natural numbers less than the length of the
|
|
||||||
given string. Since @racket[case->] just combines arrow contracts,
|
|
||||||
adding such constraints is just a matter of strengthening the individual
|
|
||||||
contracts:
|
|
||||||
<racket>
|
|
||||||
(provide/contract
|
|
||||||
[substring1 (case->
|
|
||||||
(string? . -> . string?)
|
|
||||||
(->r ([s string?]
|
|
||||||
[_ (and/c natural-number/c (</c (string-length s)))])
|
|
||||||
string?)
|
|
||||||
(->r ([s string?]
|
|
||||||
[a (and/c natural-number/c (</c (string-length s)))]
|
|
||||||
[o (and/c natural-number/c
|
|
||||||
(>=/c a)
|
|
||||||
(</c (string-length s)))])
|
|
||||||
string?))])
|
|
||||||
</racket>
|
|
||||||
Here we used @racket[->r] to name the parameters and express the
|
|
||||||
numeric constraints on them.
|
|
||||||
}
|
|
||||||
|
|
||||||
@ctc-section[#:tag "multiple"]{Multiple Result Values}
|
@ctc-section[#:tag "multiple"]{Multiple Result Values}
|
||||||
|
|
||||||
The function @racket[split] consumes a list of @racket[char]s
|
The function @racket[split] consumes a list of @racket[char]s
|
||||||
|
@ -534,8 +487,8 @@ The function @racket[split] consumes a list of @racket[char]s
|
||||||
traversing a single list.
|
traversing a single list.
|
||||||
|
|
||||||
The contract for such a function can use the ordinary
|
The contract for such a function can use the ordinary
|
||||||
function arrow @racket[->], since it
|
function arrow @racket[->], since @racket[->]
|
||||||
treats @racket[values] specially, when it appears as the
|
treats @racket[values] specially when it appears as the
|
||||||
last result:
|
last result:
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
|
@ -544,21 +497,21 @@ last result:
|
||||||
]
|
]
|
||||||
|
|
||||||
The contract for such a function can also be written
|
The contract for such a function can also be written
|
||||||
using @racket[->*], just like @racket[plus]:
|
using @racket[->*]:
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[split (->* ((listof char?))
|
[split (->* ((listof char?))
|
||||||
()
|
()
|
||||||
(values string? (listof char?)))])
|
(values string? (listof char?)))])
|
||||||
]
|
]
|
||||||
As before the contract for the argument is wrapped in an
|
As before, the contract for the argument with @racket[->*] is wrapped in an
|
||||||
extra pair of parentheses (and must always be wrapped like
|
extra pair of parentheses (and must always be wrapped like
|
||||||
that) and the empty pair of parentheses indicates that
|
that) and the empty pair of parentheses indicates that
|
||||||
there are no optoinal arguments. The contracts for the
|
there are no optional arguments. The contracts for the
|
||||||
results are inside @racket[values]: a string and a list of
|
results are inside @racket[values]: a string and a list of
|
||||||
characters.
|
characters.
|
||||||
|
|
||||||
Now suppose we also want to ensure that the first result of
|
Now, suppose that we also want to ensure that the first result of
|
||||||
@racket[split] is a prefix of the given word in list format. In that
|
@racket[split] is a prefix of the given word in list format. In that
|
||||||
case, we need to use the @racket[->d] contract combinator:
|
case, we need to use the @racket[->d] contract combinator:
|
||||||
@racketblock[
|
@racketblock[
|
||||||
|
@ -584,7 +537,7 @@ Now suppose we also want to ensure that the first result of
|
||||||
first contract strengthens the old one so that the result is a prefix of
|
first contract strengthens the old one so that the result is a prefix of
|
||||||
the given word.
|
the given word.
|
||||||
|
|
||||||
This contract is expensive to check of course. Here is a slightly
|
This contract is expensive to check, of course. Here is a slightly
|
||||||
cheaper version:
|
cheaper version:
|
||||||
@racketblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
|
@ -593,9 +546,9 @@ This contract is expensive to check of course. Here is a slightly
|
||||||
(values [s (string-len/c (length fl))]
|
(values [s (string-len/c (length fl))]
|
||||||
[c (listof char?)]))])
|
[c (listof char?)]))])
|
||||||
]
|
]
|
||||||
Click on @racket[string-len/c] to see what it does.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "no-domain"]{Procedures of Some Fixed, but Statically Unknown Arity}
|
|
||||||
|
@ctc-section[#:tag "no-domain"]{Fixed but Statically Unknown Arities}
|
||||||
|
|
||||||
Imagine yourself writing a contract for a function that accepts some other
|
Imagine yourself writing a contract for a function that accepts some other
|
||||||
function and a list of numbers that eventually applies the former to the
|
function and a list of numbers that eventually applies the former to the
|
||||||
|
|
|
@ -1,33 +1,33 @@
|
||||||
#lang scribble/doc
|
#lang scribble/doc
|
||||||
@(require scribble/manual
|
@(require scribble/manual
|
||||||
scribble/eval
|
scribble/eval
|
||||||
scheme/sandbox
|
racket/sandbox
|
||||||
"guide-utils.ss"
|
"guide-utils.ss"
|
||||||
"contracts-utils.ss"
|
"contracts-utils.ss"
|
||||||
(for-label scheme/contract))
|
(for-label racket/contract))
|
||||||
|
|
||||||
@title[#:tag "contracts-gotchas"]{Gotchas}
|
@title[#:tag "contracts-gotchas"]{Gotchas}
|
||||||
|
|
||||||
@ctc-section{Contracts and @scheme[eq?]}
|
@ctc-section{Contracts and @racket[eq?]}
|
||||||
|
|
||||||
As a general rule, adding a contract to a program should
|
As a general rule, adding a contract to a program should
|
||||||
either leave the behavior of the program unchanged, or
|
either leave the behavior of the program unchanged, or
|
||||||
should signal a contract violation. And this is almost true
|
should signal a contract violation. And this is almost true
|
||||||
for PLT Scheme contracts, with one exception: @scheme[eq?].
|
for Racket contracts, with one exception: @racket[eq?].
|
||||||
|
|
||||||
The @scheme[eq?] procedure is designed to be fast and does
|
The @racket[eq?] procedure is designed to be fast and does
|
||||||
not provide much in the way of guarantees, except that if it
|
not provide much in the way of guarantees, except that if it
|
||||||
returns true, it means that the two values behave
|
returns true, it means that the two values behave
|
||||||
identically in all respects. Internally, this is implemented
|
identically in all respects. Internally, this is implemented
|
||||||
as pointer equality at a low-level so it exposes information
|
as pointer equality at a low-level so it exposes information
|
||||||
about how PLT Scheme is implemented (and how contracts are
|
about how Racket is implemented (and how contracts are
|
||||||
implemented).
|
implemented).
|
||||||
|
|
||||||
Contracts interact poorly with @scheme[eq?] because function
|
Contracts interact poorly with @racket[eq?] because function
|
||||||
contract checking is implemented internally as wrapper
|
contract checking is implemented internally as wrapper
|
||||||
functions. For example, consider this module:
|
functions. For example, consider this module:
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme
|
racket
|
||||||
|
|
||||||
(define (make-adder x)
|
(define (make-adder x)
|
||||||
(if (= 1 x)
|
(if (= 1 x)
|
||||||
|
@ -36,51 +36,51 @@ scheme
|
||||||
(provide/contract [make-adder (-> number? (-> number? number?))])
|
(provide/contract [make-adder (-> number? (-> number? number?))])
|
||||||
]
|
]
|
||||||
|
|
||||||
It exports the @scheme[make-adder] function that is the usual curried
|
It exports the @racket[make-adder] function that is the usual curried
|
||||||
addition function, except that it returns Scheme's @scheme[add1] when
|
addition function, except that it returns Racket's @racket[add1] when
|
||||||
its input is @scheme[1].
|
its input is @racket[1].
|
||||||
|
|
||||||
You might expect that
|
You might expect that
|
||||||
@schemeblock[
|
@racketblock[
|
||||||
(eq? (make-adder 1)
|
(eq? (make-adder 1)
|
||||||
(make-adder 1))
|
(make-adder 1))
|
||||||
]
|
]
|
||||||
|
|
||||||
would return @scheme[#t], but it does not. If the contract were
|
would return @racket[#t], but it does not. If the contract were
|
||||||
changed to @scheme[any/c] (or even @scheme[(-> number? any/c)]), then
|
changed to @racket[any/c] (or even @racket[(-> number? any/c)]), then
|
||||||
the @scheme[eq?] call would return @scheme[#t].
|
the @racket[eq?] call would return @racket[#t].
|
||||||
|
|
||||||
Moral: do not use @scheme[eq?] on values that have contracts.
|
Moral: Do not use @racket[eq?] on values that have contracts.
|
||||||
|
|
||||||
@ctc-section[#:tag "exists-gotcha"]{Exists Contracts and Predicates}
|
@ctc-section[#:tag "exists-gotcha"]{Exists Contracts and Predicates}
|
||||||
|
|
||||||
Much like the @scheme[eq?] example above, @scheme[#:∃] contracts
|
Much like the @racket[eq?] example above, @racket[#:∃] contracts
|
||||||
can change the behavior of a program.
|
can change the behavior of a program.
|
||||||
|
|
||||||
Specifically,
|
Specifically,
|
||||||
the @scheme[null?] predicate (and many other predicates) return @scheme[#f]
|
the @racket[null?] predicate (and many other predicates) return @racket[#f]
|
||||||
for @scheme[#:∃] contracts, and changing one of those contracts to @scheme[any/c]
|
for @racket[#:∃] contracts, and changing one of those contracts to @racket[any/c]
|
||||||
means that @scheme[null?] might now return @scheme[#t] instead, resulting in
|
means that @racket[null?] might now return @racket[#t] instead, resulting in
|
||||||
arbitrarily different behavior depending on this boolean might flow around
|
arbitrarily different behavior depending on this boolean might flow around
|
||||||
in the program.
|
in the program.
|
||||||
|
|
||||||
@defmodulelang[scheme/exists]
|
@defmodulelang[racket/exists]
|
||||||
|
|
||||||
To work around the above problem, the
|
To work around the above problem, the
|
||||||
@schememodname[scheme/exists] library behaves just like the @schememodname[scheme],
|
@racketmodname[racket/exists] library behaves just like the @racketmodname[racket],
|
||||||
but where predicates signal errors when given @scheme[#:∃] contracts.
|
but where predicates signal errors when given @racket[#:∃] contracts.
|
||||||
|
|
||||||
Moral: do not use predicates on @scheme[#:∃] contracts, but if you're not sure, use
|
Moral: Do not use predicates on @racket[#:∃] contracts, but if you're not sure, use
|
||||||
@schememodname[scheme/exists] to be safe.
|
@racketmodname[racket/exists] to be safe.
|
||||||
|
|
||||||
@ctc-section{Defining Recursive Contracts}
|
@ctc-section{Defining Recursive Contracts}
|
||||||
|
|
||||||
When defining a self-referential contract, it is natural to use
|
When defining a self-referential contract, it is natural to use
|
||||||
@scheme[define]. For example, one might try to write a contract on
|
@racket[define]. For example, one might try to write a contract on
|
||||||
streams like this:
|
streams like this:
|
||||||
|
|
||||||
@(define e (make-base-eval))
|
@(define e (make-base-eval))
|
||||||
@(interaction-eval #:eval e (require scheme/contract))
|
@(interaction-eval #:eval e (require racket/contract))
|
||||||
@interaction[
|
@interaction[
|
||||||
#:eval e
|
#:eval e
|
||||||
(define stream/c
|
(define stream/c
|
||||||
|
@ -92,12 +92,12 @@ streams like this:
|
||||||
@close-eval[e]
|
@close-eval[e]
|
||||||
|
|
||||||
Unfortunately, this does not work because the value of
|
Unfortunately, this does not work because the value of
|
||||||
@scheme[stream/c] is needed before it is defined. Put another way, all
|
@racket[stream/c] is needed before it is defined. Put another way, all
|
||||||
of the combinators evaluate their arguments eagerly, even thought the
|
of the combinators evaluate their arguments eagerly, even thought the
|
||||||
values that they accept do not.
|
values that they accept do not.
|
||||||
|
|
||||||
Instead, use
|
Instead, use
|
||||||
@schemeblock[
|
@racketblock[
|
||||||
(define stream/c
|
(define stream/c
|
||||||
(promise/c
|
(promise/c
|
||||||
(or/c
|
(or/c
|
||||||
|
@ -106,27 +106,27 @@ Instead, use
|
||||||
(recursive-contract stream/c)))))
|
(recursive-contract stream/c)))))
|
||||||
]
|
]
|
||||||
|
|
||||||
The use of @scheme[recursive-contract] delays the evaluation of the
|
The use of @racket[recursive-contract] delays the evaluation of the
|
||||||
identifier @scheme[stream/c] until after the contract is first
|
identifier @racket[stream/c] until after the contract is first
|
||||||
checked, long enough to ensure that @scheme[stream/c] is defined.
|
checked, long enough to ensure that @racket[stream/c] is defined.
|
||||||
|
|
||||||
See also @ctc-link["lazy-contracts"].
|
See also @ctc-link["lazy-contracts"].
|
||||||
|
|
||||||
@ctc-section{Using @scheme[set!] to Assign to Variables Provided via @scheme[provide/contract]}
|
@ctc-section{Mixing @racket[set!] and @racket[provide/contract]}
|
||||||
|
|
||||||
The contract library assumes that variables exported via
|
The contract library assumes that variables exported via
|
||||||
@scheme[provide/contract] are not assigned to, but does not enforce
|
@racket[provide/contract] are not assigned to, but does not enforce
|
||||||
it. Accordingly, if you try to @scheme[set!] those variables, you
|
it. Accordingly, if you try to @racket[set!] those variables, you
|
||||||
may be surprised. Consider the following example:
|
may be surprised. Consider the following example:
|
||||||
|
|
||||||
@interaction[
|
@interaction[
|
||||||
(module server scheme
|
(module server racket
|
||||||
(define (inc-x!) (set! x (+ x 1)))
|
(define (inc-x!) (set! x (+ x 1)))
|
||||||
(define x 0)
|
(define x 0)
|
||||||
(provide/contract [inc-x! (-> void?)]
|
(provide/contract [inc-x! (-> void?)]
|
||||||
[x integer?]))
|
[x integer?]))
|
||||||
|
|
||||||
(module client scheme
|
(module client racket
|
||||||
(require 'server)
|
(require 'server)
|
||||||
|
|
||||||
(define (print-latest) (printf "x is ~s\n" x))
|
(define (print-latest) (printf "x is ~s\n" x))
|
||||||
|
@ -138,15 +138,15 @@ may be surprised. Consider the following example:
|
||||||
(require 'client)
|
(require 'client)
|
||||||
]
|
]
|
||||||
|
|
||||||
Both calls to @scheme[print-latest] print @scheme[0], even though the
|
Both calls to @racket[print-latest] print @racket[0], even though the
|
||||||
value of @scheme[x] has been incremented (and the change is visible
|
value of @racket[x] has been incremented (and the change is visible
|
||||||
inside the module @scheme[x]).
|
inside the module @racket[x]).
|
||||||
|
|
||||||
To work around this, export accessor functions, rather than
|
To work around this, export accessor functions, rather than
|
||||||
exporting the variable directly, like this:
|
exporting the variable directly, like this:
|
||||||
|
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme
|
racket
|
||||||
|
|
||||||
(define (get-x) x)
|
(define (get-x) x)
|
||||||
(define (inc-x!) (set! x (+ x 1)))
|
(define (inc-x!) (set! x (+ x 1)))
|
||||||
|
@ -155,5 +155,5 @@ scheme
|
||||||
[get-x (-> integer?)])
|
[get-x (-> integer?)])
|
||||||
]
|
]
|
||||||
|
|
||||||
Moral: This is a bug we hope to address in a future release.
|
Moral: This is a bug that we will address in a future release.
|
||||||
|
|
||||||
|
|
|
@ -3,7 +3,7 @@
|
||||||
scribble/eval
|
scribble/eval
|
||||||
"guide-utils.ss"
|
"guide-utils.ss"
|
||||||
"contracts-utils.ss"
|
"contracts-utils.ss"
|
||||||
(for-label scheme/contract))
|
(for-label racket/contract))
|
||||||
|
|
||||||
@title[#:tag "contract-boundaries"]{Contracts and Boundaries}
|
@title[#:tag "contract-boundaries"]{Contracts and Boundaries}
|
||||||
|
|
||||||
|
@ -16,72 +16,73 @@ A contract thus establishes a boundary between the two parties. Whenever a
|
||||||
value crosses this boundary, the contract monitoring system performs contract
|
value crosses this boundary, the contract monitoring system performs contract
|
||||||
checks, making sure the partners abide by the established contract.
|
checks, making sure the partners abide by the established contract.
|
||||||
|
|
||||||
In this spirit, PLT Scheme supports contracts only at module
|
In this spirit, Racket encourages contracts mainly at module
|
||||||
boundaries. Specifically, programmers may attach contracts to
|
boundaries. Specifically, programmers may attach contracts to
|
||||||
@scheme[provide] clauses and thus impose constraints and promises on the use
|
@racket[provide] clauses and thus impose constraints and promises on the use
|
||||||
of exported values. For example, the export specification
|
of exported values. For example, the export specification
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme
|
racket
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[amount positive?])
|
[amount positive?])
|
||||||
(define amount ...)
|
(define amount ...)
|
||||||
]
|
]
|
||||||
|
|
||||||
promises to all clients of the above module that amount will
|
promises to all clients of the above module that the value of @racket[amount] will
|
||||||
always be a positive number. The contract system monitors
|
always be a positive number. The contract system monitors
|
||||||
the module's obligation carefully. Every time a client
|
the module's obligation carefully. Every time a client
|
||||||
refers to @scheme[amount], the monitor checks that the value
|
refers to @racket[amount], the monitor checks that the value
|
||||||
of @scheme[amount] is indeed a positive number.
|
of @racket[amount] is indeed a positive number.
|
||||||
|
|
||||||
The contracts library is built into the Scheme language, but
|
The contracts library is built into the Racket language, but
|
||||||
if you wish to use @scheme[scheme/base], you can explicitly
|
if you wish to use @racket[racket/base], you can explicitly
|
||||||
require the contracts library like this:
|
require the contracts library like this:
|
||||||
|
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme/base
|
racket/base
|
||||||
(require scheme/contract) (code:comment "now we can write contracts")
|
(require racket/contract) (code:comment "now we can write contracts")
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[amount positive?])
|
[amount positive?])
|
||||||
(define amount ...)
|
(define amount ...)
|
||||||
]
|
]
|
||||||
|
|
||||||
@ctc-section[#:tag "amount0"]{A First Contract Violation}
|
@ctc-section[#:tag "amount0"]{Contract Violations}
|
||||||
|
|
||||||
Suppose the creator of the module had written
|
If we bind @scheme[amount] to a number that is not positive,
|
||||||
@schememod[
|
|
||||||
scheme
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[amount positive?])
|
[amount positive?])
|
||||||
|
|
||||||
(define amount 0)]
|
(define amount 0)]
|
||||||
|
|
||||||
When this module is required, the monitoring
|
then, when the module is required, the monitoring
|
||||||
system signals a violation of the contract and
|
system signals a violation of the contract and
|
||||||
blames the module for breaking its promises.
|
blames the module for breaking its promises.
|
||||||
|
|
||||||
@ctc-section[#:tag "qamount"]{A Subtle Contract Violation}
|
@; @ctc-section[#:tag "qamount"]{A Subtle Contract Violation}
|
||||||
|
|
||||||
Suppose we write this module
|
An even bigger mistake would be to bind @racket[amount]
|
||||||
@schememod[
|
to a non-number value:
|
||||||
scheme
|
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[amount positive?])
|
[amount positive?])
|
||||||
|
|
||||||
(define amount 'amount)
|
(define amount 'amount)
|
||||||
]
|
]
|
||||||
|
|
||||||
In that case, the monitoring system applies
|
In this case, the monitoring system will apply
|
||||||
@scheme[positive?] to a symbol, but @scheme[positive?]
|
@racket[positive?] to a symbol, but @racket[positive?]
|
||||||
reports an error, because its domain is only numbers. To
|
reports an error, because its domain is only numbers. To
|
||||||
make the contract capture our intentions for all Scheme
|
make the contract capture our intentions for all Racket
|
||||||
values, we can ensure that the value is both a number and is
|
values, we can ensure that the value is both a number and is
|
||||||
positive, combining the two contracts with @scheme[and/c]:
|
positive, combining the two contracts with @racket[and/c]:
|
||||||
|
|
||||||
@schemeblock[
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[amount (and/c number? positive?)])
|
[amount (and/c number? positive?)])
|
||||||
]
|
]
|
||||||
|
@ -95,13 +96,13 @@ provide/contract'd. This is currently buggy so this
|
||||||
discussion is elided. Here's the expansion of
|
discussion is elided. Here's the expansion of
|
||||||
the requiring module, just to give an idea:
|
the requiring module, just to give an idea:
|
||||||
|
|
||||||
(module m mzscheme
|
(module m racket
|
||||||
(require mzlib/contract)
|
(require mzlib/contract)
|
||||||
(provide/contract [x x-ctc]))
|
(provide/contract [x x-ctc]))
|
||||||
|
|
||||||
(module n mzscheme (require m) (define (f) ... x ...))
|
(module n racket (require m) (define (f) ... x ...))
|
||||||
==>
|
==>
|
||||||
(module n mzscheme
|
(module n racket
|
||||||
(require (rename m x x-real))
|
(require (rename m x x-real))
|
||||||
(define x (apply-contract x-real x-ctc ...))
|
(define x (apply-contract x-real x-ctc ...))
|
||||||
(define (f) ... x ...))
|
(define (f) ... x ...))
|
||||||
|
@ -122,9 +123,9 @@ Of course, this breaks assignment to the provided variable.
|
||||||
|
|
||||||
<table src="simple.ss">
|
<table src="simple.ss">
|
||||||
<tr><td bgcolor="e0e0fa">
|
<tr><td bgcolor="e0e0fa">
|
||||||
<scheme>
|
<racket>
|
||||||
;; Language: Pretty Big
|
;; Language: Pretty Big
|
||||||
(module a mzscheme
|
(module a racket
|
||||||
(require mzlib/contract)
|
(require mzlib/contract)
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
|
@ -139,7 +140,7 @@ Of course, this breaks assignment to the provided variable.
|
||||||
|
|
||||||
(define (do-it) <font color="red">(set! amount -4)</font>))
|
(define (do-it) <font color="red">(set! amount -4)</font>))
|
||||||
|
|
||||||
(module b mzscheme
|
(module b racket
|
||||||
(require a)
|
(require a)
|
||||||
|
|
||||||
(printf "~s~n" amount)
|
(printf "~s~n" amount)
|
||||||
|
@ -147,17 +148,17 @@ Of course, this breaks assignment to the provided variable.
|
||||||
(printf "~s~n" amount))
|
(printf "~s~n" amount))
|
||||||
|
|
||||||
(require b)
|
(require b)
|
||||||
</scheme>
|
</racket>
|
||||||
<td bgcolor="beige" valign="top">
|
<td bgcolor="beige" valign="top">
|
||||||
<pre>
|
<pre>
|
||||||
|
|
||||||
the "server" module
|
the "server" module
|
||||||
this allows us to write contracts
|
this allows us to write contracts
|
||||||
|
|
||||||
export @scheme[amount] with a contract
|
export @racket[amount] with a contract
|
||||||
|
|
||||||
|
|
||||||
export @scheme[do-it] without contract
|
export @racket[do-it] without contract
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -168,65 +169,71 @@ set amount to 4,
|
||||||
the "client" module
|
the "client" module
|
||||||
requires functionality from a
|
requires functionality from a
|
||||||
|
|
||||||
first reference to @scheme[amount] (okay)
|
first reference to @racket[amount] (okay)
|
||||||
a call to @scheme[do-it],
|
a call to @racket[do-it],
|
||||||
second reference to @scheme[amount] (fail)
|
second reference to @racket[amount] (fail)
|
||||||
|
|
||||||
</pre> </table>
|
</pre> </table>
|
||||||
|
|
||||||
<p><strong>Note:</strong> The above example is mostly self-explanatory. Take a
|
<p><strong>Note:</strong> The above example is mostly self-explanatory. Take a
|
||||||
look at the lines in red, however. Even though the call to @scheme[do-it]
|
look at the lines in red, however. Even though the call to @racket[do-it]
|
||||||
sets @scheme[amount] to -4, this action is <strong>not</strong> a contract
|
sets @racket[amount] to -4, this action is <strong>not</strong> a contract
|
||||||
violation. The contract violation takes place only when the client module
|
violation. The contract violation takes place only when the client module
|
||||||
(@scheme[b]) refers to @scheme[amount] again and the value flows across
|
(@racket[b]) refers to @racket[amount] again and the value flows across
|
||||||
the module boundary for a second time.
|
the module boundary for a second time.
|
||||||
|
|
||||||
</question>
|
</question>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@;{
|
||||||
|
|
||||||
@ctc-section[#:tag "obligations"]{Imposing Obligations on a Module's Clients}
|
@ctc-section[#:tag "obligations"]{Imposing Obligations on a Module's Clients}
|
||||||
|
|
||||||
On occasion, a module may want to enter a contract with
|
On occasion, a module may want to enter a contract with
|
||||||
another module only if the other module abides by certain
|
another module only if the other module abides by certain
|
||||||
rules. In other words, the module isn't just promising some
|
rules. In other words, the module isn't just promising some
|
||||||
services, it also demands the client to deliver
|
services, it also demands the client to deliver
|
||||||
something. This kind of thing happens when a module exports
|
something. That situation may happen when a module exports
|
||||||
a function, an object, a class or other values that enable
|
a function, an object, a class, or some other construct that enables
|
||||||
values to flow in both directions.
|
values to flow in both directions.
|
||||||
|
|
||||||
@ctc-section{Experimenting with Examples}
|
}
|
||||||
|
|
||||||
|
@ctc-section{Experimenting with Contracts and Modules}
|
||||||
|
|
||||||
All of the contracts and module in this chapter (excluding those just
|
All of the contracts and module in this chapter (excluding those just
|
||||||
following) are written using the standard @tt{#lang} syntax for
|
following) are written using the standard @tt{#lang} syntax for
|
||||||
describing modules. Thus, if you extract examples from this chapter in
|
describing modules. Since modules serve as the boundary between
|
||||||
order to experiment with the behavior of the contract system, you
|
parties in a contract, examples involve multiple modules.
|
||||||
would have to make multiple files.
|
|
||||||
|
|
||||||
To rectify this, PLT Scheme provides a special language, called
|
To experiment with multiple modules within a single module or within
|
||||||
@schememodname[scheme/load]. The contents of such a module is other modules (and
|
DrRacket's @tech{definitions area}, use the
|
||||||
@scheme[require] statements), using the parenthesized syntax for a
|
@racketmodname[racket/load] language. The contents of such a module
|
||||||
module. For example, to try the example earlier in this section, you
|
can be other modules (and @racket[require] statements), using the
|
||||||
would write:
|
longhand parenthesized syntax for a module (see
|
||||||
@schememod[
|
@secref["module-syntax"]). For example, try the example earlier in
|
||||||
scheme/load
|
this section as follows:
|
||||||
|
|
||||||
(module m scheme
|
@racketmod[
|
||||||
(define amount 150)
|
racket/load
|
||||||
(provide/contract [amount (and/c number? positive?)]))
|
|
||||||
|
|
||||||
(module n scheme
|
(module m racket
|
||||||
|
(provide/contract [amount (and/c number? positive?)])
|
||||||
|
(define amount 150))
|
||||||
|
|
||||||
|
(module n racket
|
||||||
(require 'm)
|
(require 'm)
|
||||||
(+ amount 10))
|
(+ amount 10))
|
||||||
|
|
||||||
(require 'n)]
|
(require 'n)]
|
||||||
|
|
||||||
Each of the modules and their contracts are wrapped in parentheses
|
Each of the modules and their contracts are wrapped in parentheses
|
||||||
with the @scheme[module] keyword at the front. The first argument to
|
with the @racket[module] keyword at the front. The first form after
|
||||||
@scheme[module] should be the name of the module, so it can be used in
|
@racket[module] is the name of the module to be used in a subsequent
|
||||||
a subsequent @scheme[require] statement (note that in the
|
@racket[require] statement (where each reference through a
|
||||||
@scheme[require], the name of the module must be prefixed with a
|
@racket[require] prefixes the name with a quote). The second form
|
||||||
quote). The second argument to @scheme[module] is the language (what
|
after @racket[module] is the language, and the remaining forms are the
|
||||||
would have come after @tt{#lang} in the usual notation), and the
|
body of the module. After all of the modules, a @racket[require]
|
||||||
remaining arguments are the body of the module. After all of the
|
starts one of the modules plus anything that is @racket[require]s.
|
||||||
modules, there must a @scheme[require] to kick things off.
|
|
||||||
|
|
||||||
|
|
|
@ -3,136 +3,161 @@
|
||||||
scribble/eval
|
scribble/eval
|
||||||
"guide-utils.ss"
|
"guide-utils.ss"
|
||||||
"contracts-utils.ss"
|
"contracts-utils.ss"
|
||||||
(for-label scheme/contract))
|
(for-label racket/contract))
|
||||||
|
|
||||||
@title[#:tag "contract-func"]{Simple Contracts on Functions}
|
@title[#:tag "contract-func"]{Simple Contracts on Functions}
|
||||||
|
|
||||||
When a module exports a function, it establishes two
|
A mathematical function has a @deftech{domain} and a
|
||||||
channels of communication between itself and the client
|
@deftech{range}. The domain indicates the kind of values that the
|
||||||
module that imports the function. If the client module calls
|
function can accept as arguments, and the range indicates the kind of
|
||||||
the function, it sends a value into the ``server''
|
values that it produces. The conventional notation for a describing a
|
||||||
module. Conversely, if such a function call ends and the
|
function with its domain and range is
|
||||||
function returns a value, the ``server'' module sends a
|
|
||||||
value back to the ``client'' module.
|
|
||||||
|
|
||||||
It is important to keep this picture in mind when you read the explanations
|
@racketblock[
|
||||||
of the various ways of imposing contracts on functions.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "argcontract"]{Restricting the Arguments of a Function}
|
|
||||||
|
|
||||||
Functions usually don't work on all possible Scheme values but only on a
|
|
||||||
select subset such as numbers, booleans, etc. Here is a module that may
|
|
||||||
represent a bank account:
|
|
||||||
|
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
|
|
||||||
(provide/contract
|
|
||||||
[create (-> string? number? any)]
|
|
||||||
[deposit (-> number? any)])
|
|
||||||
|
|
||||||
(define amount 0)
|
|
||||||
(define (create name initial-deposit) ...)
|
|
||||||
(define (deposit a) (set! amount (+ amount a)))
|
|
||||||
]
|
|
||||||
|
|
||||||
It exports two functions:
|
|
||||||
@itemize[
|
|
||||||
|
|
||||||
@item{@scheme[create]: The function's contract says that it consumes two
|
|
||||||
arguments, a string and a number, and it promises nothing about the return value. }
|
|
||||||
|
|
||||||
@item{@scheme[deposit]: The function's contract demands from the client modules
|
|
||||||
that they apply it to numbers. It promises nothing about the return value. }]
|
|
||||||
|
|
||||||
If a ``client'' module were to apply @scheme[deposit] to
|
|
||||||
@scheme['silly], it would violate the contract. The
|
|
||||||
contract monitoring system would catch this violation and
|
|
||||||
blame ``client'' for breaking the contract with the above
|
|
||||||
module.
|
|
||||||
|
|
||||||
@bold{Note:} Instead of @scheme[any] you could also use the
|
|
||||||
more specific contract @scheme[void?], which says that the function will
|
|
||||||
always return the @scheme[(void)] value. This contract, however, would require
|
|
||||||
the contract monitoring system to check the return value every time the function
|
|
||||||
is called, even though the ``client'' module can't do much with this value
|
|
||||||
anyway. In contrast, @scheme[any] tells the monitoring system @italic{not}
|
|
||||||
to check the return value. Additionally, it tells a potential client that the
|
|
||||||
``server'' module @italic{makes no promises at all} about the function's return
|
|
||||||
value.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "arrow"]{Arrows}
|
|
||||||
|
|
||||||
It is natural to use an arrow to say that an exported value is a
|
|
||||||
function. In decent high schools, you learn that a function has a domain
|
|
||||||
and a range, and that you write this fact down like this:
|
|
||||||
@schemeblock[
|
|
||||||
f : A -> B
|
f : A -> B
|
||||||
]
|
]
|
||||||
Here the @scheme[A] and @scheme[B] are sets; @scheme[A] is the
|
|
||||||
domain and @scheme[B] is the range.
|
|
||||||
|
|
||||||
Functions in a programming language have domains and ranges, too. In
|
where @racket[A] is the domain of the function and @racket[B] is the
|
||||||
statically typed languages, you write down the names of types for each
|
range.
|
||||||
argument and for the result. When all you have, however, is a Scheme name,
|
|
||||||
such as @scheme[create] or @scheme[deposit], you want to tell the
|
Functions in a programming language have domains and ranges, too, and
|
||||||
reader what the name represents (a function) and, if it is a function (or
|
a contract can ensure that a function receives only values in its
|
||||||
some other complex value) what the pieces are supposed to be. This is why
|
range and produces only values in its domain. A @racket[->] creates
|
||||||
we use a @scheme[->] to say ``hey, expect this to be a function.''
|
such a contract for a function. The forms after a @racket[->] specify
|
||||||
|
contracts for the domains and finally a contract for the range.
|
||||||
|
|
||||||
|
Here is a module that might represent a bank account:
|
||||||
|
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
So @scheme[->] says ``this is a contract for a function.'' What follows
|
|
||||||
in a function contracts are contracts (sub-contracts if you wish) that tell
|
|
||||||
the reader what kind of arguments to expect and what kind of a result the
|
|
||||||
function produces. For example,
|
|
||||||
@schemeblock[
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[create (-> string? number? boolean? account?)])
|
[deposit (-> number? any)]
|
||||||
|
[balance (-> number?)])
|
||||||
|
|
||||||
|
(define amount 0)
|
||||||
|
(define (deposit a) (set! amount (+ amount a)))
|
||||||
|
(define (balance) amount)
|
||||||
]
|
]
|
||||||
says that @scheme[create] is a function of three arguments: a string, a
|
|
||||||
number, and a boolean. Its result is an account.
|
|
||||||
|
|
||||||
In short, the arrow @scheme[->] is a @italic{contract
|
The module exports two functions:
|
||||||
combinator}. Its purpose is to combine other contracts into a contract
|
|
||||||
that says ``this is a function @italic{and} its arguments and its result
|
|
||||||
are like that.''
|
|
||||||
|
|
||||||
@ctc-section[#:tag "dots"]{Infix Contract Notation}
|
@itemize[
|
||||||
|
|
||||||
If you are used to mathematics, you like the arrow in between the
|
@item{@racket[deposit], which accepts a number and returns some value
|
||||||
domain and the range of a function, not at the beginning. If you
|
that is not specified in the contract, and}
|
||||||
have read @|HtDP|, you have seen this many times. Indeed, you may
|
|
||||||
have seen contracts such as these in other people's code:
|
|
||||||
|
|
||||||
@schemeblock[
|
@item{@racket[balance], which returns a number indicating the current
|
||||||
|
balance of the account.}
|
||||||
|
|
||||||
|
]
|
||||||
|
|
||||||
|
When a module exports a function, it establishes two channels of
|
||||||
|
communication between itself as a ``server'' and the ``client'' module
|
||||||
|
that imports the function. If the client module calls the function, it
|
||||||
|
sends a value into the server module. Conversely, if such a function
|
||||||
|
call ends and the function returns a value, the server module sends a
|
||||||
|
value back to the client module. This client--server distinction is
|
||||||
|
important, because when something goes wrong, one or the other of the
|
||||||
|
parties is to blame.
|
||||||
|
|
||||||
|
If a client module were to apply @racket[deposit] to @racket['millions],
|
||||||
|
it would violate the contract. The contract-monitoring system would
|
||||||
|
catch this violation and blame client for breaking the contract with
|
||||||
|
the above module. In contrast, if the @racket[balance] function were
|
||||||
|
to return @racket['broke], the contract-monitoring system
|
||||||
|
would blame the server module.
|
||||||
|
|
||||||
|
A @racket[->] by itself is not a contract; it is a @deftech{contract
|
||||||
|
combinator}, which combines other contracts to form a contract.
|
||||||
|
|
||||||
|
@; ------------------------------------------------------------------------
|
||||||
|
|
||||||
|
@section{Styles of @racket[->]}
|
||||||
|
|
||||||
|
If you are used to mathematical function, you may prefer a contract
|
||||||
|
arrow to appear between the domain and the range of a function, not
|
||||||
|
at the beginning. If you have read @|HtDP|, you have seen this many
|
||||||
|
times. Indeed, you may have seen contracts such as these in other
|
||||||
|
people's code:
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[create (string? number? boolean? . -> . account?)])
|
[deposit (number? . -> . any)])
|
||||||
]
|
]
|
||||||
|
|
||||||
If a PLT Scheme S-expression contains two dots with a symbol in the middle,
|
If a Racket S-expression contains two dots with a symbol in the middle,
|
||||||
the reader re-arranges the S-expression and place the symbol at the front. Thus,
|
the reader re-arranges the S-expression and place the symbol at the front,
|
||||||
@schemeblock[
|
as described in @secref["lists-and-syntax"]. Thus,
|
||||||
(string? number? boolean? . -> . account?)
|
|
||||||
|
@racketblock[
|
||||||
|
(number? . -> . any)
|
||||||
]
|
]
|
||||||
is really just a short-hand for
|
|
||||||
@schemeblock[
|
is just another way of writing
|
||||||
(-> string? number? boolean? account?)
|
|
||||||
|
@racketblock[
|
||||||
|
(-> number? any)
|
||||||
]
|
]
|
||||||
Of course, placing the arrow to the left of the range follows not only
|
|
||||||
mathematical tradition but also that of typed functional languages.
|
|
||||||
|
|
||||||
@ctc-section[#:tag "own"]{Rolling Your Own Contracts for Function Arguments}
|
@; ----------------------------------------------------------------------
|
||||||
|
@section{@racket[any] and @racket[any/c]}
|
||||||
|
|
||||||
The @scheme[deposit] function adds the given number to the value of
|
The @racket[any] contract used for @racket[deposit] matches any kind
|
||||||
@scheme[amount]. While the function's contract prevents clients from
|
of result, and it can only be used in the range position of a function
|
||||||
applying it to non-numbers, the contract still allows them to apply the function
|
contract. Instead of @racket[any] above, we could use the more
|
||||||
to complex numbers, negative numbers, or inexact numbers, all of which do not
|
specific contract @racket[void?], which says that the function will
|
||||||
represent amounts of money.
|
always return the @racket[(void)] value. The @racket[void?] contract,
|
||||||
|
however, would require the contract monitoring system to check the
|
||||||
|
return value every time the function is called, even though the
|
||||||
|
``client'' module can't do much with the value. In contrast,
|
||||||
|
@racket[any] tells the monitoring system @italic{not} to check the
|
||||||
|
return value, it tells a potential client that the ``server'' module
|
||||||
|
@italic{makes no promises at all} about the function's return value,
|
||||||
|
even whether it is a single value or multiple values.
|
||||||
|
|
||||||
To this end, the contract system allows programmers to define their own
|
The @racket[any/c] contract is similar to @racket[any], in that it
|
||||||
contracts:
|
makes no demands on a value. Unlike @scheme[any], @racket[any/c]
|
||||||
|
indicates a single value, and it is suitable for use as an argument
|
||||||
|
contract. Using @racket[any/c] as a range contract imposes a check
|
||||||
|
that the function produces a single value. That is,
|
||||||
|
|
||||||
@schememod[
|
@racketblock[(-> integer? any)]
|
||||||
scheme
|
|
||||||
|
describes a function that accepts and integer and returns any number of
|
||||||
|
values, while
|
||||||
|
|
||||||
|
@racketblock[(-> integer? any/c)]
|
||||||
|
|
||||||
|
describes a function that accepts an integer and produces a single
|
||||||
|
result (but does not say anything more about the result). The function
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
|
(define (f x) (values (+ x 1) (- x 1)))
|
||||||
|
]
|
||||||
|
|
||||||
|
matches @racket[(-> integer? any)], but not @racket[(-> integer? any/c)].
|
||||||
|
|
||||||
|
Use @racket[any/c] as a result contract when it is particularly
|
||||||
|
important to promise a single result from a function. Use @racket[any]
|
||||||
|
when you want to promise as little as possible (and incur as little
|
||||||
|
checking as possible) for a function's result.
|
||||||
|
|
||||||
|
@; ------------------------------------------------------------------------
|
||||||
|
|
||||||
|
@ctc-section[#:tag "own"]{Rolling Your Own Contracts}
|
||||||
|
|
||||||
|
The @racket[deposit] function adds the given number to the value of
|
||||||
|
@racket[amount]. While the function's contract prevents clients from
|
||||||
|
applying it to non-numbers, the contract still allows them to apply
|
||||||
|
the function to complex numbers, negative numbers, or inexact numbers,
|
||||||
|
none of which sensibly represent amounts of money.
|
||||||
|
|
||||||
|
The contract system allows programmers to define their own contracts
|
||||||
|
as functions:
|
||||||
|
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
(define (amount? a)
|
(define (amount? a)
|
||||||
(and (number? a) (integer? a) (exact? a) (>= a 0)))
|
(and (number? a) (integer? a) (exact? a) (>= a 0)))
|
||||||
|
@ -141,80 +166,66 @@ scheme
|
||||||
(code:comment "an amount is a natural number of cents")
|
(code:comment "an amount is a natural number of cents")
|
||||||
(code:comment "is the given number an amount?")
|
(code:comment "is the given number an amount?")
|
||||||
[deposit (-> amount? any)]
|
[deposit (-> amount? any)]
|
||||||
[amount? (-> any/c boolean?)])
|
[amount? (-> any/c boolean?)]
|
||||||
|
[balance (-> amount?)])
|
||||||
|
|
||||||
(define this 0)
|
(define amount 0)
|
||||||
(define (deposit a) (set! this (+ this a)))
|
(define (deposit a) (set! amount (+ amount a)))
|
||||||
|
(define (balance) amount)
|
||||||
]
|
]
|
||||||
|
|
||||||
The module introduces a
|
This module define an @racket[amount?] function as uses it as a
|
||||||
predicate, @scheme[amount?]. The @scheme[provide]
|
contract within @racket[->] contracts. When a client calls the
|
||||||
clause refers to this predicate, as a contract, for its
|
@racket[deposit] function as exported with the contract @racket[(->
|
||||||
specification of the contract of
|
amount? any)], it must supply an exact, nonnegative integer, otherwise
|
||||||
@scheme[deposit].
|
the @racket[amount?] function applied to the argument will return
|
||||||
|
@racket[#f], which will cause the contract-monitoring system to blame
|
||||||
|
the client. Similarly, the server module must provide an exact,
|
||||||
|
nonnegative integer as the result of @racket[balance] to remain
|
||||||
|
blameless.
|
||||||
|
|
||||||
Of course it makes no sense to restrict a channel of
|
Of course, it makes no sense to restrict a channel of communication to
|
||||||
communication to values that the client doesn't
|
values that the client doesn't understand. Therefore the module also
|
||||||
understand. Therefore the module also exports
|
exports the @racket[amount?] predicate itself, with a contract saying
|
||||||
the @scheme[amount?] predicate itself, with a contract
|
that it accepts an arbitrary value and returns a boolean.
|
||||||
saying that it accepts an arbitrary value and returns a
|
|
||||||
boolean.
|
|
||||||
|
|
||||||
In this case, we could also have used @scheme[natural-number/c], which
|
In this case, we could also have used @racket[natural-number/c] in
|
||||||
is a contract defined in @schememodname[scheme/contract] that is
|
place of @racket[amount?], since it implies exactly the same check:
|
||||||
equivalent to @scheme[amount] (modulo the name):
|
|
||||||
|
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
|
|
||||||
|
@racketblock[
|
||||||
(provide/contract
|
(provide/contract
|
||||||
(code:comment "an amount is a natural number of cents")
|
[deposit (-> natural-number/c any)]
|
||||||
[deposit (-> natural-number/c any)])
|
[balance (-> natural-number/c)])
|
||||||
|
|
||||||
(define this 0)
|
|
||||||
(define (deposit a) (set! this (+ this a)))
|
|
||||||
]
|
]
|
||||||
|
|
||||||
Lesson: learn about the built-in contracts in @schememodname[scheme/contract].
|
Every function that accepts one argument can be treated as a predicate
|
||||||
|
and thus used as a contract. For combining existing checks into a new
|
||||||
|
one, however, contract combinators such as @racket[and/c] and
|
||||||
|
@racket[or/c] are often useful. For example, here is yet another way
|
||||||
|
to write the contracts above:
|
||||||
|
|
||||||
@ctc-section[#:tag "and-or"]{The @scheme[and/c], @scheme[or/c], and @scheme[listof] Contract Combinators}
|
@racketblock[
|
||||||
|
(define amount/c
|
||||||
Both @scheme[and/c] and @scheme[or/c] combine contracts and
|
|
||||||
they do what you expect them to do.
|
|
||||||
|
|
||||||
For example, if we didn't have @scheme[natural-number/c], the
|
|
||||||
@scheme[amount?] contract is a bit opaque. Instead, we would define it
|
|
||||||
as follows:
|
|
||||||
|
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
|
|
||||||
(define amount
|
|
||||||
(and/c number? integer? exact? (or/c positive? zero?)))
|
(and/c number? integer? exact? (or/c positive? zero?)))
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
(code:comment "an amount is a natural number of cents")
|
[deposit (-> amount/c any)]
|
||||||
(code:comment "is the given number an amount?")
|
[balance (-> amount/c)])
|
||||||
[deposit (-> amount any)])
|
|
||||||
|
|
||||||
(define this 0)
|
|
||||||
(define (deposit a) (set! this (+ this a)))
|
|
||||||
]
|
]
|
||||||
|
|
||||||
That is, amount is a contract that enforces the following conditions: the
|
Other values also serve double duty as contracts. For example, if a
|
||||||
value satisfies @scheme[number?] and @scheme[integer?] and
|
function accepts a number or @racket[#f], @racket[(or/c number? #f)]
|
||||||
@scheme[exact?] and is either @scheme[positive?] or
|
suffices. Similarly, the @racket[amount/c] contract could have been
|
||||||
@scheme[zero?].
|
written with a @racket[0] in place of @racket[zero?]. If you use a
|
||||||
|
regular expression as a contract, the contract accepts strings and
|
||||||
|
byte strings that match the regular expression.
|
||||||
|
|
||||||
Oh, we almost forgot. What do you think @scheme[(listof char?)]
|
Naturally, you can mix your own contract-implementing functions with
|
||||||
means? Hint: it is a contract!
|
combinators like @racket[and/c]. Here is a module for creating strings
|
||||||
|
from banking records:
|
||||||
|
|
||||||
@ctc-section[#:tag "range"]{Restricting the Range of a Function}
|
@racketmod[
|
||||||
|
racket
|
||||||
Consider a utility module for creating strings from banking records:
|
|
||||||
|
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
|
|
||||||
(define (has-decimal? str)
|
(define (has-decimal? str)
|
||||||
(define L (string-length str))
|
(define L (string-length str))
|
||||||
|
@ -230,22 +241,19 @@ scheme
|
||||||
[format-nat (-> natural-number/c
|
[format-nat (-> natural-number/c
|
||||||
(and/c string? has-decimal?))])
|
(and/c string? has-decimal?))])
|
||||||
]
|
]
|
||||||
The contract of the exported function @scheme[format-number] specifies that
|
The contract of the exported function @racket[format-number] specifies
|
||||||
the function consumes a number and produces a string.
|
that the function consumes a number and produces a string. The
|
||||||
|
contract of the exported function @racket[format-nat] is more
|
||||||
The contract of the exported function @scheme[format-nat] is more
|
interesting than the one of @racket[format-number]. It consumes only
|
||||||
interesting than the one of @scheme[format-number]. It consumes only
|
|
||||||
natural numbers. Its range contract promises a string that has a
|
natural numbers. Its range contract promises a string that has a
|
||||||
@litchar{.} in the third position from the right.
|
@litchar{.} in the third position from the right.
|
||||||
|
|
||||||
@(exercise) Strengthen the promise of the range contract for
|
If we want to strengthen the promise of the range contract for
|
||||||
@scheme[format-nat] so that it admits only strings with digits and a single
|
@racket[format-nat] so that it admits only strings with digits and a single
|
||||||
dot.
|
dot, we could write it like this:
|
||||||
|
|
||||||
@(solution)
|
@racketmod[
|
||||||
|
racket
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
|
|
||||||
(define (digit-char? x)
|
(define (digit-char? x)
|
||||||
(member x '(#\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\0)))
|
(member x '(#\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\0)))
|
||||||
|
@ -263,11 +271,10 @@ scheme
|
||||||
(andmap digit-char?
|
(andmap digit-char?
|
||||||
(string->list (substring str (- L 2) L)))))
|
(string->list (substring str (- L 2) L)))))
|
||||||
|
|
||||||
(provide/contract
|
....
|
||||||
...
|
|
||||||
(code:comment "convert a number to a string")
|
|
||||||
[format-number (-> number? string?)]
|
|
||||||
|
|
||||||
|
(provide/contract
|
||||||
|
....
|
||||||
(code:comment "convert an amount (natural number) of cents")
|
(code:comment "convert an amount (natural number) of cents")
|
||||||
(code:comment "into a dollar based string")
|
(code:comment "into a dollar based string")
|
||||||
[format-nat (-> natural-number/c
|
[format-nat (-> natural-number/c
|
||||||
|
@ -275,23 +282,22 @@ scheme
|
||||||
is-decimal-string?))])
|
is-decimal-string?))])
|
||||||
]
|
]
|
||||||
|
|
||||||
|
Alternately, in this case, we could use a regular expression as a
|
||||||
|
contract:
|
||||||
|
|
||||||
@ctc-section[#:tag "coercion"]{Contracts Coerced from Other Values}
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
The contract library treats a number of Scheme values as if they are
|
(provide/contract
|
||||||
contracts directly. We've already seen one main use of that: predicates. Every
|
....
|
||||||
function that accepts one argument can be treated as a predicate
|
(code:comment "convert an amount (natural number) of cents")
|
||||||
and thus used as a contract.
|
(code:comment "into a dollar based string")
|
||||||
|
[format-nat (-> natural-number/c
|
||||||
|
(and/c string?
|
||||||
|
#rx"[0-9]*\\.[0-9][0-9][0-9]"))])
|
||||||
|
]
|
||||||
|
|
||||||
But many other values also play double duty as contracts.
|
@; ------------------------------------------------------------------------
|
||||||
For example, if your function accepts a number or @scheme[#f],
|
|
||||||
@scheme[(or/c number? #f)] suffices. Similarly, the @scheme[result/c] contract
|
|
||||||
could have been written with a @scheme[0] in place of @scheme[zero?].
|
|
||||||
|
|
||||||
Even better, if you use a regular expression as a contract, the contract
|
|
||||||
accepts strings that match the regular expression. For example,
|
|
||||||
the @scheme[is-decimal-string?] predicate could have been written
|
|
||||||
@scheme[#rx"[0-9]*\\.[0-9][0-9][0-9]"].
|
|
||||||
|
|
||||||
@ctc-section{Contracts on Higher-order Functions}
|
@ctc-section{Contracts on Higher-order Functions}
|
||||||
|
|
||||||
|
@ -302,35 +308,84 @@ themselves, can be used as contracts on the arguments and
|
||||||
results of a function.
|
results of a function.
|
||||||
|
|
||||||
For example,
|
For example,
|
||||||
@schemeblock[(-> integer? (-> integer? integer?))]
|
|
||||||
is a contract that describes a curried function. It matches
|
|
||||||
functions that accept one argument and then return another
|
|
||||||
function accepting a second argument before finally
|
|
||||||
returning an integer.
|
|
||||||
|
|
||||||
This contract
|
@racketblock[(-> integer? (-> integer? integer?))]
|
||||||
@schemeblock[(-> (-> integer? integer?) integer?)]
|
|
||||||
describes functions that accept other functions as inputs.
|
|
||||||
|
|
||||||
@ctc-section{The Difference Between @scheme[any] and @scheme[any/c]}
|
is a contract that describes a curried function. It matches functions
|
||||||
|
that accept one argument and then return another function accepting a
|
||||||
|
second argument before finally returning an integer. If a server
|
||||||
|
exports a function @racket[make-adder] with this contract, and if
|
||||||
|
@racket[make-adder] returns a value other than a function, then the
|
||||||
|
server is to blame. If @racket[make-adder] does return a function, but
|
||||||
|
the resulting function is applied to a value other than an integer,
|
||||||
|
then the client is to blame.
|
||||||
|
|
||||||
The contract @scheme[any/c] accepts any value, and
|
Similarly, the contract
|
||||||
@scheme[any] is a keyword that can appear in the range of
|
|
||||||
the function contracts (@scheme[->], @scheme[->*], and
|
@racketblock[(-> (-> integer? integer?) integer?)]
|
||||||
@scheme[->d]), so it is natural to wonder what the
|
|
||||||
difference between these two contracts is:
|
describes functions that accept other functions as its input. If a
|
||||||
@schemeblock[
|
server exports a function @racket[twice] with this contract and the
|
||||||
(-> integer? any)
|
@racket[twice] is applied to a value other than a function of one
|
||||||
(-> integer? any/c)
|
argument, then the client is to blame. If @racket[twice] is applied to
|
||||||
|
a function of one argument and @racket[twice] calls the give function
|
||||||
|
on a value other than an integer, then the server is to blame.
|
||||||
|
|
||||||
|
@; ----------------------------------------------------------------------
|
||||||
|
|
||||||
|
@ctc-section[#:tag "flat-named-contracts"]{Contract Messages with ``???''}
|
||||||
|
|
||||||
|
You wrote your module. You added contracts. You put them into the interface
|
||||||
|
so that client programmers have all the information from interfaces. It's a
|
||||||
|
piece of art:
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
|
(provide/contract
|
||||||
|
[deposit (-> (lambda (x)
|
||||||
|
(and (number? x) (integer? x) (>= x 0)))
|
||||||
|
any)])
|
||||||
|
|
||||||
|
(define this 0)
|
||||||
|
(define (deposit a) ...)
|
||||||
]
|
]
|
||||||
|
|
||||||
Both allow any result, right? There is one important difference:
|
Several clients used your module. Others used their
|
||||||
in the first case, the function may return anything at
|
modules in turn. And all of a sudden one of them sees this error
|
||||||
all, including multiple values. In the second case, the
|
message:
|
||||||
function may return any value, but not more than one. For
|
|
||||||
example, this function:
|
@inset-flow{@racketerror{bank-client broke the contract (-> ??? any)
|
||||||
@schemeblock[
|
it had with myaccount on deposit; expected <???>, given: -10}}
|
||||||
(define (f x) (values (+ x 1) (- x 1)))
|
|
||||||
]
|
Clearly, @racket[bank-client] is a module that uses @racket[myaccount]
|
||||||
meets the first contract, but not the second one.}
|
but what is the @racketerror{???} doing there? Wouldn't it be nice if
|
||||||
|
we had a name for this class of data much like we have string, number,
|
||||||
|
and so on?
|
||||||
|
|
||||||
|
For this situation, Racket provides @deftech{flat named
|
||||||
|
contracts}. The use of ``contract'' in this term shows that contracts
|
||||||
|
are first-class values. The ``flat'' means that the collection of data
|
||||||
|
is a subset of the built-in atomic classes of data; they are described
|
||||||
|
by a predicate that consumes all Racket values and produces a
|
||||||
|
boolean. The ``named'' part says what we want to do, which is to name
|
||||||
|
the contract so that error messages become intelligible:
|
||||||
|
|
||||||
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
|
(define (amount? x) (and (number? x) (integer? x) (>= x 0)))
|
||||||
|
(define amount (flat-named-contract 'amount amount?))
|
||||||
|
|
||||||
|
(provide/contract
|
||||||
|
[deposit (amount . -> . any)])
|
||||||
|
|
||||||
|
(define this 0)
|
||||||
|
(define (deposit a) ...)
|
||||||
|
]
|
||||||
|
|
||||||
|
With this little change, the error message becomes all of the
|
||||||
|
sudden quite readable:
|
||||||
|
|
||||||
|
@inset-flow{@racketerror{bank-client broke the contract (-> amount
|
||||||
|
any) it had with myaccount on deposit; expected <amount>, given: -10}}
|
||||||
|
|
||||||
|
|
|
@ -3,12 +3,12 @@
|
||||||
scribble/eval
|
scribble/eval
|
||||||
"guide-utils.ss"
|
"guide-utils.ss"
|
||||||
"contracts-utils.ss"
|
"contracts-utils.ss"
|
||||||
(for-label scheme/contract))
|
(for-label racket/contract))
|
||||||
|
|
||||||
@title[#:tag "contracts-struct"]{Contracts on Structures}
|
@title[#:tag "contracts-struct"]{Contracts on Structures}
|
||||||
|
|
||||||
Modules deal with structures in two ways. First they export
|
Modules deal with structures in two ways. First they export
|
||||||
@scheme[struct] definitions, i.e., the ability to create
|
@racket[struct] definitions, i.e., the ability to create
|
||||||
structs of a certain kind, to access their fields, to modify
|
structs of a certain kind, to access their fields, to modify
|
||||||
them, and to distinguish structs of this kind against every
|
them, and to distinguish structs of this kind against every
|
||||||
other kind of value in the world. Second, on occasion a
|
other kind of value in the world. Second, on occasion a
|
||||||
|
@ -17,12 +17,14 @@ its fields contain values of a certain kind. This section
|
||||||
explains how to protect structs with contracts for both
|
explains how to protect structs with contracts for both
|
||||||
uses.
|
uses.
|
||||||
|
|
||||||
@ctc-section[#:tag "single-struct"]{Promising Something About a Specific Structure}
|
@; ----------------------------------------------------------------------
|
||||||
|
@ctc-section[#:tag "single-struct"]{Guarantees for a Specific Value}
|
||||||
|
|
||||||
Yes. If your module defines a variable to be a structure, then on export you
|
If your module defines a variable to be a structure, then you can
|
||||||
can specify the structures shape:
|
specify the structure's shape using @racket[struct/c]:
|
||||||
@schememod[
|
|
||||||
scheme
|
@racketmod[
|
||||||
|
racket
|
||||||
(require lang/posn)
|
(require lang/posn)
|
||||||
|
|
||||||
(define origin (make-posn 0 0))
|
(define origin (make-posn 0 0))
|
||||||
|
@ -32,105 +34,98 @@ scheme
|
||||||
]
|
]
|
||||||
|
|
||||||
In this example, the module imports a library for representing positions, which
|
In this example, the module imports a library for representing positions, which
|
||||||
exports a @scheme[posn] structure. One of the @scheme[posn]s it creates
|
exports a @racket[posn] structure. One of the @racket[posn]s it creates
|
||||||
and exports stands for the origin, i.e., @tt{(0,0)}, of the grid.
|
and exports stands for the origin, i.e., @tt{(0,0)}, of the grid.
|
||||||
|
|
||||||
@ctc-section[#:tag "single-vector"]{Promising Something About a Specific Vector}
|
@margin-note{See also @racket[vector/c] and similar contract
|
||||||
|
combinators for (flat) compound data.}
|
||||||
|
|
||||||
Yes, again. See the help desk for information on @scheme[vector/c] and
|
@; ----------------------------------------------------------------------
|
||||||
similar contract combinators for (flat) compound data.
|
@ctc-section[#:tag "define-struct"]{Guarantees for All Values}
|
||||||
|
|
||||||
@ctc-section[#:tag "define-struct"]{Ensuring that All Structs are Well-Formed}
|
The book @|HtDP| teaches that @racket[posn]s should contain only
|
||||||
|
numbers in their two fields. With contracts we would enforce this
|
||||||
|
informal data definition as follows:
|
||||||
|
|
||||||
The book @link["http://www.htdp.org/"]{@italic{How to Design
|
@racketmod[
|
||||||
Programs}} teaches that @scheme[posn]s should contain only
|
racket
|
||||||
numbers in their two fields. With contracts we would enforce
|
(struct posn (x y))
|
||||||
this informal data definition as follows:
|
|
||||||
|
|
||||||
@schememod[
|
|
||||||
scheme
|
|
||||||
(define-struct posn (x y))
|
|
||||||
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
[struct posn ((x number?) (y number?))]
|
[struct posn ((x number?) (y number?))]
|
||||||
[p-okay posn?]
|
[p-okay posn?]
|
||||||
[p-sick posn?])
|
[p-sick posn?])
|
||||||
|
|
||||||
(define p-okay (make-posn 10 20))
|
(define p-okay (posn 10 20))
|
||||||
(define p-sick (make-posn 'a 'b))
|
(define p-sick (posn 'a 'b))
|
||||||
]
|
]
|
||||||
|
|
||||||
This module exports the entire structure definition: @scheme[make-posn],
|
This module exports the entire structure definition: @racket[posn],
|
||||||
@scheme[posn?], @scheme[posn-x], @scheme[posn-y],
|
@racket[posn?], @racket[posn-x], @racket[posn-y],
|
||||||
@scheme[set-posn-x!], and @scheme[set-posn-y!]. Each function enforces
|
@racket[set-posn-x!], and @racket[set-posn-y!]. Each function enforces
|
||||||
or promises that the two fields of a @scheme[posn] structure are
|
or promises that the two fields of a @racket[posn] structure are
|
||||||
numbers---when the values flow across the module boundary.
|
numbers --- when the values flow across the module boundary. Thus, if
|
||||||
|
a client calls @racket[posn] on @racket[10] and @racket['a], the
|
||||||
|
contract system signals a contract violation.
|
||||||
|
|
||||||
Thus, if a client calls @scheme[make-posn] on @scheme[10] and
|
The creation of @racket[p-sick] inside of the @racket[posn] module,
|
||||||
@scheme['a], the contract system signals a contract
|
however, does not violate the contracts. The function @racket[posn] is
|
||||||
violation.
|
used internally, so @racket['a] and @racket['b] don't cross the module
|
||||||
|
boundary. Similarly, when @racket[p-sick] crosses the boundary of
|
||||||
The creation of @scheme[p-sick] inside of the @scheme[posn] module,
|
@racket[posn], the contract promises a @racket[posn?] and nothing
|
||||||
however, does not violate the contracts. The function @scheme[make-posn] is
|
else. In particular, this check does @italic{not} require that the
|
||||||
used internally so @scheme['a] and @scheme['b] don't cross the module
|
fields of @racket[p-sick] are numbers.
|
||||||
boundary. Similarly, when @scheme[p-sick] crosses the boundary of
|
|
||||||
@scheme[posn], the contract promises a @scheme[posn?] and nothing
|
|
||||||
else. In particular, this check does @italic{not} require that the fields of
|
|
||||||
@scheme[p-sick] are numbers.
|
|
||||||
|
|
||||||
The association of contract checking with module boundaries implies that
|
The association of contract checking with module boundaries implies that
|
||||||
@scheme[p-okay] and @scheme[p-sick] look alike from a client's
|
@racket[p-okay] and @racket[p-sick] look alike from a client's
|
||||||
perspective until the client extracts the pieces:
|
perspective until the client extracts the pieces:
|
||||||
|
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme
|
racket
|
||||||
(require lang/posn)
|
(require lang/posn)
|
||||||
|
|
||||||
... (posn-x p-sick) ...
|
... (posn-x p-sick) ...
|
||||||
]
|
]
|
||||||
|
|
||||||
Using @scheme[posn-x] is the only way the client can find out what
|
Using @racket[posn-x] is the only way the client can find out what
|
||||||
a @scheme[posn] contains in the @scheme[x] field. The application of
|
a @racket[posn] contains in the @racket[x] field. The application of
|
||||||
@scheme[posn-x] sends @scheme[p-sick] back into the
|
@racket[posn-x] sends @racket[p-sick] back into the
|
||||||
@scheme[posn] module and the result value -- @scheme['a] here -- back to
|
@racket[posn] module and the result value -- @racket['a] here -- back to
|
||||||
the client, again across the module boundary. At this very point, the contract
|
the client, again across the module boundary. At this very point, the contract
|
||||||
system discovers that a promise is broken. Specifically, @scheme[posn-x]
|
system discovers that a promise is broken. Specifically, @racket[posn-x]
|
||||||
doesn't return a number but a symbol and is therefore blamed.
|
doesn't return a number but a symbol and is therefore blamed.
|
||||||
|
|
||||||
This specific example shows that the explanation for a contract violation
|
This specific example shows that the explanation for a contract violation
|
||||||
doesn't always pinpoint the source of the error. The good news is that the
|
doesn't always pinpoint the source of the error. The good news is that the
|
||||||
error is located in the @scheme[posn] module. The bad news is that the
|
error is located in the @racket[posn] module. The bad news is that the
|
||||||
explanation is misleading. Although it is true that @scheme[posn-x]
|
explanation is misleading. Although it is true that @racket[posn-x]
|
||||||
produced a symbol instead of a number, it is the fault of the programmer who
|
produced a symbol instead of a number, it is the fault of the programmer who
|
||||||
created a @scheme[posn] from symbols, i.e., the programmer who added
|
created a @racket[posn] from symbols, i.e., the programmer who added
|
||||||
|
|
||||||
@schemeblock[
|
@racketblock[
|
||||||
(define p-sick (make-posn 'a 'b))
|
(define p-sick (posn 'a 'b))
|
||||||
]
|
]
|
||||||
to the module. So, when you are looking for bugs based on contract violations,
|
|
||||||
keep this example in mind.
|
|
||||||
|
|
||||||
@(exercise) Use your knowledge from the
|
to the module. So, when you are looking for bugs based on contract
|
||||||
@ctc-link["single-struct"] section on exporting specific
|
violations, keep this example in mind.
|
||||||
structs and change the contract for @scheme[p-sick] so that
|
|
||||||
the error is caught when @scheme[sick] is exported.
|
|
||||||
|
|
||||||
@(solution)
|
If we want to fix the contract for @racket[p-sick] so that the error
|
||||||
|
is caught when @racket[sick] is exported, a single change suffices:
|
||||||
|
|
||||||
A single change suffices:
|
@racketblock[
|
||||||
|
|
||||||
@schemeblock[
|
|
||||||
(provide/contract
|
(provide/contract
|
||||||
...
|
...
|
||||||
[p-sick (struct/c posn number? number?)])
|
[p-sick (struct/c posn number? number?)])
|
||||||
]
|
]
|
||||||
|
|
||||||
Instead of exporting @scheme[p-sick] as a plain @scheme[posn?], we use a
|
That is, instead of exporting @racket[p-sick] as a plain
|
||||||
@scheme[struct/c] contract to enforce constraints on its components.
|
@racket[posn?], we use a @racket[struct/c] contract to enforce
|
||||||
|
constraints on its components.
|
||||||
|
|
||||||
|
@; ----------------------------------------------------------------------
|
||||||
@ctc-section[#:tag "lazy-contracts"]{Checking Properties of Data Structures}
|
@ctc-section[#:tag "lazy-contracts"]{Checking Properties of Data Structures}
|
||||||
|
|
||||||
Contracts written using @scheme[struct/c] immediately
|
Contracts written using @racket[struct/c] immediately
|
||||||
check the fields of the data structure, but sometimes this
|
check the fields of the data structure, but sometimes this
|
||||||
can have disastrous effects on the performance of a program
|
can have disastrous effects on the performance of a program
|
||||||
that does not, itself, inspect the entire data structure.
|
that does not, itself, inspect the entire data structure.
|
||||||
|
@ -144,12 +139,12 @@ subtree are smaller than the number in the node, and all of
|
||||||
the numbers in the right subtree are larger than the number
|
the numbers in the right subtree are larger than the number
|
||||||
in the node.
|
in the node.
|
||||||
|
|
||||||
We can implement a search function @scheme[in?] that takes
|
We can implement a search function @racket[in?] that takes
|
||||||
advantage of the structure of the binary search tree.
|
advantage of the structure of the binary search tree.
|
||||||
@schememod[
|
@racketmod[
|
||||||
scheme
|
racket
|
||||||
|
|
||||||
(define-struct node (val left right))
|
(struct node (val left right))
|
||||||
|
|
||||||
(code:comment "determines if `n' is in the binary search tree `b',")
|
(code:comment "determines if `n' is in the binary search tree `b',")
|
||||||
(code:comment "exploiting the binary search tree invariant")
|
(code:comment "exploiting the binary search tree invariant")
|
||||||
|
@ -180,48 +175,47 @@ scheme
|
||||||
]
|
]
|
||||||
|
|
||||||
In a full binary search tree, this means that
|
In a full binary search tree, this means that
|
||||||
the @scheme[in?] function only has to explore a
|
the @racket[in?] function only has to explore a
|
||||||
logarithmic number of nodes.
|
logarithmic number of nodes.
|
||||||
|
|
||||||
The contract on @scheme[in?] guarantees that its input
|
The contract on @racket[in?] guarantees that its input
|
||||||
is a binary search tree. But a little careful thought
|
is a binary search tree. But a little careful thought
|
||||||
reveals that this contract defeats the purpose of the binary
|
reveals that this contract defeats the purpose of the binary
|
||||||
search tree algorithm. In particular, consider the
|
search tree algorithm. In particular, consider the
|
||||||
inner @scheme[cond] in the @scheme[in?]
|
inner @racket[cond] in the @racket[in?]
|
||||||
function. This is where the @scheme[in?] function gets
|
function. This is where the @racket[in?] function gets
|
||||||
its speed: it avoids searching an entire subtree at each
|
its speed: it avoids searching an entire subtree at each
|
||||||
recursive call. Now compare that to the @scheme[bst-between?]
|
recursive call. Now compare that to the @racket[bst-between?]
|
||||||
function. In the case that it returns @scheme[#t], it
|
function. In the case that it returns @racket[#t], it
|
||||||
traverses the entire tree, meaning that the speedup
|
traverses the entire tree, meaning that the speedup
|
||||||
of @scheme[in?] is lost.
|
of @racket[in?] is lost.
|
||||||
|
|
||||||
In order to fix that, we can employ a new strategy for
|
In order to fix that, we can employ a new strategy for
|
||||||
checking the binary search tree contract. In particular, if
|
checking the binary search tree contract. In particular, if
|
||||||
we only checked the contract on the nodes
|
we only checked the contract on the nodes
|
||||||
that @scheme[in?] looks at, we can still guarantee that
|
that @racket[in?] looks at, we can still guarantee that
|
||||||
the tree is at least partially well-formed, but without
|
the tree is at least partially well-formed, but without
|
||||||
changing the complexity.
|
changing the complexity.
|
||||||
|
|
||||||
To do that, we need to
|
To do that, we need to use @racket[define-contract-struct] in place of
|
||||||
use @scheme[define-contract-struct] in place
|
@racket[struct]. Like @racket[struct] (and more like
|
||||||
of @scheme[define-struct]. Like @scheme[define-struct],
|
@racket[define-struct]), @racket[define-contract-struct] defines a
|
||||||
@scheme[define-contract-struct] defines a maker,
|
maker, predicate, and selectors for a new structure. Unlike
|
||||||
predicate, and selectors for a new
|
@racket[define-struct], it also defines contract combinators, in this
|
||||||
structure. Unlike @scheme[define-struct], it also
|
case @racket[node/c] and @racket[node/dc]. Also unlike
|
||||||
defines contract combinators, in this
|
@racket[define-struct], it does not allow mutators, making its structs
|
||||||
case @scheme[node/c] and @scheme[node/dc]. Also unlike
|
always immutable.
|
||||||
@scheme[define-struct], it does not allow mutators, making
|
|
||||||
its structs always immutable.
|
|
||||||
|
|
||||||
The @scheme[node/c] function accepts a contract for each
|
The @racket[node/c] function accepts a contract for each
|
||||||
field of the struct and returns a contract on the
|
field of the struct and returns a contract on the
|
||||||
struct. More interestingly, the syntactic
|
struct. More interestingly, the syntactic
|
||||||
form @scheme[node/dc] allows us to write dependent
|
form @racket[node/dc] allows us to write dependent
|
||||||
contracts, i.e., contracts where some of the contracts on
|
contracts, i.e., contracts where some of the contracts on
|
||||||
the fields depend on the values of other fields. We can use
|
the fields depend on the values of other fields. We can use
|
||||||
this to define the binary search tree contract:
|
this to define the binary search tree contract:
|
||||||
@schememod[
|
|
||||||
scheme
|
@racketmod[
|
||||||
|
racket
|
||||||
|
|
||||||
(define-contract-struct node (val left right))
|
(define-contract-struct node (val left right))
|
||||||
|
|
||||||
|
@ -245,30 +239,30 @@ scheme
|
||||||
[in? (number? bst/c . -> . boolean?)])
|
[in? (number? bst/c . -> . boolean?)])
|
||||||
]
|
]
|
||||||
|
|
||||||
In general, each use of @scheme[node/dc] must name the
|
In general, each use of @racket[node/dc] must name the
|
||||||
fields and then specify contracts for each field. In the
|
fields and then specify contracts for each field. In the
|
||||||
above, the @scheme[val] field is a contract that accepts
|
above, the @racket[val] field is a contract that accepts
|
||||||
values between @scheme[low] and @scheme[high].
|
values between @racket[low] and @racket[high].
|
||||||
The @scheme[left] and @scheme[right] fields are
|
The @racket[left] and @racket[right] fields are
|
||||||
dependent on the value of the @scheme[val] field,
|
dependent on the value of the @racket[val] field,
|
||||||
indicated by their second sub-expressions. Their contracts
|
indicated by their second sub-expressions. Their contracts
|
||||||
are built by recursive calls to
|
are built by recursive calls to
|
||||||
the @scheme[bst-between/c] function. Taken together,
|
the @racket[bst-between/c] function. Taken together,
|
||||||
this contract ensures the same thing that
|
this contract ensures the same thing that
|
||||||
the @scheme[bst-between?] function checked in the
|
the @racket[bst-between?] function checked in the
|
||||||
original example, but here the checking only happens
|
original example, but here the checking only happens
|
||||||
as @scheme[in?] explores the tree.
|
as @racket[in?] explores the tree.
|
||||||
|
|
||||||
Although this contract improves the performance
|
Although this contract improves the performance
|
||||||
of @scheme[in?], restoring it to the logarithmic
|
of @racket[in?], restoring it to the logarithmic
|
||||||
behavior that the contract-less version had, it is still
|
behavior that the contract-less version had, it is still
|
||||||
imposes a fairly large constant overhead. So, the contract
|
imposes a fairly large constant overhead. So, the contract
|
||||||
library also provides @scheme[define-opt/c] that brings
|
library also provides @racket[define-opt/c] that brings
|
||||||
down that constant factor by optimizing its body. Its shape
|
down that constant factor by optimizing its body. Its shape
|
||||||
is just like the @scheme[define] above. It expects its
|
is just like the @racket[define] above. It expects its
|
||||||
body to be a contract and then optimizes that contract.
|
body to be a contract and then optimizes that contract.
|
||||||
|
|
||||||
@schemeblock[
|
@racketblock[
|
||||||
(define-opt/c (bst-between/c low high)
|
(define-opt/c (bst-between/c low high)
|
||||||
(or/c null?
|
(or/c null?
|
||||||
(node/dc [val (between/c low high)]
|
(node/dc [val (between/c low high)]
|
||||||
|
|
|
@ -5,7 +5,7 @@
|
||||||
|
|
||||||
@title[#:tag "contracts" #:style 'toc]{Contracts}
|
@title[#:tag "contracts" #:style 'toc]{Contracts}
|
||||||
|
|
||||||
This chapter provides a gentle introduction to PLT Scheme's
|
This chapter provides a gentle introduction to Racket's
|
||||||
contract system.
|
contract system.
|
||||||
|
|
||||||
@refdetails["contracts"]{contracts}
|
@refdetails["contracts"]{contracts}
|
||||||
|
|
|
@ -28,7 +28,7 @@ A @racket[lambda] form with @math{n} @racket[_arg-id]s accepts
|
||||||
]
|
]
|
||||||
|
|
||||||
@;------------------------------------------------------------------------
|
@;------------------------------------------------------------------------
|
||||||
@section{Declaring a Rest Argument}
|
@section[#:tag "rest-args"]{Declaring a Rest Argument}
|
||||||
|
|
||||||
A @racket[lambda] expression can also have the form
|
A @racket[lambda] expression can also have the form
|
||||||
|
|
||||||
|
@ -207,7 +207,7 @@ remaining by-position arguments.
|
||||||
@refdetails["lambda"]{function expressions}
|
@refdetails["lambda"]{function expressions}
|
||||||
|
|
||||||
@;------------------------------------------------------------------------
|
@;------------------------------------------------------------------------
|
||||||
@section{Arity-Sensitive Functions: @racket[case-lambda]}
|
@section[#:tag "case-lambda"]{Arity-Sensitive Functions: @racket[case-lambda]}
|
||||||
|
|
||||||
The @racket[case-lambda] form creates a function that can have
|
The @racket[case-lambda] form creates a function that can have
|
||||||
completely different behaviors depending on the number of arguments
|
completely different behaviors depending on the number of arguments
|
||||||
|
|
|
@ -28,9 +28,9 @@ evaluator is created using @scheme[make-base-eval]. See also
|
||||||
Uses of @scheme[code:comment] and @schemeidfont{code:blank} are
|
Uses of @scheme[code:comment] and @schemeidfont{code:blank} are
|
||||||
stipped from each @scheme[datum] before evaluation.
|
stipped from each @scheme[datum] before evaluation.
|
||||||
|
|
||||||
If a @scheme[datum] has the form @scheme[(eval:alts #,(svar
|
If a @scheme[datum] has the form @scheme[(@#,indexed-scheme[eval:alts]
|
||||||
show-datum) #,(svar eval-datum))], then @svar[show-datum] is typeset,
|
#,(svar show-datum) #,(svar eval-datum))], then @svar[show-datum] is
|
||||||
while @svar[eval-datum] is evaluated.}
|
typeset, while @svar[eval-datum] is evaluated.}
|
||||||
|
|
||||||
|
|
||||||
@defform*[[(interaction-eval datum)
|
@defform*[[(interaction-eval datum)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user