racket / typed-racket

Typed Racket
Other
527 stars 104 forks source link

random numeric testing failures #1042

Open samth opened 3 years ago

samth commented 3 years ago
gus-massa commented 3 years ago

About the last one (6)

I found a minimized version:

> (/ (min 0.0 0))
- : Real [more precisely: Nonpositive-Real]
+inf.0

I think the problem is in https://github.com/racket/typed-racket/blob/6ea20bec8d41e1a188d7f831c35423293a89c98e/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt#L1234 because 0.0 is a -NonPosReal, but +inf.0 isn't.

gus-massa commented 3 years ago

About the second example in the second to last case (5b)

I found a minimized version:

(- (expt 10 309) +inf.0)        ;==> +nan.0 in typed  but -inf.0 in untyped

The problem is that in some optimization step (expt 10 309) is converted to a flonum, in this case +inf.0 so the expression is equivalent to (- +inf.0 +inf.0). I don't have any clue where the error is, but it's possible to construct similar examples with other operation, so my guess it's a shared code.

Note that the problem disappears replacing 309 with 307, because 1e307 is a normal flonum.

#lang typed/racket

(exact->inexact (expt 10 309))  ;==> +inf.0 (correct)
(- (expt 10 309) +inf.0)        ;==> +nan.0
(- (- (expt 10 309)) -inf.0)    ;==> +nan.0
(+ (expt 10 309) -inf.0)        ;==> +nan.0
(+ (- (expt 10 309)) +inf.0)    ;==> +nan.0
(* (expt 10 309) 0.0)           ;==> +nan.0
(/ +inf.0 (expt 10 309))        ;==> +nan.0
(/ (expt 10 309) 1.0)           ;==> +inf.0

(newline)

(exact->inexact (expt 10 307))  ;==> 1e+307
(- (expt 10 307) +inf.0)        ;==> -inf.0
(- (- (expt 10 307)) -inf.0)    ;==> +inf.0
(+ (expt 10 307) -inf.0)        ;==> -inf.0
(+ (- (expt 10 307)) +inf.0)    ;==> +inf.0
(* (expt 10 307) 0.0)           ;==>    0.0
(/ +inf.0 (expt 10 307))        ;==> +inf.0
(/ (expt 10 307) 1.0)           ;==> 1e+307
gus-massa commented 3 years ago

Again (5b) again:

The problem is that (- (expt 10 307) +inf.0) is transformed to (unsafe-fl- (->fl (expt 10 307)) +inf.0). My guess is that https://github.com/racket/typed-racket/blob/master/typed-racket-lib/typed-racket/optimizer/float.rkt#L126-L146 need also special cases for infinity.