I thought it would be helpful to find the most precise types possible
for numeric functions. I wrote a program that infers them using a few
thousand representative argument values, which have been chosen to
exhibit underflow, overflow, exactness preservation (e.g. perfect
squares for `sqrt' and 1 for `log'), and every special value. It's here:
https://raw.github.com/ntoronto/plt-stuff/master/typed-racket/infer-numeric-types.rkt
I've already used it to find two errors:
1. Implementation of `sqrt': most Single-Float-Complex inputs yield
Float-Complex outputs. The type is sane, but the behavior isn't:
> (sqrt 1.0f0+5.2f0i)
- : Single-Flonum-Complex
1.7741590586312472+1.465482980223009i
2. Type of `expt'. The behavior looks crazy but is arguably correct
(it's a generalization of the IEEE/ISO standard to exact arguments):
> (expt 1 +nan.0)
- : Flonum [generalized from Positive-Flonum]
1
Inference generalizes return types a little (PosRatNotInt to PosRat, for
example), joins function types with the same return type, compresses
unions of products, and names common union types. It doesn't construct a
monotone `case->' type by computing a cumulative union, nor does it
differentiate between One, Byte, Index, Fixnum, and Integer. Sam or
Vincent could do those two things better than I can. (In particular,
platform-independent Index and Fixnum types scare me.)
If you run the program as-is, it'll infer types for `sqrt', print them
simplified/compressed, and then dump all the input/output pairs that
caused it to infer Single-Float-Complex -> Float-Complex (error #1
above). If you want it to infer types for `expt', uncomment a
conspicuous line near the end, and be prepared to wait while it runs.
It would be a good idea to use something like this for automated
testing, at least for unary functions. Binary functions take a few
minutes each, to test about 40 million argument pairs.
It would be a bad idea to use the inferred types directly, without human
intervention and tweaking. They're not quite precise enough (no (One ->
One) type for `sqrt', for example), and I'm not fully convinced the
argument values are representative.
They should be pretty close to representative, though, enough to find
more errors in Racket's basic math functions and their types (if any),
to tighten up some of the types, and maybe take some of the load off
Vincent when he goes debugging.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
