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

On 01/04/2013 10:38 AM, Vincent St-Amour wrote:
> At Thu, 03 Jan 2013 21:09:52 -0700,
> Neil Toronto wrote:
>>
>> 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.
>
> Cool!
>
> I can see this being useful to tighten existing types.
>
> If the program could only report cases where the inferred type is more
> precise than existing types, that would be great. Otherwise, having to
> manually look for cases to add to existing types would be very
> labor-intensive. That should be doable by reusing some of the machinery
> from the random tester.

I was going to try that, but I reached a soft limit on my expertise. 
Doing it correctly would require changing the program to use TR's 
internal types and type-manipulation algorithms. For me, that would take 
a while. (Hint, hint. :D) I figured I could be most useful coming up 
with the representative values and a prototype.

> Also, it would be great to extend your program to infer filters, too.
> Types with filters are probably the trickiest to write/get right. Not
> sure how to infer those without getting a lot of noise, though.

Yeah, I'm not sure how to approach that. I can't help but think that to 
get meaningful results, you'd have to know enough about the filters 
you're trying to infer that you'd have already derived them.

>> It doesn't construct a  monotone `case->' type by computing a
>> cumulative union
>
> For unary function types, that's pretty straightforward.
>
> For binary function types and beyond, it gets tricky. [...]

Also, I see that monotone `case->' types are necessary:

#lang typed/racket

(: binary-id (case-> (0 -> 0) (1 -> 1)))
(define (binary-id x) x)

(binary-id (ann 0 (U 0 1)))

Type Checker: No function domains matched in function application:
Domains: One
          Zero
Arguments: (U Zero One)


If this restriction were lifted, the inferred types would be fine as 
they are. (FWIW, the inferred argument types are disjoint.) Would that 
be unreasonable or unsound?

> A solution, which Sam and I discussed some time ago, would be to change
> how typechecking of intersection types works. Instead of looking at the
> cases in order and picking the first one that matches, the typechecker
> could pick all the cases that match, and intersect the return types.
> This could tremendously simplify the types of many numeric operations
> (and potentially speed up typechecking), and would solve the problem
> above.
>
> However, the consequences of that change are not obvious. It's clearly
> backwards-incompatible, but it's unclear which programs such a change
> would break, if any. Maybe it's worth revisiting that idea.

I'm reading "TR could be faster and give tighter return types." What's 
the downside?

Neil ⊥