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!.<br><br>I&#39;m wondering if there is benefit for some deep in the bowels of the Racket runtime optimized Index type increment operation, e.g., (: ++ (Index -&gt; Index)).  <br>
<br>(add1 x) is of type Integer -&gt; 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.<br>
<br>(let ((v &#39;#(1 2 3)))<br>  (let: loop : Void ((idx : Index 0))<br>    (display (vector-ref v idx))<br>    (loop (assert (add1 idx) Index?))))<br><br>I&#39;m robbing Peter to pay Paul here.  The vector-ref bounds check is elided but I&#39;m paying for this pleasure with explicit checks on the index in every loop. <br>
<br>[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&#39;d guess the latter.]<br>
<br>I realize there is no free lunch here and somewhere a tax / toll must be paid.    So I&#39;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 &#39;++&#39; or &#39;inc1&#39; of type (Index -&gt; Index) which happily throws a runtime exception if the variable overflows the Index type size.<br>
<br>Then the following happens:<br><br>(let ((v &#39;#(1 2 3)))<br>
  (let: loop : Void ((idx : Index 0))<br>
    (display (vector-ref v idx))<br>
    (loop (++ idx))))<br><br>And Typed/Racket will show happy Green Boxes for a runtime optimized Index increment and an elided bounds check in the vector-ref.<br><br>Obviously this not a super critical thing.   I don&#39;t know if it involves a couple of bit-mask operations in the runtime or involves rewriting the entire numeric tower.<br>
<br>Since I&#39;m asking .... more ideally I&#39;d like the Racket runtime to offer an optimized Ring Algebra on the set of Index type values for the multiplication and addition operations.<br><br>