[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