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

Just to be clear.  The below does work in TR and idx is of type Index.
However when one embeds the (in-range 3 5)  directly in the for/vector idx
is not of type Index.  No reason why it shouldn't however.

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

(define: s : (Sequenceof Index) (in-range 3 5))

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


On Wed, Feb 27, 2013 at 4:34 PM, Ray Racine <ray.racine at gmail.com> wrote:

> 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/9d1fb107/attachment.html>