On 10/01/2012 02:06 PM, Sam Tobin-Hochstadt wrote:
On Mon, Oct 1, 2012 at 2:26 PM, Neil Toronto <neil.toro...@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 ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
