<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Dec 29, 2012 at 9:09 PM, Neil Toronto <span dir="ltr"><<a href="mailto:neil.toronto@gmail.com" target="_blank">neil.toronto@gmail.com</a>></span> wrote:<br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 12/29/2012 06:18 PM, Robby Findler wrote:<br> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"> On Sat, Dec 29, 2012 at 3:57 PM, Matthias Felleisen<br></div><div class="im"> <<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a> <mailto:<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>>> wrote:<br> <br> I think the questions really concern the interaction between TR's<br> generation of contracts and contracts themselves:<br> <br> 1. TR does not seem to exploit as much knowledge as possible when<br> it generates contracts.<br> Example: (All (a) ((Foo -> a) Foo -> a) seems to be such an example<br> (perhaps extreme)<br> Where can Foo come from? Why does TR wrap a contract around the<br> domain of Foo -> a --<br> TR proved that it is applied to Foo if anything. Is TR too<br> aggressive in negative positions?<br> </div></blockquote> <br> I'm almost certain it is. Sam? (Wherefore art thou, Sam?)<br> <br> I can see an argument for having overly aggressive contracts at first, before having large test cases that demonstrate TR's implementation is almost always sound. If these are training wheels, though, we should consider removing them. The math library alone has at least 18k lines of TR code, it and exercises the type system pretty thoroughly.<div class="im"> <br> <br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> In this case, the chaperone is necessary, since the "a" means one value<br> (not multiple), so you cannot eliminate the contract. Sadly.<br> </blockquote> <br></div> One asymmetry between multiple arguments and multiple return values is that the number of arguments a procedure accepts is observable, but the number of return values isn't. If it were observable, and TR were less aggressive with the first `Foo', a chaperone would be unnecessary.<br> <br> There have got to be other uses for that, but I can't think of any offhand. Something to do with continuations, maybe? But TR could easily annotate lambdas with the number of values they return.<div class="im"><br> <br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> 2. Multiple crossings impose the same contracts over and over. BUT<br> 'same' is not necessarily<br> expressed as eq?. Can the contract library do better here? Is the<br> 'inner loop' assumption<br> wrong?<br> <br> <br> The contract system has support for comparing contracts in a useful way<br> for this (contract-stronger?). The problem Neil ⊥ identified is that the<br> values that go thru them are rarely eq? so checking the contracts that<br> are on the values isn't helpful since they've changed just enough to<br> avoid being able to detect that the are the "same" value.<br> <br> At least that's what I understood from him.<br> </blockquote> <br></div> That's right.<br> <br> But the array values - their procedures in particular - almost always have an equivalent contract. Is it possible to retrieve the contract on a value, check it, and pass the value through unchanged if the additional contract you're considering putting on it isn't stronger?<div class="im"> <br></div></blockquote><div><br></div><div style>That's what the patch I sent does I think (specifically in the case of an arrow contract on a function)? Am I missing something?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="im"> <br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> But thinking a little bit more about this: I think that maybe we're<br> seeing a slightly distored picture on this last point. The functions<br> that Neil was using in his examples didn't do anything and normally<br> functions would do something, so the cost for this point is exaggerated<br> as compared to what would happen in a real program.<br> </blockquote> <br></div> No. No, no, no. This isn't distorted. With automatically deforesting arrays, function call overhead is almost everything. The array procedures themselves do very little: they usually just call other array procedures, tweaking the input or output. (Example: the procedure of the array returned by `matrix-transpose' calls the original array's procedure with swapped row and column indexes.)<br> <br> To see an example using arrays that do something, load up "math/tests/mandelbrot-test.<u></u>rkt". Add the line<br> <br> (time (void (mandelbrot 0.05 20)))<br> <br> somewhere after the `mandelbrot' definition, and run it. On my computer, it reports 30ms.<br> <br> Change the language to Racket. Change the line<br> <br> (define c (array->fcarray (array-make-rectangular x y)))<br> <br> to<br> <br> (define c (array->fcarray (inline-array-map make-rectangular x y)))<br> <br> (because there's currently a problem using `array-make-rectangular' in untyped code). Run it. On my computer, it reports 2700ms, or about 90x the time taken by the typed code.<span class="HOEnZb"><font color="#888888"><br> <br><br></font></span></blockquote><div><br></div><div style>Well, then, improving runtime support for chaperones might be a good direction to look, then. Seems like being able to inline thru chaperones and distribute checks around might take a lot of work (I'm not sure) but it seems like there is a lot of things one might do.</div> <div style><br></div><div style>Robby </div></div><br></div></div>