[plt-scheme] new contracts: lazy struct contracts

From: Robby Findler (robby at cs.uchicago.edu)
Date: Sat Mar 18 19:11:00 EST 2006

The contract library now supports lazy contracts on (immutable)
structs. Details below (from the just checked in manual -- out in the
next nightly build).

Robby

============================================================

Typically, constracts on data structures can be written using flat
contracts. For example, one might write a sorted list contract as a
function that accepts a list and traverses it, ensuring that the
elements are in order. Such contracts, however, can change the
asymptotic running time of the program, since the contract may end up
exploring more of a function's input than the function itself does. To
circumvent this problem, the `define-contract-struct' form introduces
contract combinators that are lazy that is, they only verify the
contract holds for the portion of some data structure that is actually
inspected. More precisely, a lazy data structure contract on a struct
is not checked until a selector extracts a field of a struct.

The form

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

is like the corresponding define-struct, with two differences: it does
not define field mutators and it does define two contract constructors:
struct-name/c struct-name/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. It syntax is:

  (struct-name/dc field-spec ...)

where each field-spec is one of the following two lines:

  [field contract-expr]
  [field (field ...) contract-expr]

In each case, the first field name specifies which field the contract
applies to, and 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 field names in middle second indicate which
fields it depends on. These dependencies can only be to fields that
come earlier in the struct.

As an example consider this module:

(module product mzscheme
  (require (lib "contract.ss"))

  (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?)]))

It provides a 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.



Posted on the users mailing list.