<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Dec 28, 2012, at 8:04 PM, Robby Findler wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; font-family: 'Lucida Grande'; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 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>I think the questions really concern the interaction between TR's generation of contracts and contracts themselves: &nbsp;</div><div><br></div><div>&nbsp;1. TR does not seem to exploit as much knowledge as possible when it generates contracts.&nbsp;</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>Example: (All (a) ((Foo -&gt; a) Foo -&gt; a) seems to be such an example (perhaps extreme)</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>Where can Foo come from? Why does TR wrap a contract around the domain of Foo -&gt; a --&nbsp;</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>TR proved that it is applied to Foo if anything. Is TR too aggressive in negative positions?&nbsp;</div><div>&nbsp;</div><div>&nbsp;2. Multiple crossings impose the same contracts over and over. BUT 'same' is not necessarily&nbsp;</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>expressed as eq?. Can the contract library do better here? Is the 'inner loop' assumption&nbsp;</div><div><span class="Apple-tab-span" style="white-space:pre">        </span>wrong?&nbsp;</div><div><br></div><div>&nbsp;3. And then there seems to be a chaperone question, though I don't understand that one.&nbsp;</div><div><br></div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre">        </span></div></body></html>