<div dir="ltr">Thanks Robby<div><br></div><div>... and I was so close!</div><div><br></div><div>The revised and improved version of the slides is up:</div><div><br></div><div><a href="http://www.slideshare.net/DanielPrager/introduction-to-contracts-and-functional-contracts">http://www.slideshare.net/DanielPrager/introduction-to-contracts-and-functional-contracts</a><br> </div><div><br></div><div><br></div><div>Cheers</div><div><br></div><div>Dan</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Sep 5, 2013 at 7:37 AM, Robby Findler <span dir="ltr"><<a href="mailto:robby@eecs.northwestern.edu" target="_blank">robby@eecs.northwestern.edu</a>></span> wrote:<br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">You need to indicate that the contract on 'r' needs 'n', ie replace "[r (->i" with "[r (n) (->i".<span class="HOEnZb"><font color="#888888"><div> <br></div><div>Robby</div></font></span></div><div class="gmail_extra"><br><br> <div class="gmail_quote"><div><div class="h5">On Wed, Sep 4, 2013 at 4:33 PM, Daniel Prager <span dir="ltr"><<a href="mailto:daniel.a.prager@gmail.com" target="_blank">daniel.a.prager@gmail.com</a>></span> wrote:<br> </div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"> <div dir="ltr"><div><span style="color:rgb(34,34,34)">On Wed, Sep 4, 2013 at 7:58 AM, Matthias Felleisen </span><span dir="ltr" style="color:rgb(34,34,34)"><<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>></span><span style="color:rgb(34,34,34)"> wrote:</span><br> <br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">You can't. Sam has had this combination on his todo list for 7 years and he never got around to it. Perhaps I signed his dissertation too early :-)</blockquote> <div><br></div></div><div>I noticed that contract support is missing from TR. I have, however, constructed a roll-my-own contract example with TR, and it would be great if Sam (or another!) pushed forward on contract support for TR.</div> <div> <div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">This is from my code base. It is a function that consumes the dimensions of a (functional image) canvas and created a gridded image and an event handler that tells you on which "tile" a user clicked. It is highly real, higher-order, dependent, and yet not difficult to understand.</blockquote> <div class="gmail_extra"><br></div></div><div class="gmail_extra">Alas, I am having trouble mentally parsing this, but may still flash it up (with acknowledgement!) as a realistic example.</div><div class="gmail_extra"><br> </div> <div class="gmail_extra">In trying to construct a simpler (yet not easily do-able with static types) example I'm running into trouble getting my subcontract right.</div><div class="gmail_extra"><br></div><div class="gmail_extra"> I get an "n unbound identifier" error on the penultimate line:</div><div class="gmail_extra"><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_extra"><div class="gmail_extra"> ;; make-indenter: Nat -> (String -> String)</div></div><div class="gmail_extra"><div class="gmail_extra">;;</div></div><div class="gmail_extra"><div class="gmail_extra">;; Example: ((make-indenter 4) "foo") -> " foo"</div> </div><div class="gmail_extra"><div class="gmail_extra">;;</div></div><div class="gmail_extra"><div class="gmail_extra">(define/contract (make-indenter n)</div></div><div class="gmail_extra"><div class="gmail_extra"> (->i ([n natural-number/c])</div> </div><div class="gmail_extra"><div class="gmail_extra"> [r (->i ([s string?])</div></div><div class="gmail_extra"><div class="gmail_extra"> [result string?]</div></div><div class="gmail_extra"><div class="gmail_extra"> #:post (s result) (= (string-length result)</div></div><div class="gmail_extra"><div class="gmail_extra"> (+ n (string-length s))))])</div></div><div class="gmail_extra"> <div class="gmail_extra"> (λ (s) (string-append (make-string n #\space) s)))</div></div></blockquote><div class="gmail_extra"><br></div><div class="gmail_extra">How should I access 'n'?</div><div class="gmail_extra"><br></div><div class="gmail_extra"> <br></div><div class="gmail_extra">Many thanks</div><div class="gmail_extra"><br></div><div class="gmail_extra">Dan</div></div> <br></div></div><div class="im">____________________<br> Racket Users list:<br> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br> <br></div></blockquote></div><br></div> </blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr"><div style="font-family:arial;font-size:small"><b>Daniel Prager</b></div><div style="font-family:arial;font-size:small">Agile/Lean Coaching, Software Development and Leadership</div> <div style="font-family:arial;font-size:small"><font color="#999999">Twitter:</font> <a href="https://twitter.com/agilejitsu" style="color:rgb(17,85,204)" target="_blank">@agilejitsu</a> </div><div style="font-family:arial;font-size:small"> <font color="#999999">Blog:</font> <a href="http://agile-jitsu.blogspot.com/" style="color:rgb(17,85,204)" target="_blank">agile-jitsu.blogspot.com</a></div></div> </div>