[plt-scheme] Problem with Contracts - HtDP 21.1.3

David found my mistake in the pedagogic exercise and share it  
privately with me.




On Nov 10, 2008, at 2:43 PM, Felix Klock's PLT scheme proxy wrote:

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