# [plt-scheme] Problem with Contracts - HtDP 21.1.3

 From: Matthias Felleisen (matthias at ccs.neu.edu) Date: Fri Nov 7 11:57:07 EST 2008 Previous message: [plt-scheme] Problem with Contracts - HtDP 21.1.3 Next message: [plt-scheme] Problem with Contracts - HtDP 21.1.3 Messages sorted by: [date] [thread] [subject] [author]

```
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
>   (cond
>     [(zero? n) x]
>     [else (+ 1
> --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
>
>
>
>
>
>
>
>
>
>
> _________________________________________________