7.3 Lazy Data-structure Contracts

(define-contract-struct id (field-id ...))

Like define-struct, but with two differences: it does not define field mutators, and it does define two contract constructors: id/c and id/dc. The first is a procedure that accepts as many arguments as there are fields and returns a contract for struct values whose fields match the arguments. The second is a syntactic form that also produces contracts on the structs, but the contracts on later fields may depend on the values of earlier fields.

The generated contract combinators are lazy: they only verify the contract holds for the portion of some data structure that is actually inspected. More precisely, a lazy data structure contract is not checked until a selector extracts a field of a struct.

(id/dc field-spec ...)

field-spec   =   [field-id contract-expr]     |   [field-id (field-id ...) contract-expr]

In each field-spec case, the first field-id specifies which field the contract applies to; the fields must be specified in the same order as the original define-contract-struct. The first case is for when the contract on the field does not depend on the value of any other field. The second case is for when the contract on the field does depend on some other fields, and the parenthesized field-ids indicate which fields it depends on; these dependencies can only be to earlier fields.

As an example, consider the following module:

(module product mzscheme

(require mzlib/contract)

(define-contract-struct kons (hd tl))

; sorted-list/gt : number -> contract

; produces a contract that accepts

; sorted kons-lists whose elements

; are all greater than num.

(define (sorted-list/gt num)

(or/c null?

(kons/dc [hd (>=/c num)]

[tl (hd) (sorted-list/gt hd)])))

; product : kons-list -> number

; computes the product of the values

; in the list. if the list contains

; zero, it avoids traversing the rest

; of the list.

(define (product l)

(cond

[(null? l) 1]

[else

(if (zero? (kons-hd l))

0

(* (kons-hd l)

(product (kons-tl l))))]))

(provide kons? make-kons kons-hd kons-tl)

(provide/contract [product (-> (sorted-list/gt -inf.0) number?)]))

The module provides a single function, product whose contract indicates that it accepts sorted lists of numbers and produces numbers. Using an ordinary flat contract for sorted lists, the product function cannot avoid traversing having its entire argument be traversed, since the contract checker will traverse it before the function is called. As written above, however, when the product function aborts the traversal of the list, the contract checking also stops, since the kons/dc contract constructor generates a lazy contract.