I agree with that, to a point. Here were are now considering a very concrete tradeoff, however: asking the user to cope with code duplication in return for ... what? Very little, I claim. In particular, I think that TR already has lots of type+contracts that are asserted (not proven) to be equivalent. For example, + seems to have a pretty big type in the implementation--- has that contract been proven to match to the type?
That is, what I'm trying to say is that there are currently a few people that can make these unproven assertions about types and contracts that match up. Why should they be the only ones? EVEN BETTER: we can use random testing to falsify these! Systematically! Vincent is already doing this a little bit and he has found bugs. If we make this an explicit thing to connect types to contracts and allow people to make more connections, then we can do a better job finding bugs in the currently untested/unproven ones! (random testing uber alles :) Robby On Tue, Jun 26, 2012 at 8:29 PM, Matthias Felleisen <matth...@ccs.neu.edu> wrote: > > Because the point of types is to have something proven. > > > On Jun 26, 2012, at 9:29 PM, Robby Findler wrote: > >> This sounds like a terrible solution. >> >> There are lots of places in our system where we just declare facts and >> don't prove them and then use them for lots of things (often >> optimizations). Why should this one be special? >> >> Robby >> >> On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen >> <matth...@ccs.neu.edu> wrote: >>> >>> On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: >>> >>>> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that >>>> (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. >>>> :) >>>> >>>> Another option is to provide both log1p and fllog1p. I just wrote fllog1p >>>> anyway. >>> >>> >>> Sounds like the right solution -- and now you see how every type system >>> forces you to duplicate code. -- Matthias >>> > _________________________ Racket Developers list: http://lists.racket-lang.org/dev