<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Dec 29, 2012 at 3:57 PM, Matthias Felleisen <span dir="ltr"><<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>></span> wrote:<br>
<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"><div style="word-wrap:break-word"><div class="im"><br><div>
<div>On Dec 28, 2012, at 8:04 PM, Robby Findler wrote:</div><br><blockquote type="cite"><span style="border-collapse:separate;font-family:'Lucida Grande';font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:-webkit-auto;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;font-size:medium">Overall, I feel like some of what you're asking has to do with what TR is doing and some with what's going on inside the procedure chaperones and so I'm not sure the contract library itself is a place where fixes can happen.</span></blockquote>
</div><br><div><br></div></div><div>I think the questions really concern the interaction between TR's generation of contracts and contracts themselves: </div><div><br></div><div> 1. TR does not seem to exploit as much knowledge as possible when it generates contracts. </div>
<div><span style="white-space:pre-wrap"> </span>Example: (All (a) ((Foo -> a) Foo -> a) seems to be such an example (perhaps extreme)</div><div><span style="white-space:pre-wrap"> </span>Where can Foo come from? Why does TR wrap a contract around the domain of Foo -> a -- </div>
<div><span style="white-space:pre-wrap"> </span>TR proved that it is applied to Foo if anything. Is TR too aggressive in negative positions? </div><div> </div></div></blockquote><div><br></div><div style>In this case, the chaperone is necessary, since the "a" means one value (not multiple), so you cannot eliminate the contract. Sadly.</div>
<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"><div style="word-wrap:break-word"><div> 2. Multiple crossings impose the same contracts over and over. BUT 'same' is not necessarily </div>
<div><span style="white-space:pre-wrap"> </span>expressed as eq?. Can the contract library do better here? Is the 'inner loop' assumption </div><div><span style="white-space:pre-wrap"> </span>wrong? </div><div><br>
</div></div></blockquote><div><br></div><div style>The contract system has support for comparing contracts in a useful way for this (contract-stronger?). The problem Neil ⊥ identified is that the values that go thru them are rarely eq? so checking the contracts that are on the values isn't helpful since they've changed just enough to avoid being able to detect that the are the "same" value. </div>
<div style><br></div><div style>At least that's what I understood from him.</div><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">
<div style="word-wrap:break-word"><div></div><div> 3. And then there seems to be a chaperone question, though I don't understand that one. </div><div><br></div><div><br></div></div></blockquote><div><br></div><div style>
What I meant was that the runtime system has much smoother paths in place for calling a function than for calling a function with a chaperone on it. And so when Neil uses the profiler to try to find the time difference, he's not seeing anything because the time is invisible to the profiler: it is all being taken up by the slow path for calling a function with a chaperone on it.</div>
<div><br></div><div style>But thinking a little bit more about this: I think that maybe we're seeing a slightly distored picture on this last point. The functions that Neil was using in his examples didn't do anything and normally functions would do something, so the cost for this point is exaggerated as compared to what would happen in a real program.</div>
<div style><br></div><div style>Robby</div></div><br></div></div>