<div>and shared it privately with me.<br></div><div><br></div>It is a bad habit.  In the future I'll make my replies public to avoid redundancies. <div><br></div><div>Felix, thank you for your comments. </div><div><br> </div><div>In Matthias's original proposed solution, X was unconstrained...</div><div><br></div><div>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....</div> <div><br></div><div>Thanks, </div><div>Dave<br><br><div class="gmail_quote">On Mon, Nov 10, 2008 at 11:52 AM, Matthias Felleisen <span dir="ltr"><<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>></span> wrote:<br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><br> David found my mistake in the pedagogic exercise and share it privately with me.<div><div></div><div class="Wj3C7c"><br> <br> <br> <br> <br> On Nov 10, 2008, at 2:43 PM, Felix Klock's PLT scheme proxy wrote:<br> <br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> David (cc'ing Matthias and the plt-scheme list)-<br> <br> On Nov 7, 2008, at 11:57 AM, Matthias Felleisen wrote:<br> <br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">  (X U -> U) W U Nat -> U<br> <br> 4. The second argument is used as the first input to f so U = W<br> <br>  (X U -> U) U U Nat -> U<br> <br> 5. No other constraints so we're fine<br> <br> And I may have made a mistake so check the calculation -- Matthias<br> </blockquote> <br> Step 4 makes an incorrect deduction.<br> <br> I believe it should be:<br> <br> 4. The second argument is used as the first input to f, so X = W<br> <br>  (X U -> U) X U Nat -> U<br> <br> 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.<br> <br> ----<br> <br> 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.<br> <br> -Felix Klock<br> <br> <br> </blockquote> <br> </div></div></blockquote></div><br></div>