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

At Wed, 02 Jan 2013 12:39:21 -0700,
Neil Toronto wrote:
> > Interesting. My extremely limited experience -- and Shriram's --
> > suggests an eternal struggle with the numerical tower for 'beginners'
> > like myself.
> 
> This is my experience as well.
> 
> One place this bit me pretty early was getting TR to optimize loops over 
> indexes *without using casts or assertions*.

Right, fixnum types are tricky. They don't have many closure properties,
so it's hard to stay within these types.

Because of this, we try to avoid exposing these types to beginners as
much as possible (by, e.g., not having functions in the standard library
require them as arguments). The hope is that only experts that are
trying to either (1) get every bit of performance our of their programs
or (2) enforce strict range properties in their programs actually need
to use these types. For the first use case, OC provides some help (and
better support is on the way).

In your experience, have these types caused you trouble other than when
you went looking for them specifically?

> Unfortunately, (i . fx> . 0) doesn't prove i : Positive-Index, even 
> though it could.

That's a bug.

> This brings me to what I think is the major issue for us n00bs: the 
> types force you to understand the numeric tower really well if you want 
> to use types more precise than `Number'. Before you reach that level of 
> understanding, though, and Typed Racket spits errors at you, it's hard 
> to tell whether it has a legitimate complaint - especially when you 
> don't know whether you should expect, say, (i . fx> . 0) to prove i : 
> Positive-Index.

Were there specific corners of the tower that you found frustrating
(other than fixnum types)?

> 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.

> 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.

I actually see that as a positive: if a property is too hard to prove
using the type system alone, you have the option to use casts,
assertions, or tests to help TR prove what you want [1]. Casts,
assertions and tests give you extra power to prove things that you
couldn't prove otherwise, or to make proofs easier.

As for the difficulty of proving properties, specific types could
probably be improved, but I don't have a general solution. Racket's
numeric tower is complicated, and TR needs to be compatible with it.

Thanks for the feedback!

Vincent


[1] Assertions and tests are usually cheap, but casts are surprisingly
    expensive since they involve contracts. There's probably room for
    improvement there. In the meantime, I'll extend OC to warn you when
    you use casts in hot code.