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

On 01/02/2013 02:51 PM, Vincent St-Amour wrote:
> At Wed, 02 Jan 2013 12:39:21 -0700,
> Neil Toronto wrote:
>> 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?

Not that I recall. If I stick to union types like Integer, 
Exact-Rational, Flonum, Real, and Number, they don't often show up. I 
expect generalization and covariance have a lot to do with it.

Of course, these types caused me trouble immediately because I went 
looking for them immediately, to get optimizations. It's a happy 
accident that always using Index for bounds and bounds-checked values 
works out so well. (Unless you planned it?)

>> 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)?

Mostly `sqrt' and `log', when it's hard to prove their arguments are 
nonnegative. I've gotten around it using `flsqrt' and `fllog'. I was 
usually working with flonums anyway.

One that has bugged me recently is that TR can't prove (* x (conjugate 
x)) : Nonnegative-Real. I have no idea how you'd do it without turning 
Number into a product type, though.

I almost forgot this one:

   > (/ (ann 5 Nonnegative-Real) (ann 3 Nonnegative-Real))
   - : Real
   1 2/3

If you want more, you can grep for `assert' in the math library.

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

We should differentiate between what *I* can prove and what *Typed 
Racket* can prove. I can usually prove more. For example, *I* know that 
this function preserves types:

   (: x^2n (Real Positive-Integer -> Nonnegative-Real))
   (define (x^2n x n)
     (expt x (* 2 n)))

But TR has no concept of "even, positive integer". (To be clear, I'm not 
advocating adding it.) Frustration happens when I know something, but I 
can't get TR to "know" it.

FWIW, this mismatch doesn't happen very often anymore, probably because 
I know TR's model of the numeric tower a lot better, and because you've 
improved Racket's basic math types a lot.

Neil ⊥