You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
typesetting/quad/qtest/mds/contracts.md

145 KiB

Contracts

This chapter provides a gentle introduction to Rackets contract system.

+[missing] in [missing] provides more on contracts.

1 Contracts and Boundaries                         
  1.1 Contract Violations                          
  1.2 Experimenting with Contracts and Modules     
  1.3 Experimenting with Nested Contract Boundaries
                                                   
2 Simple Contracts on Functions                    
  2.1 Styles of `->`                               
  2.2 Using `define/contract` and `->`             
  2.3 `any` and `any/c`                            
  2.4 Rolling Your Own Contracts                   
  2.5 Contracts on Higher-order Functions          
  2.6 Contract Messages with “???”                 
  2.7 Dissecting a contract error message          
                                                   
3 Contracts on Functions in General                
  3.1 Optional Arguments                           
  3.2 Rest Arguments                               
  3.3 Keyword Arguments                            
  3.4 Optional Keyword Arguments                   
  3.5 Contracts for `case-lambda`                  
  3.6 Argument and Result Dependencies             
  3.7 Checking State Changes                       
  3.8 Multiple Result Values                       
  3.9 Fixed but Statically Unknown Arities         
                                                   
4 Contracts: A Thorough Example                    
                                                   
5 Contracts on Structures                          
  5.1 Guarantees for a Specific Value              
  5.2 Guarantees for All Values                    
  5.3 Checking Properties of Data Structures       
                                                   
6 Abstract Contracts using `#:exists` and `#:∃`    
                                                   
7 Additional Examples                              
  7.1 A Customer-Manager Component                 
  7.2 A Parameteric \(Simple\) Stack               
  7.3 A Dictionary                                 
  7.4 A Queue                                      
                                                   
8 Building New Contracts                           
  8.1 Contract Struct Properties                   
  8.2 With all the Bells and Whistles              
                                                   
9 Gotchas                                          
  9.1 Contracts and `eq?`                          
  9.2 Contract boundaries and `define/contract`    
  9.3 Exists Contracts and Predicates              
  9.4 Defining Recursive Contracts                 
  9.5 Mixing `set!` and `contract-out`             

1. Contracts and Boundaries

Like a contract between two business partners, a software contract is an agreement between two parties. The agreement specifies obligations and guarantees for each “product” or value that is handed from one party to the other.

A contract thus establishes a boundary between the two parties. Whenever a value crosses this boundary, the contract monitoring system performs contract checks, making sure the partners abide by the established contract.

In this spirit, Racket encourages contracts mainly at module boundaries. Specifically, programmers may attach contracts to provide clauses and thus impose constraints and promises on the use of exported values. For example, the export specification

#lang racket                               
                                           
(provide (contract-out [amount positive?]))
                                           
(define amount ...)                        

promises to all clients of the above module that the value of amount will always be a positive number. The contract system monitors the modules obligation carefully. Every time a client refers to amount, the monitor checks that the value of amount is indeed a positive number.

The contracts library is built into the Racket language, but if you wish to use racket/base, you can explicitly require the contracts library like this:

#lang racket/base                                     
(require racket/contract) ; now we can write contracts
                                                      
(provide (contract-out [amount positive?]))           
                                                      
(define amount ...)                                   

1.1. Contract Violations

If we bind amount to a number that is not positive,

#lang racket                               
                                           
(provide (contract-out [amount positive?]))
                                           
(define amount 0)                          

then, when the module is required, the monitoring system signals a violation of the contract and blames the module for breaking its promises.

An even bigger mistake would be to bind amount to a non-number value:

#lang racket                               
                                           
(provide (contract-out [amount positive?]))
                                           
(define amount 'amount)                    

In this case, the monitoring system will apply positive? to a symbol, but positive? reports an error, because its domain is only numbers. To make the contract capture our intentions for all Racket values, we can ensure that the value is both a number and is positive, combining the two contracts with and/c:

(provide (contract-out [amount (and/c number? positive?)]))

1.2. Experimenting with Contracts and Modules

All of the contracts and modules in this chapter (excluding those just following) are written using the standard #lang syntax for describing modules. Since modules serve as the boundary between parties in a contract, examples involve multiple modules.

To experiment with multiple modules within a single module or within DrRackets definitions area, use Rackets submodules. For example, try the example earlier in this section like this:

#lang racket                                                 
                                                             
(module+ server                                              
  (provide (contract-out [amount (and/c number? positive?)]))
  (define amount 150))                                       
                                                             
(module+ main                                                
  (require (submod ".." server))                             
  (+ amount 10))                                             

Each of the modules and their contracts are wrapped in parentheses with the module+ keyword at the front. The first form after module is the name of the module to be used in a subsequent require statement (where each reference through a require prefixes the name with "..").

1.3. Experimenting with Nested Contract Boundaries

In many cases, it makes sense to attach contracts at module boundaries. It is often convenient, however, to be able to use contracts at a finer granularity than modules. The define/contract form enables this kind of use:

#lang racket               
                           
(define/contract amount    
  (and/c number? positive?)
  150)                     
                           
(+ amount 10)              

In this example, the define/contract form establishes a contract boundary between the definition of amount and its surrounding context. In other words, the two parties here are the definition and the module that contains it.

Forms that create these nested contract boundaries can sometimes be subtle to use because they may have unexpected performance implications or blame a party that may seem unintuitive. These subtleties are explained in Using define/contract and -> and Contract boundaries and define/contract.

2. Simple Contracts on Functions

A mathematical function has a domain and a range. The domain indicates the kind of values that the function can accept as arguments, and the range indicates the kind of values that it produces. The conventional notation for describing a function with its domain and range is

f : A -> B

where A is the domain of the function and B is the range.

Functions in a programming language have domains and ranges, too, and a contract can ensure that a function receives only values in its domain and produces only values in its range. A -> creates such a contract for a function. The forms after a -> specify contracts for the domains and finally a contract for the range.

Here is a module that might represent a bank account:

#lang racket                                   
                                               
(provide (contract-out                         
          [deposit (-> number? any)]           
          [balance (-> number?)]))             
                                               
(define amount 0)                              
(define (deposit a) (set! amount (+ amount a)))
(define (balance) amount)                      

The module exports two functions:

  • deposit, which accepts a number and returns some value that is not specified in the contract, and

  • 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 clientserver 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 deposit to 'millions, it would violate the contract. The contract-monitoring system would catch this violation and blame the client for breaking the contract with the above module. In contrast, if the balance function were to return 'broke, the contract-monitoring system would blame the server module.

A -> by itself is not a contract; it is a contract combinator, which combines other contracts to form a contract.

2.1. Styles of ->

If you are used to mathematical functions, 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 How to Design Programs, you have seen this many times. Indeed, you may have seen contracts such as these in other peoples code:

(provide (contract-out                    
          [deposit (number? . -> . any)]))

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, as described in [missing]. Thus,

(number? . -> . any)

is just another way of writing

(-> number? any)

2.2. Using define/contract and ->

The define/contract form introduced in Experimenting with Nested Contract Boundaries can also be used to define functions that come with a contract. For example,

(define/contract (deposit amount)
  (-> number? any)               
  ; implementation goes here     
  ....)                          

which defines the deposit function with the contract from earlier. Note that this has two potentially important impacts on the use of deposit:

  • The contract will be checked on any call to deposit that is outside of the definition of deposit even those inside the module in which it is defined. Because there may be many calls inside the module, this checking may cause the contract to be checked too often, which could lead to a performance degradation. This is especially true if the function is called repeatedly from a loop.

  • In some situations, a function may be written to accept a more lax set of inputs when called by other code in the same module. For such use cases, the contract boundary established by define/contract is too strict.

2.3. any and any/c

The any contract used for deposit matches any kind of result, and it can only be used in the range position of a function contract. Instead of any above, we could use the more specific contract void?, which says that the function will always return the (void) value. The 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 cant do much with the value. In contrast, any tells the monitoring system not to check the return value, it tells a potential client that the “server” module makes no promises at all about the functions return value, even whether it is a single value or multiple values.

The any/c contract is similar to any, in that it makes no demands on a value. Unlike any, any/c indicates a single value, and it is suitable for use as an argument contract. Using any/c as a range contract imposes a check that the function produces a single value. That is,

(-> integer? any)

describes a function that accepts an integer and returns any number of values, while

(-> 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

(define (f x) (values (+ x 1) (- x 1)))

matches (-> integer? any), but not (-> integer? any/c).

Use any/c as a result contract when it is particularly important to promise a single result from a function. Use any when you want to promise as little as possible (and incur as little checking as possible) for a functions result.

2.4. Rolling Your Own Contracts

The deposit function adds the given number to the value of amount. While the functions 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:

#lang racket                                         
                                                     
(define (amount? a)                                  
  (and (number? a) (integer? a) (exact? a) (>= a 0)))
                                                     
(provide (contract-out                               
          ; an amount is a natural number of cents   
          ; is the given number an amount?           
          [deposit (-> amount? any)]                 
          [amount? (-> any/c boolean?)]              
          [balance (-> amount?)]))                   
                                                     
(define amount 0)                                    
(define (deposit a) (set! amount (+ amount a)))      
(define (balance) amount)                            

This module defines an amount? function and uses it as a contract within -> contracts. When a client calls the deposit function as exported with the contract (-> amount? any), it must supply an exact, nonnegative integer, otherwise the amount? function applied to the argument will return #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 balance to remain blameless.

Of course, it makes no sense to restrict a channel of communication to values that the client doesnt understand. Therefore the module also exports the amount? predicate itself, with a contract saying that it accepts an arbitrary value and returns a boolean.

In this case, we could also have used natural-number/c in place of amount?, since it implies exactly the same check:

(provide (contract-out                       
          [deposit (-> natural-number/c any)]
          [balance (-> natural-number/c)]))  

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 and/c and or/c are often useful. For example, here is yet another way to write the contracts above:

(define amount/c                                         
  (and/c number? integer? exact? (or/c positive? zero?)))
                                                         
(provide (contract-out                                   
          [deposit (-> amount/c any)]                    
          [balance (-> amount/c)]))                      

Other values also serve double duty as contracts. For example, if a function accepts a number or #f, (or/c number? #f) suffices. Similarly, the amount/c contract could have been written with a 0 in place of zero?. If you use a regular expression as a contract, the contract accepts strings and byte strings that match the regular expression.

Naturally, you can mix your own contract-implementing functions with combinators like and/c. Here is a module for creating strings from banking records:

#lang racket                                              
                                                          
(define (has-decimal? str)                                
  (define L (string-length str))                          
  (and (>= L 3)                                           
       (char=? #\. (string-ref str (- L 3)))))            
                                                          
(provide (contract-out                                    
          ; convert a random number to a string           
          [format-number (-> number? string?)]            
                                                          
          ; convert an amount into a string with a decimal
          ; point, as in an amount of US currency         
          [format-nat (-> natural-number/c                
                          (and/c string? has-decimal?))]))

The contract of the exported function format-number specifies that the function consumes a number and produces a string. The contract of the exported function format-nat is more interesting than the one of format-number. It consumes only natural numbers. Its range contract promises a string that has a . in the third position from the right.

If we want to strengthen the promise of the range contract for format-nat so that it admits only strings with digits and a single dot, we could write it like this:

#lang racket                                              
                                                          
(define (digit-char? x)                                   
  (member x '(#\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\0)))  
                                                          
(define (has-decimal? str)                                
  (define L (string-length str))                          
  (and (>= L 3)                                           
       (char=? #\. (string-ref str (- L 3)))))            
                                                          
(define (is-decimal-string? str)                          
  (define L (string-length str))                          
  (and (has-decimal? str)                                 
       (andmap digit-char?                                
               (string->list (substring str 0 (- L 3))))  
       (andmap digit-char?                                
               (string->list (substring str (- L 2) L)))))
                                                          
....                                                      
                                                          
(provide (contract-out                                    
          ....                                            
          ; convert an  amount (natural number) of cents  
          ; into a dollar-based string                    
          [format-nat (-> natural-number/c                
                          (and/c string?                  
                                 is-decimal-string?))]))  

Alternately, in this case, we could use a regular expression as a contract:

#lang racket                                                  
                                                              
(provide                                                      
 (contract-out                                                
  ....                                                        
  ; convert an  amount (natural number) of cents              
  ; into a dollar-based string                                
  [format-nat (-> natural-number/c                            
                  (and/c string? #rx"[0-9]*\\.[0-9][0-9]"))]))

2.5. Contracts on Higher-order Functions

Function contracts are not just restricted to having simple predicates on their domains or ranges. Any of the contract combinators discussed here, including function contracts themselves, can be used as contracts on the arguments and results of a function.

For example,

(-> 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. If a server exports a function make-adder with this contract, and if make-adder returns a value other than a function, then the server is to blame. If 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.

Similarly, the contract

(-> (-> integer? integer?) integer?)

describes functions that accept other functions as its input. If a server exports a function twice with this contract and the twice is applied to a value other than a function of one argument, then the client is to blame. If twice is applied to a function of one argument and twice calls the given function on a value other than an integer, then the server is to blame.

2.6. 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. Its a piece of art:

> (module bank-server racket                                 
    (provide                                                 
     (contract-out                                           
      [deposit (-> (λ (x)                                    
                     (and (number? x) (integer? x) (>= x 0)))
                   any)]))                                   
                                                             
    (define total 0)                                         
    (define (deposit a) (set! total (+ a total))))           

Several clients used your module. Others used their modules in turn. And all of a sudden one of them sees this error message:

> (require 'bank-server)             
> (deposit -10)                      
deposit: contract violation          
  expected: ???                      
  given: -10                         
  in: the 1st argument of            
      (-> ??? any)                   
  contract from: bank-server         
  blaming: top-level                 
   (assuming the contract is correct)
  at: eval:2.0                       

What is the ??? doing there? Wouldnt 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 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:

> (module improved-bank-server racket                          
    (provide                                                   
     (contract-out                                             
      [deposit (-> (flat-named-contract                        
                    'amount                                    
                    (λ (x)                                     
                      (and (number? x) (integer? x) (>= x 0))))
                   any)]))                                     
                                                               
    (define total 0)                                           
    (define (deposit a) (set! total (+ a total))))             

With this little change, the error message becomes quite readable:

> (require 'improved-bank-server)    
> (deposit -10)                      
deposit: contract violation          
  expected: amount                   
  given: -10                         
  in: the 1st argument of            
      (-> amount any)                
  contract from: improved-bank-server
  blaming: top-level                 
   (assuming the contract is correct)
  at: eval:5.0                       

2.7. Dissecting a contract error message

In general, each contract error message consists of six sections:

  • a name for the function or method associated with the contract and either the phrase “contract violation” or “broke its contract” depending on whether the contract was violated by the client or the server; e.g. in the previous example:

    deposit: contract violation

  • a description of the precise aspect of the contract that was violated,

    expected: amount given: -10

  • the complete contract plus a path into it showing which aspect was violated,

    in: the 1st argument of -> amount any

  • the module where the contract was put (or, more generally, the boundary that the contract mediates),

    contract from: improved-bank-server

  • who was blamed,

    blaming: top-level
    assuming the contract is correct

  • and the source location where the contract appears.

    at: eval:5.0

3. Contracts on Functions in General

The -> contract constructor works for functions that take a fixed number of arguments and where the result contract is independent of the input arguments. To support other kinds of functions, Racket supplies additional contract constructors, notably ->* and ->i.

3.1. Optional Arguments

Take a look at this excerpt from a string-processing module, inspired by the Scheme cookbook:

#lang racket                                            
                                                        
(provide                                                
 (contract-out                                          
  ; pad the given str left and right with               
  ; the (optional) char so that it is centered          
  [string-pad-center (->* (string? natural-number/c)    
                          (char?)                       
                          string?)]))                   
                                                        
(define (string-pad-center str width [pad #\space])     
  (define field-width (min width (string-length str)))  
  (define rmargin (ceiling (/ (- width field-width) 2)))
  (define lmargin (floor (/ (- width field-width) 2)))  
  (string-append (build-string lmargin (λ (x) pad))     
                 str                                    
                 (build-string rmargin (λ (x) pad))))   

The module exports string-pad-center, a function that creates a string of a given width with the given string in the center. The default fill character is #\space; if the client module wishes to use a different character, it may call string-pad-center with a third argument, a char, overwriting the default.

The function definition uses optional arguments, which is appropriate for this kind of functionality. The interesting point here is the formulation of the contract for the string-pad-center.

The contract combinator ->*, demands several groups of contracts:

  • The first one is a parenthesized group of contracts for all required arguments. In this example, we see two: string? and natural-number/c.

  • The second one is a parenthesized group of contracts for all optional arguments: char?.

  • The last one is a single contract: the result of the function.

Note that if a default value does not satisfy a contract, you wont get a contract error for this interface. If you cant trust yourself to get the initial value right, you need to communicate the initial value across a boundary.

3.2. Rest Arguments

The max operator consumes at least one real number, but it accepts any number of additional arguments. You can write other such functions using a rest argument, such as in max-abs:

See [missing] for an introduction to rest arguments.

(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 ->*: a #:rest keyword specifies a contract on a list of arguments after the required and optional arguments:

(provide                                                  
 (contract-out                                            
  [max-abs (->* (real?) () #:rest (listof real?) real?)]))

As always for ->*, the contracts for the required arguments are enclosed in the first pair of parentheses, which in this case is a single real number. The empty pair of parenthesis indicates that there are no optional arguments not counting the rest arguments. The contract for the rest argument follows #:rest; since all additional arguments must be real numbers, the list of rest arguments must satisfy the contract (listof real?).

3.3. Keyword Arguments

It turns out that the -> contract constructor also contains support for keyword arguments. For example, consider this function, which creates a simple GUI and asks the user a yes-or-no question:

See [missing] for an introduction to keyword arguments.

#lang racket/gui                                             
                                                             
(define (ask-yes-or-no-question question                     
                                #:default answer             
                                #:title title                
                                #:width w                    
                                #:height h)                  
  (define d (new dialog% [label title] [width w] [height h]))
  (define msg (new message% [label question] [parent d]))    
  (define (yes) (set! answer #t) (send d show #f))           
  (define (no) (set! answer #f) (send d show #f))            
  (define yes-b (new button%                                 
                     [label "Yes"] [parent d]                
                     [callback (λ (x y) (yes))]              
                     [style (if answer '(border) '())]))     
  (define no-b (new button%                                  
                    [label "No"] [parent d]                  
                    [callback (λ (x y) (no))]                
                    [style (if answer '() '(border))]))      
  (send d show #t)                                           
  answer)                                                    
                                                             
(provide (contract-out                                       
          [ask-yes-or-no-question                            
           (-> string?                                       
               #:default boolean?                            
               #:title string?                               
               #:width exact-integer?                        
               #:height exact-integer?                       
               boolean?)]))                                  

If you really want to ask a yes-or-no question via a GUI, you should use message-box/custom. For that matter, its usually better to provide buttons with more specific answers than “yes” and “no.”

The contract for ask-yes-or-no-question uses ->, and in the same way that lambda or `define`-based functions allows a keyword to precede a functions formal argument, -> allows a keyword to precede a function contracts argument contract. In this case, the contract says that ask-yes-or-no-question must receive four keyword arguments, one for each of the keywords #:default, #:title, #:width, and #:height. As in a function definition, the order of the keywords in -> relative to each other does not matter for clients of the function; only the relative order of argument contracts without keywords matters.

3.4. Optional Keyword Arguments

Of course, many of the parameters in ask-yes-or-no-question (from the previous question) have reasonable defaults and should be made optional:

(define (ask-yes-or-no-question question                    
                                #:default answer            
                                #:title [title "Yes or No?"]
                                #:width [w 400]             
                                #:height [h 200])           
  ...)                                                      

To specify this functions contract, we need to use ->* again. It supports keywords just as you might expect in both the optional and mandatory argument sections. In this case, we have the mandatory keyword #:default and optional keywords #:title, #:width, and #:height. So, we write the contract like this:

(provide (contract-out                   
          [ask-yes-or-no-question        
           (->* (string?                 
                 #:default boolean?)     
                (#:title string?         
                 #:width exact-integer?  
                 #:height exact-integer?)
                                         
                boolean?)]))             

That is, we put the mandatory keywords in the first section, and we put the optional ones in the second section.

3.5. Contracts for case-lambda

A function defined with case-lambda might impose different constraints on its arguments depending on how many are provided. For example, a report-cost function might convert either a pair of numbers or a string into a new string:

See [missing] for an introduction to case-lambda.

(define report-cost                               
  (case-lambda                                    
    [(lo hi) (format "between $~a and $~a" lo hi)]
    [(desc) (format "~a of dollars" desc)]))      
> (report-cost 5 8)                               
"between $5 and $8"                               
> (report-cost "millions")                        
"millions of dollars"                             

The contract for such a function is formed with the case-> combinator, which combines as many functional contracts as needed:

(provide (contract-out                        
          [report-cost                        
           (case->                            
            (integer? integer? . -> . string?)
            (string? . -> . string?))]))      

As you can see, the contract for report-cost combines two function contracts, which is just as many clauses as the explanation of its functionality required.

3.6. Argument and Result Dependencies

The following is an excerpt from an imaginary numerics module:

(provide                                                 
 (contract-out                                           
  [real-sqrt (->i ([argument (>=/c 1)])                  
                  [result (argument) (<=/c argument)])]))

The word “indy” is meant to suggest that blame may be assigned to the contract itself, because the contract must be considered an independent component. The name was chosen in response to two existing labels—“lax” and “picky”—for different semantics of function contracts in the research literature.

The contract for the exported function real-sqrt uses the ->i rather than ->* function contract. The “i” stands for an indy dependent contract, meaning the contract for the function range depends on the value of the argument. The appearance of argument in the line for results contract means that the result depends on the argument. In this particular case, the argument of 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 the more general ->* contract, but with names added that can be used elsewhere in the contract.

Going back to the bank-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 an account structure type and the following functions:

(provide (contract-out                               
          [balance (-> account? amount/c)]           
          [withdraw (-> account? amount/c account?)] 
          [deposit (-> account? amount/c account?)]))

Besides requiring that a client provide a valid amount for a withdrawal, however, the amount should be less than or equal to the specified accounts 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:

#lang racket                                                        
                                                                    
; section 1: the contract definitions                               
(struct account (balance))                                          
(define amount/c natural-number/c)                                  
                                                                    
; section 2: the exports                                            
(provide                                                            
 (contract-out                                                      
  [create   (amount/c . -> . account?)]                             
  [balance  (account? . -> . amount/c)]                             
  [withdraw (->i ([acc account?]                                    
                  [amt (acc) (and/c amount/c (<=/c (balance acc)))])
                 [result (acc amt)                                  
                         (and/c account?                            
                                (lambda (res)                       
                                  (>= (balance res)                 
                                      (- (balance acc) amt))))])]   
  [deposit  (->i ([acc account?]                                    
                  [amt amount/c])                                   
                 [result (acc amt)                                  
                         (and/c account?                            
                                (lambda (res)                       
                                  (>= (balance res)                 
                                      (+ (balance acc) amt))))])])) 
                                                                    
; 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 create and balance. For withdraw and deposit, however, the contracts check and guarantee the more complicated constraints on balance and deposit. The contract on the second argument to withdraw uses (balance acc) to check whether the supplied withdrawal amount is small enough, where acc is the name given within ->i to the functions first argument. The contract on the result of withdraw uses both acc and amt to guarantee that no more than that requested amount was withdrawn. The contract on deposit similarly uses acc and 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 flat-named-contract within a helper function mk-account-contract to provide better error messages.

#lang racket                                                               
                                                                           
; 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 less than ~a expected")               
                                                                           
(define (mk-account-contract acc amt op msg)                               
  (define balance0 (balance acc))                                          
  (define (ctr a)                                                          
    (and (account? a) (op balance0 (balance a))))                          
  (flat-named-contract (format msg balance0) ctr))                         
                                                                           
; section 2: the exports                                                   
(provide                                                                   
 (contract-out                                                             
  [create   (amount/c . -> . account?)]                                    
  [balance  (account? . -> . amount/c)]                                    
  [withdraw (->i ([acc account?]                                           
                  [amt (acc) (and/c amount/c (<=/c (balance acc)))])       
                 [result (acc amt) (mk-account-contract acc amt >= msg>)])]
  [deposit  (->i ([acc account?]                                           
                  [amt amount/c])                                          
                 [result (acc amt)                                         
                         (mk-account-contract acc amt <= msg<)])]))        
                                                                           
; 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)))                                   

3.7. Checking State Changes

The ->i contract combinator can also ensure that a function only modifies state according to certain constraints. For example, consider this contract (it is a slightly simplified version from the function preferences:add-panel in the framework):

(->i ([parent (is-a?/c area-container-window<%>)])     
      [_ (parent)                                      
       (let ([old-children (send parent get-children)])
         (λ (child)                                    
           (andmap eq?                                 
                   (append old-children (list child))  
                   (send parent get-children))))])     

It says that the function accepts a single argument, named parent, and that parent must be an object matching the interface area-container-window<%>.

The range contract ensures that the function only modifies the children of parent by adding a new child to the front of the list. It accomplishes this by using the _ instead of a normal identifier, which tells the contract library that the range contract does not depend on the values of any of the results, and thus the contract library evaluates the expression following the _ when the function is called, instead of when it returns. Therefore the call to the get-children method happens before the function under the contract is called. When the function under contract returns, its result is passed in as child, and the contract ensures that the children after the function return are the same as the children before the function called, but with one more child, at the front of the list.

To see the difference in a toy example that focuses on this point, consider this program

#lang racket                                           
(define x '())                                         
(define (get-x) x)                                     
(define (f) (set! x (cons 'f x)))                      
(provide                                               
 (contract-out                                         
  [f (->i () [_ (begin (set! x (cons 'ctc x)) any/c)])]
  [get-x (-> (listof symbol?))]))                      

If you were to require this module, call f, then the result of get-x would be '(f ctc). In contrast, if the contract for f were

(->i () [res (begin (set! x (cons 'ctc x)) any/c)])

only changing the underscore to `res`, then the result of get-x would be '(ctc f).

3.8. Multiple Result Values

The function split consumes a list of chars and delivers the string that occurs before the first occurrence of #\newline (if any) and the rest of the list:

(define (split l)                                        
  (define (split l w)                                    
    (cond                                                
      [(null? l) (values (list->string (reverse w)) '())]
      [(char=? #\newline (car l))                        
       (values (list->string (reverse w)) (cdr l))]      
      [else (split (cdr l) (cons (car l) w))]))          
  (split l '()))                                         

It is a typical multiple-value function, returning two values by traversing a single list.

The contract for such a function can use the ordinary function arrow ->, since -> treats values specially when it appears as the last result:

(provide (contract-out                                  
          [split (-> (listof char?)                     
                     (values string? (listof char?)))]))

The contract for such a function can also be written using ->*:

(provide (contract-out                                   
          [split (->* ((listof char?))                   
                      ()                                 
                      (values string? (listof char?)))]))

As before, the contract for the argument with ->* is wrapped in an extra pair of parentheses and must always be wrapped like that and the empty pair of parentheses indicates that there are no optional arguments. The contracts for the results are inside values: a string and a list of characters.

Now, suppose that we also want to ensure that the first result of split is a prefix of the given word in list format. In that case, we need to use the ->i contract combinator:

(define (substring-of? s)                                       
  (flat-named-contract                                          
    (format "substring of ~s" s)                                
    (lambda (s2)                                                
      (and (string? s2)                                         
           (<= (string-length s2) (string-length s))            
           (equal? (substring s 0 (string-length s2)) s2)))))   
                                                                
(provide                                                        
 (contract-out                                                  
  [split (->i ([fl (listof char?)])                             
              (values [s (fl) (substring-of? (list->string fl))]
                      [c (listof char?)]))]))                   

Like ->*, the ->i combinator uses a function over the argument to create the range contracts. Yes, it doesnt just return one contract but as many as the function produces values: one contract per value. In this case, the second contract is the same as before, ensuring that the second result is a list of chars. In contrast, the first contract strengthens the old one so that the result is a prefix of the given word.

This contract is expensive to check, of course. Here is a slightly cheaper version:

(provide                                                 
 (contract-out                                           
  [split (->i ([fl (listof char?)])                      
              (values [s (fl) (string-len/c (length fl))]
                      [c (listof char?)]))]))            

3.9. Fixed but Statically Unknown Arities

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 latter. Unless the arity of the given function matches the length of the given list, your procedure is in trouble.

Consider this n-step function:

; (number ... -> (union #f number?)) (listof number) -> void
(define (n-step proc inits)                                 
  (let ([inc (apply proc inits)])                           
    (when inc                                               
      (n-step proc (map (λ (x) (+ x inc)) inits)))))        

The argument of n-step is proc, a function proc whose results are either numbers or false, and a list. It then applies proc to the list inits. As long as proc returns a number, n-step treats that number as an increment for each of the numbers in inits and recurs. When proc returns false, the loop stops.

Here are two uses:

; nat -> nat                  
(define (f x)                 
  (printf "~s\n" x)           
  (if (= x 0) #f -1))         
(n-step f '(2))               
                              
; nat nat -> nat              
(define (g x y)               
  (define z (+ x y))          
  (printf "~s\n" (list x y z))
  (if (= z 0) #f -1))         
                              
(n-step g '(1 1))             

A contract for n-step must specify two aspects of procs behavior: its arity must include the number of elements in inits, and it must return either a number or #f. The latter is easy, the former is difficult. At first glance, this appears to suggest a contract that assigns a variable-arity to proc:

(->* ()                     
     #:rest (listof any/c)  
     (or/c number? false/c))

This contract, however, says that the function must accept any number of arguments, not a specific but undetermined number. Thus, applying n-step to (lambda (x) x) and (list 1) breaks the contract because the given function accepts only one argument.

The correct contract uses the unconstrained-domain-> combinator, which specifies only the range of a function, not its domain. It is then possible to combine this contract with an arity test to specify the correct contract for n-step:

(provide                                          
 (contract-out                                    
  [n-step                                         
   (->i ([proc (inits)                            
          (and/c (unconstrained-domain->          
                  (or/c false/c number?))         
                 (λ (f) (procedure-arity-includes?
                         f                        
                         (length inits))))]       
         [inits (listof number?)])                
        ()                                        
        any)]))                                   

4. Contracts: A Thorough Example

This section develops several different flavors of contracts for one and the same example: Rackets argmax function. According to its Racket documentation, the function consumes a procedure proc and a non-empty list of values, lst. It

returns the first element in the list lst that maximizes the result of proc.

The emphasis on first is ours.

Examples:

> (argmax add1 (list 1 2 3))                      
3                                                 
> (argmax sqrt (list 0.4 0.9 0.16))               
0.9                                               
> (argmax second '((a 2) (b 3) (c 4) (d 1) (e 4)))
'(c 4)                                            

Here is the simplest possible contract for this function:

version 1

#lang racket                                                
                                                            
(define (argmax f lov) ...)                                 
                                                            
(provide                                                    
 (contract-out                                              
  [argmax (-> (-> any/c real?) (and/c pair? list?) any/c)]))

This contract captures two essential conditions of the informal description of argmax:

  • the given function must produce numbers that are comparable according to <. In particular, the contract (-> any/c number?) would not do, because number? also recognizes complex numbers in Racket.

  • the given list must contain at least one item.

When combined with the name, the contract explains the behavior of argmax at the same level as an ML function type in a module signature except for the non-empty list aspect.

Contracts may communicate significantly more than a type signature, however. Take a look at this second contract for argmax:

version 2

#lang racket                                                
                                                            
(define (argmax f lov) ...)                                 
                                                            
(provide                                                    
 (contract-out                                              
  [argmax                                                   
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
         (r (f lov)                                         
            (lambda (r)                                     
              (define f@r (f r))                            
              (for/and ([v lov]) (>= f@r (f v))))))]))      

It is a dependent contract that names the two arguments and uses the names to impose a predicate on the result. This predicate computes (f r) where r is the result of argmax and then validates that this value is greater than or equal to all values of f on the items of lov.

Is it possible that argmax could cheat by returning a random value that accidentally maximizes f over all elements of lov? With a contract, it is possible to rule out this possibility:

version 2 rev. a

#lang racket                                                
                                                            
(define (argmax f lov) ...)                                 
                                                            
(provide                                                    
 (contract-out                                              
  [argmax                                                   
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
         (r (f lov)                                         
            (lambda (r)                                     
              (define f@r (f r))                            
              (and (memq r lov)                             
                   (for/and ([v lov]) (>= f@r (f v)))))))]))

The memq function ensures that r is intensionally equal That is, "pointer equality" for those who prefer to think at the hardware level. to one of the members of lov. Of course, a moments worth of reflection shows that it is impossible to make up such a value. Functions are opaque values in Racket and without applying a function, it is impossible to determine whether some random input value produces an output value or triggers some exception. So we ignore this possibility from here on.

Version 2 formulates the overall sentiment of argmaxs documentation, but it fails to bring across that the result is the first element of the given list that maximizes the given function f. Here is a version that communicates this second aspect of the informal documentation:

version 3

#lang racket                                                         
                                                                     
(define (argmax f lov) ...)                                          
                                                                     
(provide                                                             
 (contract-out                                                       
  [argmax                                                            
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()         
         (r (f lov)                                                  
            (lambda (r)                                              
              (define f@r (f r))                                     
              (and (for/and ([v lov]) (>= f@r (f v)))                
                   (eq? (first (memf (lambda (v) (= (f v) f@r)) lov))
                        r)))))]))                                    

That is, the memf function determines the first element of lov whose value under f is equal to rs value under f. If this element is intensionally equal to r, the result of argmax is correct.

This second refinement step introduces two problems. First, both conditions recompute the values of f for all elements of lov. Second, the contract is now quite difficult to read. Contracts should have a concise formulation that a client can comprehend with a simple scan. Let us eliminate the readability problem with two auxiliary functions that have reasonably meaningful names:

version 3 rev. a

#lang racket                                                
                                                            
(define (argmax f lov) ...)                                 
                                                            
(provide                                                    
 (contract-out                                              
  [argmax                                                   
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
         (r (f lov)                                         
            (lambda (r)                                     
              (define f@r (f r))                            
              (and (is-first-max? r f@r f lov)              
                   (dominates-all f@r f lov)))))]))         
                                                            
; where                                                     
                                                            
; f@r is greater or equal to all (f v) for v in lov         
(define (dominates-all f@r f lov)                           
  (for/and ([v lov]) (>= f@r (f v))))                       
                                                            
; r is eq? to the first element v of lov for which (pred? v)
(define (is-first-max? r f@r f lov)                         
  (eq? (first (memf (lambda (v) (= (f v) f@r)) lov)) r))    

The names of the two predicates express their functionality and, in principle, render it unnecessary to read their definitions.

This step leaves us with the problem of the newly introduced inefficiency. To avoid the recomputation of (f v) for all v on lov, we change the contract so that it computes these values and reuses them as needed:

version 3 rev. b

#lang racket                                                        
                                                                    
(define (argmax f lov) ...)                                         
                                                                    
(provide                                                            
 (contract-out                                                      
  [argmax                                                           
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()        
         (r (f lov)                                                 
            (lambda (r)                                             
              (define f@r (f r))                                    
              (define flov (map f lov))                             
              (and (is-first-max? r f@r (map list lov flov))        
                   (dominates-all f@r flov)))))]))                  
                                                                    
; where                                                             
                                                                    
; f@r is greater or equal to all f@v in flov                        
(define (dominates-all f@r flov)                                    
  (for/and ([f@v flov]) (>= f@r f@v)))                              
                                                                    
; r is (first x) for the first x in lov+flov s.t. (= (second x) f@r)
(define (is-first-max? r f@r lov+flov)                              
  (define fst (first lov+flov))                                     
  (if (= (second fst) f@r)                                          
      (eq? (first fst) r)                                           
      (is-first-max? r f@r (rest lov+flov))))                       

Now the predicate on the result once again computes all values of f for elements of lov once.

The word "eager" comes from the literature on the linguistics of contracts.

Version 3 may still be too eager when it comes to calling f. While Rackets argmax always calls f no matter how many items lov contains, let us imagine for illustrative purposes that our own implementation first checks whether the list is a singleton. If so, the first element would be the only element of lov and in that case there would be no need to compute (f r). The argmax of Racket implicitly argues that it not only promises the first value that maximizes f over lov but also that f produces/produced a value for the result. As a matter of fact, since f may diverge or raise an exception for some inputs, argmax should avoid calling f when possible.

The following contract demonstrates how a higher-order dependent contract needs to be adjusted so as to avoid being over-eager:

version 4

#lang racket                                                        
                                                                    
(define (argmax f lov)                                              
  (if (empty? (rest lov))                                           
      (first lov)                                                   
      ...))                                                         
                                                                    
(provide                                                            
 (contract-out                                                      
  [argmax                                                           
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()        
         (r (f lov)                                                 
            (lambda (r)                                             
              (cond                                                 
                [(empty? (rest lov)) (eq? (first lov) r)]           
                [else                                               
                 (define f@r (f r))                                 
                 (define flov (map f lov))                          
                 (and (is-first-max? r f@r (map list lov flov))     
                      (dominates-all f@r flov))]))))]))             
                                                                    
; where                                                             
                                                                    
; f@r is greater or equal to all f@v in flov                        
(define (dominates-all f@r lov) ...)                                
                                                                    
; r is (first x) for the first x in lov+flov s.t. (= (second x) f@r)
(define (is-first-max? r f@r lov+flov) ...)                         

Note that such considerations dont apply to the world of first-order contracts. Only a higher-order or lazy language forces the programmer to express contracts with such precision.

The problem of diverging or exception-raising functions should alert the reader to the even more general problem of functions with side-effects. If the given function f has visible effects say it logs its calls to a file then the clients of argmax will be able to observe two sets of logs for each call to argmax. To be precise, if the list of values contains more than one element, the log will contain two calls of f per value on lov. If f is expensive to compute, doubling the calls imposes a high cost.

To avoid this cost and to signal problems with overly eager contracts, a contract system could record the i/o of contracted function arguments and use these hashtables in the dependency specification. This is a topic of on-going research in PLT. Stay tuned.

5. Contracts on Structures

Modules deal with structures in two ways. First they export struct definitions, i.e., the ability to create structs of a certain kind, to access their fields, to modify them, and to distinguish structs of this kind against every other kind of value in the world. Second, on occasion a module exports a specific struct and wishes to promise that its fields contain values of a certain kind. This section explains how to protect structs with contracts for both uses.

5.1. Guarantees for a Specific Value

If your module defines a variable to be a structure, then you can specify the structures shape using struct/c:

#lang racket                                    
(require lang/posn)                             
                                                
(define origin (make-posn 0 0))                 
                                                
(provide (contract-out                          
          [origin (struct/c posn zero? zero?)]))

In this example, the module imports a library for representing positions, which exports a posn structure. One of the posns it creates and exports stands for the origin, i.e., (0,0), of the grid.

See also vector/c and similar contract combinators for flat compound data.

5.2. Guarantees for All Values

The book How to Design Programs teaches that posns should contain only numbers in their two fields. With contracts we would enforce this informal data definition as follows:

#lang racket                                     
(struct posn (x y))                              
                                                 
(provide (contract-out                           
          [struct posn ((x number?) (y number?))]
          [p-okay posn?]                         
          [p-sick posn?]))                       
                                                 
(define p-okay (posn 10 20))                     
(define p-sick (posn 'a 'b))                     

This module exports the entire structure definition: posn, posn?, posn-x, posn-y, set-posn-x!, and set-posn-y!. Each function enforces or promises that the two fields of a posn structure are numbers — when the values flow across the module boundary. Thus, if a client calls posn on 10 and 'a, the contract system signals a contract violation.

The creation of p-sick inside of the posn module, however, does not violate the contracts. The function posn is used internally, so 'a and 'b dont cross the module boundary. Similarly, when p-sick crosses the boundary of posn, the contract promises a posn? and nothing else. In particular, this check does not require that the fields of p-sick are numbers.

The association of contract checking with module boundaries implies that p-okay and p-sick look alike from a clients perspective until the client extracts the pieces:

#lang racket           
(require lang/posn)    
                       
... (posn-x p-sick) ...

Using posn-x is the only way the client can find out what a posn contains in the x field. The application of posn-x sends p-sick back into the posn module and the result value 'a here back to the client, again across the module boundary. At this very point, the contract system discovers that a promise is broken. Specifically, posn-x doesnt return a number but a symbol and is therefore blamed.

This specific example shows that the explanation for a contract violation doesnt always pinpoint the source of the error. The good news is that the error is located in the posn module. The bad news is that the explanation is misleading. Although it is true that posn-x produced a symbol instead of a number, it is the fault of the programmer who created a posn from symbols, i.e., the programmer who added

(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.

If we want to fix the contract for p-sick so that the error is caught when sick is exported, a single change suffices:

(provide                                    
 (contract-out                              
  ...                                       
  [p-sick (struct/c posn number? number?)]))

That is, instead of exporting p-sick as a plain posn?, we use a struct/c contract to enforce constraints on its components.

5.3. Checking Properties of Data Structures

Contracts written using struct/c immediately check the fields of the data structure, but sometimes this can have disastrous effects on the performance of a program that does not, itself, inspect the entire data structure.

As an example, consider the binary search tree search algorithm. A binary search tree is like a binary tree, except that the numbers are organized in the tree to make searching the tree fast. In particular, for each interior node in the tree, all of the numbers in the left subtree are smaller than the number in the node, and all of the numbers in the right subtree are larger than the number in the node.

We can implement a search function in? that takes advantage of the structure of the binary search tree.

#lang racket                                                 
                                                             
(struct node (val left right))                               
                                                             
; determines if `n' is in the binary search tree `b',        
; exploiting the binary search tree invariant                
(define (in? n b)                                            
  (cond                                                      
    [(null? b) #f]                                           
    [else (cond                                              
            [(= n (node-val b))                              
             #t]                                             
            [(< n (node-val b))                              
             (in? n (node-left b))]                          
            [(> n (node-val b))                              
             (in? n (node-right b))])]))                     
                                                             
; a predicate that identifies binary search trees            
(define (bst-between? b low high)                            
  (or (null? b)                                              
      (and (<= low (node-val b) high)                        
           (bst-between? (node-left b) low (node-val b))     
           (bst-between? (node-right b) (node-val b) high))))
                                                             
(define (bst? b) (bst-between? b -inf.0 +inf.0))             
                                                             
(provide (struct-out node))                                  
(provide (contract-out                                       
          [bst? (any/c . -> . boolean?)]                     
          [in? (number? bst? . -> . boolean?)]))             

In a full binary search tree, this means that the in? function only has to explore a logarithmic number of nodes.

The contract on in? guarantees that its input is a binary search tree. But a little careful thought reveals that this contract defeats the purpose of the binary search tree algorithm. In particular, consider the inner cond in the in? function. This is where the in? function gets its speed: it avoids searching an entire subtree at each recursive call. Now compare that to the bst-between? function. In the case that it returns #t, it traverses the entire tree, meaning that the speedup of in? is lost.

In order to fix that, we can employ a new strategy for checking the binary search tree contract. In particular, if we only checked the contract on the nodes that in? looks at, we can still guarantee that the tree is at least partially well-formed, but without changing the complexity.

To do that, we need to use struct/dc to define bst-between?. Like struct/c, struct/dc defines a contract for a structure. Unlike struct/c, it allows fields to be marked as lazy, so that the contracts are only checked when the matching selector is called. Also, it does not allow mutable fields to be marked as lazy.

The struct/dc form accepts a contract for each field of the struct and returns a contract on the struct. More interestingly, struct/dc allows us to write dependent contracts, i.e., contracts where some of the contracts on the fields depend on the values of other fields. We can use this to define the binary search tree contract:

#lang racket                                                            
                                                                        
(struct node (val left right))                                          
                                                                        
; determines if `n' is in the binary search tree `b'                    
(define (in? n b) ... as before ...)                                    
                                                                        
; bst-between : number number -> contract                               
; builds a contract for binary search trees                             
; whose values are between low and high                                 
(define (bst-between/c low high)                                        
  (or/c null?                                                           
        (struct/dc node [val (between/c low high)]                      
                        [left (val) #:lazy (bst-between/c low val)]     
                        [right (val) #:lazy (bst-between/c val high)])))
                                                                        
(define bst/c (bst-between/c -inf.0 +inf.0))                            
                                                                        
(provide (struct-out node))                                             
(provide (contract-out                                                  
          [bst/c contract?]                                             
          [in? (number? bst/c . -> . boolean?)]))                       

In general, each use of struct/dc must name the fields and then specify contracts for each field. In the above, the val field is a contract that accepts values between low and high. The left and right fields are dependent on the value of the val field, indicated by their second sub-expressions. They are also marked with the #:lazy keyword to indicate that they should be checked only when the appropriate accessor is called on the struct instance. Their contracts are built by recursive calls to the bst-between/c function. Taken together, this contract ensures the same thing that the bst-between? function checked in the original example, but here the checking only happens as in? explores the tree.

Although this contract improves the performance of in?, restoring it to the logarithmic behavior that the contract-less version had, it is still imposes a fairly large constant overhead. So, the contract library also provides define-opt/c that brings down that constant factor by optimizing its body. Its shape is just like the define above. It expects its body to be a contract and then optimizes that contract.

(define-opt/c (bst-between/c low high)                                  
  (or/c null?                                                           
        (struct/dc node [val (between/c low high)]                      
                        [left (val) #:lazy (bst-between/c low val)]     
                        [right (val) #:lazy (bst-between/c val high)])))

6. Abstract Contracts using #:exists and #:∃

The contract system provides existential contracts that can protect abstractions, ensuring that clients of your module cannot depend on the precise representation choices you make for your data structures.

You can type #:exists instead of #:∃ if you cannot easily type unicode characters; in DrRacket, typing \exists followed by either alt-\ or control-\ depending on your platform will produce .

The contract-out form allows you to write

#:∃ name-of-a-new-contract

as one of its clauses. This declaration introduces the variable name-of-a-new-contract, binding it to a new contract that hides information about the values it protects.

As an example, consider this simple implementation of a queue datastructure:

#lang racket                                             
(define empty '())                                       
(define (enq top queue) (append queue (list top)))       
(define (next queue) (car queue))                        
(define (deq queue) (cdr queue))                         
(define (empty? queue) (null? queue))                    
                                                         
(provide                                                 
 (contract-out                                           
  [empty (listof integer?)]                              
  [enq (-> integer? (listof integer?) (listof integer?))]
  [next (-> (listof integer?) integer?)]                 
  [deq (-> (listof integer?) (listof integer?))]         
  [empty? (-> (listof integer?) boolean?)]))             

This code implements a queue purely in terms of lists, meaning that clients of this data structure might use car and cdr directly on the data structure perhaps accidentally and thus any change in the representation (say to a more efficient representation that supports amortized constant time enqueue and dequeue operations) might break client code.

To ensure that the queue representation is abstract, we can use #:∃ in the contract-out expression, like this:

(provide                         
 (contract-out                   
  #:∃ queue                      
  [empty queue]                  
  [enq (-> integer? queue queue)]
  [next (-> queue integer?)]     
  [deq (-> queue queue)]         
  [empty? (-> queue boolean?)])) 

Now, if clients of the data structure try to use car and cdr, they receive an error, rather than mucking about with the internals of the queues.

See also Exists Contracts and Predicates.

7. Additional Examples

This section illustrates the current state of Rackets contract implementation with a series of examples from Design by Contract, by Example [Mitchell02].

Mitchell and McKims principles for design by contract DbC are derived from the 1970s style algebraic specifications. The overall goal of DbC is to specify the constructors of an algebra in terms of its observers. While we reformulate Mitchell and McKims terminology and we use a mostly applicative approach, we retain their terminology of “classes” and “objects”:

  • Separate queries from commands.

    A query returns a result but does not change the observable properties of an object. A command changes the visible properties of an object, but does not return a result. In applicative implementation a command typically returns an new object of the same class.

  • Separate basic queries from derived queries.

    A derived query returns a result that is computable in terms of basic queries.

  • For each derived query, write a post-condition contract that specifies the result in terms of the basic queries.

  • For each command, write a post-condition contract that specifies the changes to the observable properties in terms of the basic queries.

  • For each query and command, decide on a suitable pre-condition contract.

Each of the following sections corresponds to a chapter in Mitchell and McKims book but not all chapters show up here. We recommend that you read the contracts first near the end of the first modules, then the implementation in the first modules, and then the test module at the end of each section.

Mitchell and McKim use Eiffel as the underlying programming language and employ a conventional imperative programming style. Our long-term goal is to transliterate their examples into applicative Racket, structure-oriented imperative Racket, and Rackets class system.

Note: To mimic Mitchell and McKims informal notion of parametericity parametric polymorphism, we use first-class contracts. At several places, this use of first-class contracts improves on Mitchell and McKims design see comments in interfaces.

7.1. A Customer-Manager Component

This first module contains some struct definitions in a separate module in order to better track bugs.

#lang racket                                              
; data definitions                                        
                                                          
(define id? symbol?)                                      
(define id-equal? eq?)                                    
(define-struct basic-customer (id name address) #:mutable)
                                                          
; interface                                               
(provide                                                  
 (contract-out                                            
  [id?                   (-> any/c boolean?)]             
  [id-equal?             (-> id? id? boolean?)]           
  [struct basic-customer ((id id?)                        
                          (name string?)                  
                          (address string?))]))           
; end of interface                                        

This module contains the program that uses the above.

#lang racket                                                
                                                            
(require "1.rkt") ; the module just above                   
                                                            
; implementation                                            
; [listof (list basic-customer? secret-info)]               
(define all '())                                            
                                                            
(define (find c)                                            
  (define (has-c-as-key p)                                  
    (id-equal? (basic-customer-id (car p)) c))              
  (define x (filter has-c-as-key all))                      
  (if (pair? x) (car x) x))                                 
                                                            
(define (active? c)                                         
  (pair? (find c)))                                         
                                                            
(define not-active? (compose not active? basic-customer-id))
                                                            
(define count 0)                                            
(define (get-count) count)                                  
                                                            
(define (add c)                                             
  (set! all (cons (list c 'secret) all))                    
  (set! count (+ count 1)))                                 
                                                            
(define (name id)                                           
  (define bc-with-id (find id))                             
  (basic-customer-name (car bc-with-id)))                   
                                                            
(define (set-name id name)                                  
  (define bc-with-id (find id))                             
  (set-basic-customer-name! (car bc-with-id) name))         
                                                            
(define c0 0)                                               
; end of implementation                                     
                                                            
(provide                                                    
 (contract-out                                              
  ; how many customers are in the db?                       
  [get-count (-> natural-number/c)]                         
  ; is the customer with this id active?                    
  [active?   (-> id? boolean?)]                             
  ; what is the name of the customer with this id?          
  [name      (-> (and/c id? active?) string?)]              
  ; change the name of the customer with this id            
  [set-name  (->i ([id id?] [nn string?])                   
                  [result any/c] ; result contract          
                  #:post (id nn) (string=? (name id) nn))]  
                                                            
  [add       (->i ([bc (and/c basic-customer? not-active?)])
                  ; A pre-post condition contract must use  
                  ; a side-effect to express this contract  
                  ; via post-conditions                     
                  #:pre () (set! c0 count)                  
                  [result any/c] ; result contract          
                  #:post () (> count c0))]))                

The tests:

#lang racket                                                  
(require rackunit rackunit/text-ui "1.rkt" "1b.rkt")          
                                                              
(add (make-basic-customer 'mf "matthias" "brookstone"))       
(add (make-basic-customer 'rf "robby" "beverly hills park"))  
(add (make-basic-customer 'fl "matthew" "pepper clouds town"))
(add (make-basic-customer 'sk "shriram" "i city"))            
                                                              
(run-tests                                                    
 (test-suite                                                  
  "manager"                                                   
  (test-equal? "id lookup" "matthias" (name 'mf))             
  (test-equal? "count" 4 (get-count))                         
  (test-true "active?" (active? 'mf))                         
  (test-false "active? 2" (active? 'kk))                      
  (test-true "set name" (void? (set-name 'mf "matt")))))      

7.2. A Parameteric Simple Stack

#lang racket                                                      
                                                                  
; a contract utility                                              
(define (eq/c x) (lambda (y) (eq? x y)))                          
                                                                  
(define-struct stack (list p? eq))                                
                                                                  
(define (initialize p? eq) (make-stack '() p? eq))                
(define (push s x)                                                
  (make-stack (cons x (stack-list s)) (stack-p? s) (stack-eq s))) 
(define (item-at s i) (list-ref (reverse (stack-list s)) (- i 1)))
(define (count s) (length  (stack-list s)))                       
(define (is-empty? s) (null? (stack-list s)))                     
(define not-empty? (compose not is-empty?))                       
(define (pop s) (make-stack (cdr (stack-list s))                  
                            (stack-p? s)                          
                            (stack-eq s)))                        
(define (top s) (car (stack-list s)))                             
                                                                  
(provide                                                          
 (contract-out                                                    
  ; predicate                                                     
  [stack?     (-> any/c boolean?)]                                
                                                                  
  ; primitive queries                                             
  ; how many items are on the stack?                              
  [count      (-> stack? natural-number/c)]                       
                                                                  
  ; which item is at the given position?                          
  [item-at                                                        
   (->d ([s stack?] [i (and/c positive? (<=/c (count s)))])       
        ()                                                        
        [result (stack-p? s)])]                                   
                                                                  
  ; derived queries                                               
  ; is the stack empty?                                           
  [is-empty?                                                      
   (->d ([s stack?])                                              
        ()                                                        
        [result (eq/c (= (count s) 0))])]                         
                                                                  
  ; which item is at the top of the stack                         
  [top                                                            
   (->d ([s (and/c stack? not-empty?)])                           
        ()                                                        
        [t (stack-p? s)] ; a stack item, t is its name            
        #:post-cond                                               
        ([stack-eq s] t (item-at s (count s))))]                  
                                                                  
  ; creation                                                      
  [initialize                                                     
   (->d ([p contract?] [s (p p . -> . boolean?)])                 
        ()                                                        
        ; Mitchell and McKim use (= (count s) 0) here to express  
        ; the post-condition in terms of a primitive query        
        [result (and/c stack? is-empty?)])]                       
                                                                  
  ; commands                                                      
  ; add an item to the top of the stack                           
  [push                                                           
   (->d ([s stack?] [x (stack-p? s)])                             
        ()                                                        
        [sn stack?] ; result kind                                 
        #:post-cond                                               
        (and (= (+ (count s) 1) (count sn))                       
             ([stack-eq s] x (top sn))))]                         
                                                                  
  ; remove the item at the top of the stack                       
  [pop                                                            
   (->d ([s (and/c stack? not-empty?)])                           
        ()                                                        
        [sn stack?] ; result kind                                 
        #:post-cond                                               
        (= (- (count s) 1) (count sn)))]))                        

The tests:

#lang racket                                           
(require rackunit rackunit/text-ui "2.rkt")            
                                                       
(define s0 (initialize (flat-contract integer?) =))    
(define s2 (push (push s0 2) 1))                       
                                                       
(run-tests                                             
 (test-suite                                           
  "stack"                                              
  (test-true                                           
   "empty"                                             
   (is-empty? (initialize (flat-contract integer?) =)))
  (test-true "push" (stack? s2))                       
  (test-true                                           
   "push exn"                                          
   (with-handlers ([exn:fail:contract? (lambda _ #t)]) 
     (push (initialize (flat-contract integer?)) 'a)   
     #f))                                              
  (test-true "pop" (stack? (pop s2)))                  
  (test-equal? "top" (top s2) 1)                       
  (test-equal? "toppop" (top (pop s2)) 2)))            

7.3. A Dictionary

#lang racket                                                            
                                                                        
; a shorthand for use below                                             
(define-syntax                                                         
  (syntax-rules ()                                                      
    [( antecedent consequent) (if antecedent consequent #t)]))         
                                                                        
; implementation                                                        
(define-struct dictionary (l value? eq?))                               
; the keys should probably be another parameter (exercise)              
                                                                        
(define (initialize p eq) (make-dictionary '() p eq))                   
(define (put d k v)                                                     
  (make-dictionary (cons (cons k v) (dictionary-l d))                   
                   (dictionary-value? d)                                
                   (dictionary-eq? d)))                                 
(define (rem d k)                                                       
  (make-dictionary                                                      
   (let loop ([l (dictionary-l d)])                                     
     (cond                                                              
       [(null? l) l]                                                    
       [(eq? (caar l) k) (loop (cdr l))]                                
       [else (cons (car l) (loop (cdr l)))]))                           
   (dictionary-value? d)                                                
   (dictionary-eq? d)))                                                 
(define (count d) (length (dictionary-l d)))                            
(define (value-for d k) (cdr (assq k (dictionary-l d))))                
(define (has? d k) (pair? (assq k (dictionary-l d))))                   
(define (not-has? d) (lambda (k) (not (has? d k))))                     
; end of implementation                                                 
                                                                        
; interface                                                             
(provide                                                                
 (contract-out                                                          
  ; predicates                                                          
  [dictionary? (-> any/c boolean?)]                                     
  ; basic queries                                                       
  ; how many items are in the dictionary?                               
  [count       (-> dictionary? natural-number/c)]                       
  ; does the dictionary define key k?                                   
  [has?        (->d ([d dictionary?] [k symbol?])                       
                    ()                                                  
                    [result boolean?]                                   
                    #:post-cond                                         
                    ((zero? (count d)) .  . (not result)))]            
  ; what is the value of key k in this dictionary?                      
  [value-for   (->d ([d dictionary?]                                    
                     [k (and/c symbol? (lambda (k) (has? d k)))])       
                    ()                                                  
                    [result (dictionary-value? d)])]                    
  ; initialization                                                      
  ; post condition: for all k in symbol, (has? d k) is false.           
  [initialize  (->d ([p contract?] [eq (p p . -> . boolean?)])          
                    ()                                                  
                    [result (and/c dictionary? (compose zero? count))])]
  ; commands                                                            
  ; Mitchell and McKim say that put shouldn't consume Void (null ptr)   
  ; for v. We allow the client to specify a contract for all values     
  ; via initialize. We could do the same via a key? parameter           
  ; (exercise). add key k with value v to this dictionary               
  [put         (->d ([d dictionary?]                                    
                     [k (and/c symbol? (not-has? d))]                   
                     [v (dictionary-value? d)])                         
                    ()                                                  
                    [result dictionary?]                                
                    #:post-cond                                         
                    (and (has? result k)                                
                         (= (count d) (- (count result) 1))             
                         ([dictionary-eq? d] (value-for result k) v)))] 
  ; remove key k from this dictionary                                   
  [rem         (->d ([d dictionary?]                                    
                     [k (and/c symbol? (lambda (k) (has? d k)))])       
                    ()                                                  
                    [result (and/c dictionary? not-has?)]               
                    #:post-cond                                         
                    (= (count d) (+ (count result) 1)))]))              
; end of interface                                                      

The tests:

#lang racket                                                             
(require rackunit rackunit/text-ui "3.rkt")                              
                                                                         
(define d0 (initialize (flat-contract integer?) =))                      
(define d (put (put (put d0 'a 2) 'b 2) 'c 1))                           
                                                                         
(run-tests                                                               
 (test-suite                                                             
  "dictionaries"                                                         
  (test-equal? "value for" 2 (value-for d 'b))                           
  (test-false "has?" (has? (rem d 'b) 'b))                               
  (test-equal? "count" 3 (count d))                                      
  (test-case "contract check for put: symbol?"                           
             (define d0 (initialize (flat-contract integer?) =))         
             (check-exn exn:fail:contract? (lambda () (put d0 "a" 2))))))

7.4. A Queue

#lang racket                                                              
                                                                          
; Note: this queue doesn't implement the capacity restriction             
; of Mitchell and McKim's queue but this is easy to add.                  
                                                                          
; a contract utility                                                      
(define (all-but-last l) (reverse (cdr (reverse l))))                     
(define (eq/c x) (lambda (y) (eq? x y)))                                  
                                                                          
; implementation                                                          
(define-struct queue (list p? eq))                                        
                                                                          
(define (initialize p? eq) (make-queue '() p? eq))                        
(define items queue-list)                                                 
(define (put q x)                                                         
  (make-queue (append (queue-list q) (list x))                            
              (queue-p? q)                                                
              (queue-eq q)))                                              
(define (count s) (length  (queue-list s)))                               
(define (is-empty? s) (null? (queue-list s)))                             
(define not-empty? (compose not is-empty?))                               
(define (rem s)                                                           
  (make-queue (cdr (queue-list s))                                        
              (queue-p? s)                                                
              (queue-eq s)))                                              
(define (head s) (car (queue-list s)))                                    
                                                                          
; interface                                                               
(provide                                                                  
 (contract-out                                                            
  ; predicate                                                             
  [queue?     (-> any/c boolean?)]                                        
                                                                          
  ; primitive queries                                                     
  ; Imagine providing this 'query' for the interface of the module        
  ; only. Then in Racket there is no reason to have count or is-empty?    
  ; around (other than providing it to clients). After all items is       
  ; exactly as cheap as count.                                            
  [items      (->d ([q queue?]) () [result (listof (queue-p? q))])]       
                                                                          
  ; derived queries                                                       
  [count      (->d ([q queue?])                                           
                   ; We could express this second part of the post        
                   ; condition even if count were a module "attribute"    
                   ; in the language of Eiffel; indeed it would use the   
                   ; exact same syntax (minus the arrow and domain).      
                   ()                                                     
                   [result (and/c natural-number/c                        
                                  (=/c (length (items q))))])]            
                                                                          
  [is-empty?  (->d ([q queue?])                                           
                   ()                                                     
                   [result (and/c boolean?                                
                                  (eq/c (null? (items q))))])]            
                                                                          
  [head       (->d ([q (and/c queue? (compose not is-empty?))])           
                   ()                                                     
                   [result (and/c (queue-p? q)                            
                                  (eq/c (car (items q))))])]              
  ; creation                                                              
  [initialize (-> contract?                                               
                  (contract? contract? . -> . boolean?)                   
                  (and/c queue? (compose null? items)))]                  
                                                                          
  ; commands                                                              
  [put        (->d ([oldq queue?] [i (queue-p? oldq)])                    
                   ()                                                     
                   [result                                                
                    (and/c                                                
                     queue?                                               
                     (lambda (q)                                          
                       (define old-items (items oldq))                    
                       (equal? (items q) (append old-items (list i)))))])]
                                                                          
  [rem        (->d ([oldq (and/c queue? (compose not is-empty?))])        
                   ()                                                     
                   [result                                                
                    (and/c queue?                                         
                           (lambda (q)                                    
                             (equal? (cdr (items oldq)) (items q))))])])) 
; end of interface                                                        

The tests:

#lang racket                                                      
(require rackunit rackunit/text-ui "5.rkt")                       
                                                                  
(define s (put (put (initialize (flat-contract integer?) =) 2) 1))
                                                                  
(run-tests                                                        
 (test-suite                                                      
  "queue"                                                         
  (test-true                                                      
   "empty"                                                        
   (is-empty? (initialize (flat-contract integer?) =)))           
  (test-true "put" (queue? s))                                    
  (test-equal? "count" 2 (count s))                               
  (test-true "put exn"                                            
             (with-handlers ([exn:fail:contract? (lambda _ #t)])  
               (put (initialize (flat-contract integer?)) 'a)     
               #f))                                               
  (test-true "remove" (queue? (rem s)))                           
  (test-equal? "head" 2 (head s))))                               

8. Building New Contracts

Contracts are represented internally as functions that accept information about the contract (who is to blame, source locations, etc.) and produce projections in the spirit of Dana Scott that enforce the contract.

In a general sense, a projection is a function that accepts an arbitrary value, and returns a value that satisfies the corresponding contract. For example, a projection that accepts only integers corresponds to the contract (flat-contract integer?), and can be written like this:

(define int-proj                      
  (λ (x)                              
    (if (integer? x)                  
        x                             
        (signal-contract-violation))))

As a second example, a projection that accepts unary functions on integers looks like this:

(define int->int-proj                        
  (λ (f)                                     
    (if (and (procedure? f)                  
             (procedure-arity-includes? f 1))
        (λ (x) (int-proj (f (int-proj x))))  
        (signal-contract-violation))))       

Although these projections have the right error behavior, they are not quite ready for use as contracts, because they do not accommodate blame and do not provide good error messages. In order to accommodate these, contracts do not just use simple projections, but use functions that accept a blame object encapsulating the names of two parties that are the candidates for blame, as well as a record of the source location where the contract was established and the name of the contract. They can then, in turn, pass that information to raise-blame-error to signal a good error message.

Here is the first of those two projections, rewritten for use in the contract system:

(define (int-proj blame)                     
  (λ (x)                                     
    (if (integer? x)                         
        x                                    
        (raise-blame-error                   
         blame                               
         x                                   
         '(expected: "<integer>" given: "~e")
         x))))                               

The new argument specifies who is to be blamed for positive and negative contract violations.

Contracts, in this system, are always established between two parties. One party, called the server, provides some value according to the contract, and the other, the client, consumes the value, also according to the contract. The server is called the positive position and the client the negative position. So, in the case of just the integer contract, the only thing that can go wrong is that the value provided is not an integer. Thus, only the positive party the server can ever accrue blame. The raise-blame-error function always blames the positive party.

Compare that to the projection for our function contract:

(define (int->int-proj blame)                                 
  (define dom (int-proj (blame-swap blame)))                  
  (define rng (int-proj blame))                               
  (λ (f)                                                      
    (if (and (procedure? f)                                   
             (procedure-arity-includes? f 1))                 
        (λ (x) (rng (f (dom x))))                             
        (raise-blame-error                                    
         blame                                                
         f                                                    
         '(expected "a procedure of one argument" given: "~e")
         f))))                                                

In this case, the only explicit blame covers the situation where either a non-procedure is supplied to the contract or the procedure does not accept one argument. As with the integer projection, the blame here also lies with the producer of the value, which is why raise-blame-error is passed blame unchanged.

The checking for the domain and range are delegated to the int-proj function, which is supplied its arguments in the first two lines of the int->int-proj function. The trick here is that, even though the int->int-proj function always blames what it sees as positive, we can swap the blame parties by calling blame-swap on the given blame object, replacing the positive party with the negative party and vice versa.

This technique is not merely a cheap trick to get the example to work, however. The reversal of the positive and the negative is a natural consequence of the way functions behave. That is, imagine the flow of values in a program between two modules. First, one module (the server) defines a function, and then that module is required by another the client. So far, the function itself has to go from the original, providing module to the requiring module. Now, imagine that the requiring module invokes the function, supplying it an argument. At this point, the flow of values reverses. The argument is traveling back from the requiring module to the providing module! The client is “serving” the argument to the server, and the server is receiving that value as a client. And finally, when the function produces a result, that result flows back in the original direction from server to client. Accordingly, the contract on the domain reverses the positive and the negative blame parties, just like the flow of values reverses.

We can use this insight to generalize the function contracts and build a function that accepts any two contracts and returns a contract for functions between them.

This projection also goes further and uses blame-add-context to improve the error messages when a contract violation is detected.

(define (make-simple-function-contract dom-proj range-proj)     
  (λ (blame)                                                    
    (define dom (dom-proj (blame-add-context blame              
                                             "the argument of"  
                                             #:swap? #t)))      
    (define rng (range-proj (blame-add-context blame            
                                               "the range of")))
    (λ (f)                                                      
      (if (and (procedure? f)                                   
               (procedure-arity-includes? f 1))                 
          (λ (x) (rng (f (dom x))))                             
          (raise-blame-error                                    
           blame                                                
           f                                                    
           '(expected "a procedure of one argument" given: "~e")
           f)))))                                               

While these projections are supported by the contract library and can be used to build new contracts, the contract library also supports a different API for projections that can be more efficient. Specifically, a late neg projection accepts a blame object without the negative blame information and then returns a function that accepts both the value to be contracted and the name of the negative party, in that order. The returned function then in turn returns the value with the contract. Rewriting int->int-proj to use this API looks like this:

(define (int->int-proj blame)                                 
  (define dom-blame (blame-add-context blame                  
                                       "the argument of"      
                                       #:swap? #t))           
  (define rng-blame (blame-add-context blame "the range of")) 
  (define (check-int v to-blame neg-party)                    
    (unless (integer? v)                                      
      (raise-blame-error                                      
       to-blame #:missing-party neg-party                     
       v                                                      
       '(expected "an integer" given: "~e")                   
       v)))                                                   
  (λ (f neg-party)                                            
    (if (and (procedure? f)                                   
             (procedure-arity-includes? f 1))                 
        (λ (x)                                                
          (check-int x dom-blame neg-party)                   
          (define ans (f x))                                  
          (check-int ans rng-blame neg-party)                 
          ans)                                                
        (raise-blame-error                                    
         blame #:missing-party neg-party                      
         f                                                    
         '(expected "a procedure of one argument" given: "~e")
         f))))                                                

The advantage of this style of contract is that the blame argument can be supplied on the server side of the contract boundary and the result can be used for each different client. With the simpler situation, a new blame object has to be created for each client.

One final problem remains before this contract can be used with the rest of the contract system. In the function above, the contract is implemented by creating a wrapper function for f, but this wrapper function does not cooperate with equal?, nor does it let the runtime system know that there is a relationship between the result function and f, the input function.

To remedy these two problems, we should use chaperones instead of just using λ to create the wrapper function. Here is the int->int-proj function rewritten to use a chaperone:

(define (int->int-proj blame)                                 
  (define dom-blame (blame-add-context blame                  
                                       "the argument of"      
                                       #:swap? #t))           
  (define rng-blame (blame-add-context blame "the range of")) 
  (define (check-int v to-blame neg-party)                    
    (unless (integer? v)                                      
      (raise-blame-error                                      
       to-blame #:missing-party neg-party                     
       v                                                      
       '(expected "an integer" given: "~e")                   
       v)))                                                   
  (λ (f neg-party)                                            
    (if (and (procedure? f)                                   
             (procedure-arity-includes? f 1))                 
        (chaperone-procedure                                  
         f                                                    
         (λ (x)                                               
           (check-int x dom-blame neg-party)                  
           (values (λ (ans)                                   
                     (check-int ans rng-blame neg-party)      
                     ans)                                     
                   x)))                                       
        (raise-blame-error                                    
         blame #:missing-party neg-party                      
         f                                                    
         '(expected "a procedure of one argument" given: "~e")
         f))))                                                

Projections like the ones described above, but suited to other, new kinds of value you might make, can be used with the contract library primitives. Specifically, we can use make-chaperone-contract to build it:

(define int->int-contract               
  (make-contract                        
   #:name 'int->int                     
   #:late-neg-projection int->int-proj))

and then combine it with a value and get some contract checking.

(define/contract (f x)               
  int->int-contract                  
  "not an int")                      
> (f #f)                             
f: contract violation;               
 expected an integer                 
  given: #f                          
  in: the argument of                
      int->int                       
  contract from: (function f)        
  blaming: top-level                 
   (assuming the contract is correct)
  at: eval:5.0                       
> (f 1)                              
f: broke its own contract;           
 promised an integer                 
  produced: "not an int"             
  in: the range of                   
      int->int                       
  contract from: (function f)        
  blaming: (function f)              
   (assuming the contract is correct)
  at: eval:5.0                       

8.1. Contract Struct Properties

The make-chaperone-contract function is okay for one-off contracts, but often you want to make many different contracts that differ only in some pieces. The best way to do that is to use a struct with either prop:contract, prop:chaperone-contract, or prop:flat-contract.

For example, lets say we wanted to make a simple form of the -> contract that accepts one contract for the range and one for the domain. We should define a struct with two fields and use build-chaperone-contract-property to construct the chaperone contract property we need.

(struct simple-arrow (dom rng)                 
  #:property prop:chaperone-contract           
  (build-chaperone-contract-property           
   #:name                                      
   (λ (arr) (simple-arrow-name arr))           
   #:late-neg-projection                       
   (λ (arr) (simple-arrow-late-neg-proj arr))))

To do the automatic coercion of values like integer? and #f into contracts, we need to call coerce-chaperone-contract (note that this rejects impersonator contracts and does not insist on flat contracts; to do either of those things, call coerce-contract or coerce-flat-contract instead).

(define (simple-arrow-contract dom rng)                       
  (simple-arrow (coerce-contract 'simple-arrow-contract dom)  
                (coerce-contract 'simple-arrow-contract rng)))

To define simple-arrow-name is straight-forward; it needs to return an s-expression representing the contract:

(define (simple-arrow-name arr)                 
  `(-> ,(contract-name (simple-arrow-dom arr))  
       ,(contract-name (simple-arrow-rng arr))))

And we can define the projection using a generalization of the projection we defined earlier, this time using chaperones:

(define (simple-arrow-late-neg-proj arr)                                 
  (define dom-ctc (get/build-late-neg-projection (simple-arrow-dom arr)))
  (define rng-ctc (get/build-late-neg-projection (simple-arrow-rng arr)))
  (λ (blame)                                                             
    (define dom+blame (dom-ctc (blame-add-context blame                  
                                                  "the argument of"      
                                                  #:swap? #t)))          
    (define rng+blame (rng-ctc (blame-add-context blame "the range       
of")))                                                                   
    (λ (f neg-party)                                                     
      (if (and (procedure? f)                                            
               (procedure-arity-includes? f 1))                          
          (chaperone-procedure                                           
           f                                                             
           (λ (arg)                                                      
             (values                                                     
              (λ (result) (rng+blame result neg-party))                  
              (dom+blame arg neg-party))))                               
          (raise-blame-error                                             
           blame #:missing-party neg-party                               
           f                                                             
           '(expected "a procedure of one argument" given: "~e")         
           f)))))                                                        
(define/contract (f x)                     
  (simple-arrow-contract integer? boolean?)
  "not a boolean")                         
> (f #f)                                   
f: contract violation                      
  expected: integer?                       
  given: #f                                
  in: the argument of                      
      (-> integer? boolean?)               
  contract from: (function f)              
  blaming: top-level                       
   (assuming the contract is correct)      
  at: eval:12.0                            
> (f 1)                                    
f: broke its own contract                  
  promised: boolean?                       
  produced: "not a boolean"                
  in: the range of                         
      (-> integer? boolean?)               
  contract from: (function f)              
  blaming: (function f)                    
   (assuming the contract is correct)      
  at: eval:12.0                            

8.2. With all the Bells and Whistles

There are a number of optional pieces to a contract that simple-arrow-contract did not add. In this section, we walk through all of them to show examples of how they can be implemented.

The first is a first-order check. This is used by or/c in order to determine which of the higher-order argument contracts to use when it sees a value. Heres the function for our simple arrow contract.

(define (simple-arrow-first-order ctc)          
  (λ (v) (and (procedure? v)                    
              (procedure-arity-includes? v 1))))

It accepts a value and returns #f if the value is guaranteed not to satisfy the contract, and #t if, as far as we can tell, the value satisfies the contract, just be inspecting first-order properties of the value.

The next is random generation. Random generation in the contract library consists of two pieces: the ability to randomly generate values satisfying the contract and the ability to exercise values that match the contract that are given, in the hopes of finding bugs in them (and also to try to get them to produce interesting values to be used elsewhere during generation).

To exercise contracts, we need to implement a function that is given a arrow-contract struct and some fuel. It should return two values: a function that accepts values of the contract and exercises them, plus a list of values that the exercising process will always produce. In the case of our simple contract, we know that we can always produce values of the range, as long as we can generate values of the domain (since we can just call the function). So, heres a function that matches the exercise argument of build-chaperone-contract-propertys contract:

(define (simple-arrow-contract-exercise arr)                        
  (define env (contract-random-generate-get-current-environment))   
  (λ (fuel)                                                         
    (define dom-generate                                            
      (contract-random-generate/choose (simple-arrow-dom arr) fuel))
    (cond                                                           
      [dom-generate                                                 
       (values                                                      
        (λ (f) (contract-random-generate-stash                      
                env                                                 
                (simple-arrow-rng arr)                              
                (f (dom-generate))))                                
        (list (simple-arrow-rng arr)))]                             
      [else                                                         
       (values void '())])))                                        

If the domain contract can be generated, then we know we can do some good via exercising. In that case, we return a procedure that calls f the function matching the contract with something that we generated from the domain, and we stash the result value in the environment too. We also return (simple-arrow-rng arr) to indicate that exercising will always produce something of that contract.

If we cannot, then we simply return a function that does no exercising `void` and the empty list (indicating that we wont generate any values).

Then, to generate values matching the contract, we define a function that when given the contract and some fuel, makes up a random function. To help make it a more effective testing function, we can exercise any arguments it receives, and also stash them into the generation environment, but only if we can generate values of the range contract.

(define (simple-arrow-contract-generate arr)                              
  (λ (fuel)                                                               
    (define env (contract-random-generate-get-current-environment))       
    (define rng-generate                                                  
      (contract-random-generate/choose (simple-arrow-rng arr) fuel))      
    (cond                                                                 
      [rng-generate                                                       
       (λ ()                                                              
         (λ (arg)                                                         
           (contract-random-generate-stash env (simple-arrow-dom arr) arg)
           (rng-generate)))]                                              
      [else                                                               
       #f])))                                                             

When the random generation pulls something out of the environment, it needs to be able to tell if a value that has been passed to contract-random-generate-stash is a candidate for the contract it is trying to generate. Of course, it the contract passed to contract-random-generate-stash is an exact match, then it can use it. But it can also use the value if the contract is stronger (in the sense that it accepts fewer values).

To provide that functionality, we implement this function:

(define (simple-arrow-first-stronger? this that)     
  (and (simple-arrow? that)                          
       (contract-stronger? (simple-arrow-dom that)   
                           (simple-arrow-dom this))  
       (contract-stronger? (simple-arrow-rng this)   
                           (simple-arrow-rng that))))

This function accepts this and that, two contracts. It is guaranteed that this will be one of our simple arrow contracts, since were supplying this function together with the simple arrow implementation. But the that argument might be any contract. This function checks to see if that is also a simple arrow contract and, if so compares the domain and range. Of course, there are other contracts that we could also check for e.g., contracts built using `->` or `->*`, but we do not need to. The stronger function is allowed to return #f if it doesnt know the answer but if it returns #t, then the contract really must be stronger.

Now that we have all of the pieces implemented, we need to pass them to build-chaperone-contract-property so the contract system starts using them:

(struct simple-arrow (dom rng)                                    
  #:property prop:custom-write contract-custom-write-property-proc
  #:property prop:chaperone-contract                              
  (build-chaperone-contract-property                              
   #:name                                                         
   (λ (arr) (simple-arrow-name arr))                              
   #:late-neg-projection                                          
   (λ (arr) (simple-arrow-late-neg-proj arr))                     
   #:first-order simple-arrow-first-order                         
   #:stronger simple-arrow-first-stronger?                        
   #:generate simple-arrow-contract-generate                      
   #:exercise simple-arrow-contract-exercise))                    
(define (simple-arrow-contract dom rng)                           
  (simple-arrow (coerce-contract 'simple-arrow-contract dom)      
                (coerce-contract 'simple-arrow-contract rng)))    

We also add a prop:custom-write property so that the contracts print properly, e.g.:

> (simple-arrow-contract integer? integer?)
(-> integer? integer?)                     

(We use prop:custom-write because the contract library can not depend on

#lang racket/generic

but yet still wants to provide some help to make it easy to use the right printer.)

Now that thats done, we can use the new functionality. Heres a random function, generated by the contract library, using our simple-arrow-contract-generate function:

(define a-random-function                     
  (contract-random-generate                   
   (simple-arrow-contract integer? integer?)))
> (a-random-function 0)                       
-1.0                                          
> (a-random-function 1)                       
1                                             

Heres how the contract system can now automatically find bugs in functions that consume simple arrow contracts:

(define/contract (misbehaved-f f)                   
  (-> (simple-arrow-contract integer? boolean?) any)
  (f "not an integer"))                             
> (contract-exercise misbehaved-f)                  
misbehaved-f: broke its own contract                
  promised: integer?                                
  produced: "not an integer"                        
  in: the argument of                               
      the 1st argument of                           
      (-> (-> integer? boolean?) any)               
  contract from: (function misbehaved-f)            
  blaming: (function misbehaved-f)                  
   (assuming the contract is correct)               
  at: eval:25.0                                     

And if we hadnt implemented simple-arrow-first-order, then or/c would not be able to tell which branch of the or/c to use in this program:

(define/contract (maybe-accepts-a-function f)
  (or/c (simple-arrow-contract real? real?)  
        (-> real? real? real?)               
        real?)                               
  (if (procedure? f)                         
      (if (procedure-arity-includes f 1)     
          (f 1132)                           
          (f 11 2))                          
      f))                                    
> (maybe-accepts-a-function sqrt)            
maybe-accepts-a-function: contract violation 
  expected: real?                            
  given: #<procedure:sqrt>                   
  in: the argument of                        
      a part of the or/c of                  
      (or/c                                  
       (-> real? real?)                      
       (-> real? real? real?)                
       real?)                                
  contract from:                             
      (function maybe-accepts-a-function)    
  blaming: top-level                         
   (assuming the contract is correct)        
  at: eval:27.0                              
> (maybe-accepts-a-function 123)             
123                                          

9. Gotchas

9.1. Contracts and eq?

As a general rule, adding a contract to a program should either leave the behavior of the program unchanged, or should signal a contract violation. And this is almost true for Racket contracts, with one exception: eq?.

The eq? procedure is designed to be fast and does not provide much in the way of guarantees, except that if it returns true, it means that the two values behave identically in all respects. Internally, this is implemented as pointer equality at a low-level so it exposes information about how Racket is implemented and how contracts are implemented.

Contracts interact poorly with eq? because function contract checking is implemented internally as wrapper functions. For example, consider this module:

#lang racket                                              
                                                          
(define (make-adder x)                                    
  (if (= 1 x)                                             
      add1                                                
      (lambda (y) (+ x y))))                              
(provide (contract-out                                    
          [make-adder (-> number? (-> number? number?))]))

It exports the make-adder function that is the usual curried addition function, except that it returns Rackets add1 when its input is 1.

You might expect that

(eq? (make-adder 1) 
     (make-adder 1))

would return #t, but it does not. If the contract were changed to any/c or even `(-> number? any/c)`, then the eq? call would return #t.

Moral: Do not use eq? on values that have contracts.

9.2. Contract boundaries and define/contract

The contract boundaries established by define/contract, which creates a nested contract boundary, are sometimes unintuitive. This is especially true when multiple functions or other values with contracts interact. For example, consider these two interacting functions:

> (define/contract (f x)             
    (-> integer? integer?)           
    x)                               
> (define/contract (g)               
    (-> string?)                     
    (f "not an integer"))            
> (g)                                
f: contract violation                
  expected: integer?                 
  given: "not an integer"            
  in: the 1st argument of            
      (-> integer? integer?)         
  contract from: (function f)        
  blaming: top-level                 
   (assuming the contract is correct)
  at: eval:2.0                       

One might expect that the function g will be blamed for breaking the terms of its contract with f. Blaming g would be right if f and g were directly establishing contracts with each other. They arent, however. Instead, the access between f and g is mediated through the top-level of the enclosing module.

More precisely, f and the top-level of the module have the (-> integer? integer?) contract mediating their interaction; g and the top-level have (-> string?) mediating their interaction, but there is no contract directly between f and g. This means that the reference to f in the body of g is really the top-level of the modules responsibility, not gs. In other words, the function f has been given to g with no contract between g and the top-level and thus the top-level is blamed.

If we wanted to add a contract between g and the top-level, we can use define/contracts #:freevar declaration and see the expected blame:

> (define/contract (f x)              
    (-> integer? integer?)            
    x)                                
> (define/contract (g)                
    (-> string?)                      
    #:freevar f (-> integer? integer?)
    (f "not an integer"))             
> (g)                                 
f: contract violation                 
  expected: integer?                  
  given: "not an integer"             
  in: the 1st argument of             
      (-> integer? integer?)          
  contract from: top-level            
  blaming: (function g)               
   (assuming the contract is correct) 
  at: eval:6.0                        

Moral: if two values with contracts should interact, put them in separate modules with contracts at the module boundary or use #:freevar.

9.3. Exists Contracts and Predicates

Much like the eq? example above, #:∃ contracts can change the behavior of a program.

Specifically, the null? predicate and many other predicates return #f for #:∃ contracts, and changing one of those contracts to any/c means that null? might now return #t instead, resulting in arbitrarily different behavior depending on how this boolean might flow around in the program.

 #lang racket/exists package: [base](https://pkgs.racket-lang.org/package/base)

To work around the above problem, the racket/exists library behaves just like racket, but predicates signal errors when given #:∃ contracts.

Moral: Do not use predicates on #:∃ contracts, but if youre not sure, use racket/exists to be safe.

9.4. Defining Recursive Contracts

When defining a self-referential contract, it is natural to use define. For example, one might try to write a contract on streams like this:

> (define stream/c                                   
    (promise/c                                       
     (or/c null?                                     
           (cons/c number? stream/c))))              
stream/c: undefined;                                 
 cannot reference an identifier before its definition
  in module: top-level                               

Unfortunately, this does not work because the value of stream/c is needed before it is defined. Put another way, all of the combinators evaluate their arguments eagerly, even though the values that they accept do not.

Instead, use

(define stream/c                                     
  (promise/c                                         
   (or/c                                             
    null?                                            
    (cons/c number? (recursive-contract stream/c)))))

The use of recursive-contract delays the evaluation of the identifier stream/c until after the contract is first checked, long enough to ensure that stream/c is defined.

See also Checking Properties of Data Structures.

9.5. Mixing set! and contract-out

The contract library assumes that variables exported via contract-out are not assigned to, but does not enforce it. Accordingly, if you try to set! those variables, you may be surprised. Consider the following example:

> (module server racket                           
    (define (inc-x!) (set! x (+ x 1)))            
    (define x 0)                                  
    (provide (contract-out [inc-x! (-> void?)]    
                           [x integer?])))        
> (module client racket                           
    (require 'server)                             
                                                  
    (define (print-latest) (printf "x is ~s\n" x))
                                                  
    (print-latest)                                
    (inc-x!)                                      
    (print-latest))                               
> (require 'client)                               
x is 0                                            
x is 0                                            

Both calls to print-latest print 0, even though the value of x has been incremented and the change is visible inside the module `x`.

To work around this, export accessor functions, rather than exporting the variable directly, like this:

#lang racket                                  
                                              
(define (get-x) x)                            
(define (inc-x!) (set! x (+ x 1)))            
(define x 0)                                  
(provide (contract-out [inc-x! (-> void?)]    
                       [get-x (-> integer?)]))

Moral: This is a bug that we will address in a future release.