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

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.

Neil ⊥

On 06/26/2012 07:05 PM, Matthias Felleisen wrote:
>
> How would you check soundness between a type and its contract?
>
> Types, like theorem provers, are addictive. The more expressivity
> they provide, the more programmers want to play with them.
>
> Use Real ->  Real and you'll be fine. -- Matthias
>
>
>
> On Jun 26, 2012, at 8:37 PM, Robby Findler wrote:
>
>> In this case, the contract could turn into a dependent one with the
>> same semantics. Does it make sense for TR to allow a user to declare
>> the equivalent contract?
>>
>> Robby
>>
>> On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto<neil.toronto at gmail.com>  wrote:
>>> Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to
>>> have precise types. For example, log1p could have the type
>>>
>>>   (case->  (Zero ->  Zero)
>>>           (Float ->  Float)
>>>           (Real ->  Real))
>>>
>>> It was easy to get the implementation to typecheck, but when I tried to plot
>>> it in untyped Racket, I got this:
>>>
>>>   Type Checker: The type of log1p cannot be converted to a contract in: log1p
>>>
>>> I really don't want to have two versions of the library. Could TR use the
>>> most general type (Real ->  Real) as the contract? Or would that be unsound?
>>>
>>> Neil ⊥
>>> _________________________
>>>   Racket Developers list:
>>>   http://lists.racket-lang.org/dev
>>
>> _________________________
>>   Racket Developers list:
>>   http://lists.racket-lang.org/dev
>