[racket-dev] math collection [was: Hyperbolic functions]

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Tue Jun 26 21:34:35 EDT 2012

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 :)


On Tue, Jun 26, 2012 at 8:29 PM, Matthias Felleisen
<matthias at 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
>> <matthias at 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

Posted on the dev mailing list.