<div dir="ltr"><div class="im"><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><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>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><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 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>