[racket-dev] Inferring numeric function types from representative argument values

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 ⊥