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 ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
