[racket] Typed/Racket Runtime Optimized Bounded (Index) Increment Operation

At Mon, 14 May 2012 18:52:33 -0400,
Ray Racine wrote:
> I love seeing all them little green boxes informing me that Typed/Racket
> has elided runtime operation.  Some of my recent code is doing a great deal
> of  processing (Vectorof Float) with vector-ref / vector-set!.
> 
> I'm wondering if there is benefit for some deep in the bowels of the Racket
> runtime optimized Index type increment operation, e.g., (: ++ (Index ->
> Index)).
> 
> (add1 x) is of type Integer -> Integer, which is optimized as a fixnum
> operation.  But it also results in the type contraction from Index to
> Integer.  One can assert the index variable back to an Index type, but this
> is burdensome as one is commonly in some iterative loop with a vector-ref /
> vector-set! calls.  Typed/Racket elides a bounds check, but at the cost of
> my code explicitly re-asserting the validity of the Index type after every
> increment.

The `Index' and `Fixnum' types are not closed under addition. `add1'
can't be given type `(Index -> Index)' because there exists a value of
type `Index' (the highest) whose successor is too big to be an `Index'.
However, the successor should be a `Fixnum', which can still trigger
some optimizations. The situation is the same with `add1' of a `Fixnum'.

We've thought about adding additional sub-`Index' types, but we found
them not to be worth the added complexity to the numeric tower, which in
turn increased typechecking time. Inserting assertions or
fixnum-specific operations (from `racket/fixnum') handle all the cases
that these sub-`Index' types would have handled while keeping the type
system much simpler.

> (let ((v '#(1 2 3)))
>   (let: loop : Void ((idx : Index 0))
>     (display (vector-ref v idx))
>     (loop (assert (add1 idx) Index?))))
> 
> I'm robbing Peter to pay Paul here.  The vector-ref bounds check is elided
> but I'm paying for this pleasure with explicit checks on the index in every
> loop.

You can use Typed Racket's occurrence typing mechanism to avoid it:

    (let* ([v '#(1 2 3)]
           [n (vector-length v)])
      (let: loop : Void ((idx : Nonnegative-Fixnum 0))
        (when (< idx n)
          (display (vector-ref v idx))
          (loop (add1 idx)))))

If the comparison `(< idx n)' returns true, `idx' is smaller than a
value of type `Index' (`n'), and therefore must be an index itself.
Then, when adding one to it, the result is a `Nonnegative-Fixnum', and
we're back where we started. Occurrence typing allows you to use the
checks that are already in your program to refine your types.

> [Aside: Which is more performant?  Eliding the bounds check or avoiding the
> Index? check and using Integer for the indexing variable and letting the
> vector-ref impl bounds check the vector-ref for me.  I'd guess the latter.]

It depends. If the index is of type `Fixnum' (or more precise),
comparisons can be optimized. Benchmarking is the only way to know for
sure.

> I realize there is no free lunch here and somewhere a tax / toll must be
> paid.    So I'm thinking (of limited utility to this special case of
> indexing, but common enough nonetheless) of a dedicated Racket runtime
> operator that optimizes an increment with bounds (Index) check operation.
> Say '++' or 'inc1' of type (Index -> Index) which happily throws a runtime
> exception if the variable overflows the Index type size.

`fx+' from `racket/fixnum' throws an exception if its result is not a
fixnum. There's currently no equivalent for `Index', though.

`Index'es are a Typed Racket concept that we introduced to capture the
fact that certain quantities (vector lengths, for example) are bounded
by something smaller than fixnum size, which allows tricks like the one
above, and in general makes it easier to stay within fixnum range.
Fixnums are what really matter for optimization.

The operation you're suggesting, if implemented at the Typed Racket
level, would not be any faster than doing the `index?' check yourself.
If implemented as a Racket primitive, it could be faster (checking the
bit pattern directly instead of doing a comparison), but I'm not sure
how clean it would be to introduce a Typed Racket concept, `Index'es, at
the Racket level.

I suspect that `fx+' may do all you want. If not, let me know.

> Then the following happens:
> 
> (let ((v '#(1 2 3)))
>   (let: loop : Void ((idx : Index 0))
>     (display (vector-ref v idx))
>     (loop (++ idx))))
> 
> And Typed/Racket will show happy Green Boxes for a runtime optimized Index
> increment and an elided bounds check in the vector-ref.

Another tricky thing about `++': it could not be optimized in this
situation. The correctness of the program depends on `++' returning an
`Index', so the check on its output cannot be elided, otherwise it could
silently return something bigger and violate the type system's
invariants.

`fx+' has the same limitation. You can use it to guarantee and preserve
fixnumness (which may enable optimimzations down the road), but it
usually can't be itself optimized further. It's already faster than `+',
though, so that may be good enough for you.

To summarize, fixnum optimizations are tricky. Performance Report helps
you see what's going on, but it's not as good as it should be at
explaining why things go wrong, and how to fix them, when fixnums are
involved. I'm working on it.

> Since I'm asking .... more ideally I'd like the Racket runtime to offer an
> optimized Ring Algebra on the set of Index type values for the
> multiplication and addition operations.

We've been thinking about adding 32/64-bit modular operations for some
time. However, the interaction with existing range-bounded types like
`Index' and `Fixnum' may not be clean because of the differences in
bounds.

Vincent