[plt-scheme] Problem with Contracts - HtDP 21.1.3

David (cc'ing Matthias and the plt-scheme list)-

On Nov 7, 2008, at 11:57 AM, Matthias Felleisen wrote:

>   (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

Step 4 makes an incorrect deduction.

I believe it should be:

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

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

The way I caught this: usually all of the parameters have some sort of  
relationship with other parts of the contract (on either side of the - 
 > arrow).  In Matthias's original proposed solution, X was  
unconstrained, which raised a red flag in my mind.

----

Also, there are ways to revise the interface to natural-f that  
completely eliminate the X from the contract, which may make for an  
interesting design exercise.

-Felix Klock