[racket-dev] Single-flonum-ness not preserved in racket/math functions

On 06/05/2012 03:57 PM, Vincent St-Amour wrote:
> At Tue, 05 Jun 2012 15:45:09 -0600,
> Neil Toronto wrote:
>> Vincent, is there a quick way for me to test whether the types I give
>> the new functions are sound?
>
> I recently added redex-based random testing for TR's float types. It's
> in collects/tests/typed-racket/tr-random-testing.rkt.
>
> Currently, it only tests flonum (i.e. double precision) operations and
> types, but it should be easy to expand to single-flonums.

Thanks! I've adapted it and will commit the changes with the ones to 
racket/math.

I've managed to make it always find a counterexample. But there are only 
a few single-flonum -> flonum issues. Most of them are because I've 
changed the random-flonum-generating code to sometimes generate *very* 
small random numbers. Here's the counterexample I found earlier today 
that motivated that change to the random testing:

#lang typed/racket

(require/typed
  unstable/flonum
  [+min.0  Positive-Float])  ; the smallest positive flonum

 > +min.0
- : Float [generalized from Positive-Float]
4.9406564584125e-324
 > (sqr +min.0)
- : Float [generalized from Positive-Float]
0.0


I'm not comfortable messing with those precise primitive types yet, so 
I'll let you handle that. When I push my commits tomorrow, 
tr-random-testing.rkt will fail. After you've fixed the erroneous types, 
I'll be able to use your fixes to figure out the right types for the 
functions I added to racket/math.

Neil ⊥