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

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