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

Huh? 

On Jun 26, 2012, at 9:27 PM, Robby Findler wrote:

> Well, you wouldn't. Are the implementations of the contracts proven to
> be equivalent currently? Or do you just have a theorem that matches up
> the ones in some model somewhere?
> 
> Robby
> 
> On Tue, Jun 26, 2012 at 8:05 PM, Matthias Felleisen
> <matthias at ccs.neu.edu> 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
>>