[plt-scheme] Problem with Contracts - HtDP 21.1.3

On Nov 6, 2008, at 10:53 PM, David Yrueta wrote:


Think of cons as a function with contract

    X [Listof X] -> [Listof X]

The key is to start this "pattern matching exercises" by using  
variables for the various components of the contract:

1. natural-f takes four arguments and returns the third one. Also the  
fourth one is guaranteed to be a Nat and the first is a function of  
two args:

    (X Y -> Z) W U Nat -> U

2. The result of f is also a possible result of the function, so  
let's say Z = U

   (X Y -> U) W U Nat -> U

3. The second input to f is the result of natural-f, so Y = U

   (X U -> U) W U Nat -> U

4. The second argument is used as the first input to f so U = W

   (X U -> U) U U Nat -> U

5. No other constraints so we're fine

And I may have made a mistake so check the calculation -- Matthias







> If function "natural-f" --
>
> ;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) ))]))
>
> -- properly abstracts over the the functions 
>
> ;; copy : N X  ->  (listof X)
> ;; to create a list that contains
> ;; obj n times
> (define (copy n obj)
>   (cond
>     [(zero? n) empty]
>     [else (cons obj
>                 (copy (sub1 n) obj))]))
>  	
> ;; n-adder : N number  ->  number
> ;; to add n to x using
> ;; (+ 1 ...) only
> (define (n-adder n x)
>   (cond
>     [(zero? n) x]
>     [else (+ 1
>              (n-adder (sub1 n) x))]))
> --then what is the general contract for "natural-f"?
>
> Considering "natural-f" as an abstraction of function "n-adder"  
> above, the resulting contract would be:
> (number number -> number) number number number -> number
> (ex. (check-expect (natural-f + 1 5 9) 14)
>
> 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 difference between the two contracts appears to be in the  
> output types.  The first output type is basic, which is consistent  
> with the contract output for "n-adder"; the second output type is  
> defined, which conflicts with "n-adder."  Avoiding conflict means  
> choosing the first representation of "cons" in place of f in  
> "natural-f"'s contract. S my guess is that the proper general  
> contract for "natural-f" would be:
>
> ;natural-f: (X Y -> Y) X Y number -> Y
>
> Is this right? If not, where am I going wrong?
>
> Thanks,
> Dave
>
>
>
>
>
>
>
>
>
>
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20081107/0171b2ce/attachment.html>