[racket-dev] Math library initial commit almost ready; comments on issues welcome

On 10/01/2012 02:06 PM, Sam Tobin-Hochstadt wrote:
> On Mon, Oct 1, 2012 at 2:26 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
>>   * `math/base' re-exports `racket/math', but with extra constants (like
>> `phi.0') and functions (like `power-of-two?'). It also exports improved
>> hyperbolic functions, such as a new `sinh' that's much more accurate near
>> zero: in the worst case, 2e-16 relative error (which is great) instead of
>> 0.5 (which is really bad). But its type in `math/base' is
>>
>>    (case-> (Zero -> Zero)
>>            (Flonum -> Flonum)
>>            (Real -> Real)
>>            (Float-Complex -> Float-Complex)
>>            (Complex -> Complex))
>>
>> I haven't been able to give it a type as specific as the type of the `sinh'
>> exported from `racket/math'.
>
> Why aren't you able to do this?

Shortly, because the type checker doesn't have enough information to 
check only reachable code in each pass through the function's 
definition. Here's `flsinh' without most of its implementation, and with 
only three of its potential `case->' types:

   #lang typed/racket

   (require racket/flonum)

   (: flsinh+ (Positive-Flonum -> Positive-Flonum))
   (define (flsinh+ x) (error 'unimplemented))

   (: flsinh (case-> (Negative-Flonum -> Negative-Flonum)
                     (Positive-Flonum -> Positive-Flonum)
                     (Flonum -> Flonum)))
   (define (flsinh x)
     (cond [(x . fl> . 0.0)  (flsinh+ x)]
           [(x . fl< . 0.0)  (- (flsinh+ (- x)))]
           [else  x]))

While TR checks the definition of `flsinh' with the type Negative-Flonum 
-> Negative-Flonum, it gives this type error:

   Type Checker: Expected Negative-Flonum, but got Positive-Flonum in:
   (flsinh+ x)

It doesn't know that (flsinh+ x) is unreachable when x : 
Negative-Flonum. There are similar type errors in the second clause with 
flsinh : Positive-Flonum -> Positive-Flonum.

This definition also fails in the same way:

   (define (flsinh x)
     (cond [(negative? x)  (- (flsinh+ (- x)))]
           [(positive? x)  (flsinh+ x)]
           [else  x]))

This definition gives only one type error, in the first clause:

   (define (flsinh x)
     (cond [((make-predicate Positive-Flonum) x)  (flsinh+ x)]
           [((make-predicate Negative-Flonum) x)  (- (flsinh+ (- x)))]
           [else  x]))

By the second clause, x : Negative-Flonum when `flsinh' has either type. 
(It actually leaves Flonum-Nan out of the type of `x', which is 
impressively correct. :D)

This WOULD work:

   (define (flsinh x)
     (cond [(flpositive? x)  (flsinh+ x)]
           [(flnegative? x)  (- (flsinh+ (- x)))]
           [else  x]))

if I could define `flpositive?' and `flnegative?' with the types

   (: flnegative? (case-> (Nonnegative-Flonum -> False : Nothing)
                          (Flonum -> Boolean : Negative-Flonum)))

   (: flpositive? (case-> (Nonpositive-Flonum -> False : Nothing)
                          (Flonum -> Boolean : Positive-Flonum)))

But I haven't been able to implement them for the same reason I can't 
define `flsinh' with more specific types. Also, it looks like a hack.

Neil ⊥