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

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