[plt-scheme] Problem with Contracts - HtDP 21.1.3
On Nov 6, 2008, at 10:53 PM, David Yrueta wrote:
> ;apply function f to x n times with a base case of TH where n=0
> ;(check-expect (natural-f cons 'x empty 5) (list 'x 'x 'x 'x 'x))
> ;(check-expect (natural-f + 1 5 9) 14)
> (define (natural-f f x TH n)
> (cond
> [(zero? n) TH]
> [else (f x
> (natural-f f x TH (sub1 n) ))]))
> ...
> --then what is the general contract for "natural-f"?
..
> my guess is that the proper general contract for "natural-f" would be:
>
> ;natural-f: (X Y -> Y) X Y number -> Y
Yes, that looks good to me.
> Considering "natural-f" as an abstraction of function "n-adder"
> above, the resulting contract would be:
> (number number -> number) number number number -> number
Right: in this case both X and Y are number.
> But what would the contract for "natural-f" be if it was viewed as
> an abstraction of function "copy?"
> (ex.(check-expect (natural-f cons 'x empty 5) (list 'x 'x 'x 'x 'x))
>
> In that case, argument "f" would take the value of "cons," so the
> question (for me) comes down to how to represent the primitive
> "cons" as a function type within a contract.
>
> Is "cons" represented as (X Y -> Y)
> where X is any Scheme ITEM, Y is the Scheme-value list, and the
> result is basic type Y (Scheme-value list)?
>
> Or is "cons" represented as (X list -> (listof X)
> where X is any Scheme ITEM, "list" is Scheme-value list, and the
> result is defined type (listof X)?
The former is correct, but less informative than it could be. The
latter (as amended; see below) is also correct, and more
informative. In general, we say
cons : X list-of-X -> list-of-X
so this fits into the natural-f framework perfectly well with Y =
list-of-X
What the contract really means is "for any set X, if cons is called
on an element of set X and a list all of whose elements are in set X,
then the result will be a list all of whose elements are in set X."
The set X doesn't have to be a standard data type; it really is ANY
set of Scheme-representable objects. So if somebody should happen to
call "cons" on a number and a list of strings, the contract still
applies but is less informative because you need to define X as
"number or string" in order for the preconditions to hold.
Stephen Bloch
sbloch at adelphi.edu