[racket] Typed Racket - (Sequenceof Index) As Looping Index

The below is just an observation.

Historically in TR I've always struggled with Index vs Fixnum vs Natural
for the vector indexing type when iterating over a vector (or large
sub-ranges or even larger vectors).  Either the Optimizer complains that an
index? check was not elided in a vector-ref OR you end up doing something
along the lines of  (assert (add1 idx) index?) while looping your index
variable passing over the Vector.

But I've just noticed that one can construct TR recognized (Sequenceof
Index).

So in theory, TR + Compiler should be able to elide a number of checks,
such as (assert idx index?), use `unsafe-vector-ref', even elide in loop
bounds checks if the vector is supplied to the 'for'.  This assumes the
(Sequenceof Index) is an efficient generator.  i.e., (in-range 3 10000000)
is not allocating 10000000 somethings. ( I don't know what it "really" is
happening overall, just what I think is possible.  Sufficiently smart
compiler yada yada.)

;;;;;;;;;;;;;;;;
;; Example
;;;;;;;;;;;;;;;;

(: v (Vectorof Symbol))
(define v '#(a b c d e))

;; Efficient!!!
;; s : (Sequenceof Index)
;; See below for 's' construction.
(for/vector: : (Vectorof Symbol)
  ([idx : Index s])
  (vector-ref v idx))

However if one tries to inline the (in-range ...) construction, TR appears
to over-generalized and infers (Sequenceof Positive-Fixnum) in lieu of the
more compiler optimizable specific (Sequenceof Index).

;; Not optimal as idx is not recognized as restricted to type Index.
for/vector: : (Vectorof Symbol)
  ([idx : Index (in-range 3 5)])
  (vector-ref v idx))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Creating a (Sequenceof Index)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#lang typed/racket
(require racket/sequence)

;; Index bounds checking is occurring on construction!!
;; (define: s : (Sequenceof Index) (in-range 3 890235782389053905))
;; stdin::311: Type Checker: Expected (Sequenceof Index), but got
(Sequenceof Nonnegative-Integer)
;;  in: (in-range 3 890235782389053905)
;; ...

(define: s : (Sequenceof Index) (in-range 3 100000000))
(define-values (s-more? s-next?)(sequence-generate s))

;; > more?
;; - : (-> Boolean)
;; #<procedure:sequence-more?>
;; > next?
;; - : (-> Index)
;; #<procedure:sequence-next>

(: v (Vectorof Symbol))
(define v '#(a b c d e))

(when (s-more?)
  (vector-ref v (s-next?))) ;; should be eliding index? check.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130227/30d5fca3/attachment.html>