[racket-dev] Five feature/limitation interactions conspire to drive mad

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Wed Jan 2 22:20:15 EST 2013

On Jan 2, 2013, at 4:51 PM, Vincent St-Amour wrote:

>> It would be really handy if TR could give counterexamples in these 
>> cases. "This is how you can end up with an exact zero by multiplying an 
>> exact rational and a flonum: (* 0 1.0)."
> Since most TR optimization failures can be traced back to a failure to
> typecheck at an optimizable type, Optimization Coach should be able to
> help you here. It doesn't currently provide counter-examples, but I'll
> look into it.
> However, OC requires a program that typechecks, so it doesn't always
> apply. Perhaps applying optimization coaching techniques (especially
> proximity) to type error messages would work. Worth a try.

Absolutely worth a try. I doubt anyone else has done type checking with counter-example generation. -- Matthias

Posted on the dev mailing list.