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

On Jan 2, 2013, at 2:39 PM, Neil Toronto wrote:

> After you do understand the numeric tower well, you start looking for ways to prove to TR that your code won't explode at runtime. It's not always possible - again because, sometimes, the types aren't as precise as they could be. But sometimes because it's just hard.
> 
> One fine example is `sqrt'. Its types are sensible:
> 
>  > (sqrt (ann 5 Real))
>  - : Number
>  2.23606797749979
> 
>  > (sqrt (ann 5 Nonnegative-Real))
>  - : Real [generalized from Nonnegative-Real]
>  2.23606797749979
> 
> But it's often really hard to prove that something is nonnegative without an explicit cast, assertion, or test, and thus stay within the reals in expressions with roots.


That's precisely the example with which I launched Vincent on the numerical hierarchy paper. I am not saying I can't program with it. I am saying the desire to prove the exact type -- and knowing that you could do even better -- drives me nuts. So I'd rather program in bliss -- plain old Racket :-) 

;; --- 

I have asked Sam and Vincent to write a chapter in the TR guide on how to program well with numerics and TR. I think you are in an even better position than they are. If you have time, could you distill your experience into some lessons for our Guide? That would be absolutely terrific. (You know what they say about busy men who just completed a large task: ask them, and they will say 'yes'.) 

Thanks. -- Matthias