[plt-scheme] Problem with Contracts - HtDP 21.1.3

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Mon Nov 10 15:39:11 EST 2008

On Nov 10, 2008, at 3:10 PM, David Yrueta wrote:

> and shared it privately with me.

private is good in this example, though I doubt exposing the solution  
to 20.1.3 deep in a thread is much of a problem.




>
>
> It is a bad habit.  In the future I'll make my replies public to  
> avoid redundancies.
>
> Felix, thank you for your comments.
>
> In Matthias's original proposed solution, X was unconstrained...
>
> Is there a simple way to define the difference between a  
> constrained and unconstrained variable?  Is it the same as the  
> difference between bound and unbound?  Judging by your comment, it  
> seems that making the distinction can be useful, but I don't know  
> how to make it; further, I wouldn't appreciate the significance of  
> the distinction even if I could....
>
> Thanks,
> Dave
>
> On Mon, Nov 10, 2008 at 11:52 AM, Matthias Felleisen  
> <matthias at ccs.neu.edu> wrote:
>
> 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
>
>
>
>



Posted on the users mailing list.