<br><div>This type checks. Not sure if it is the "same thing" as the original however.</div><div><br></div><div>(: check-array-indexes (Symbol </div><div> (Vectorof Index)</div><div> (U (Vectorof Index) (Vectorof Integer))</div> <div> -> (Vectorof Index)))</div><div>(define (check-array-indexes name ds js)</div><div> </div><div> (define (raise-index-error)</div><div> (error name "expected indexes for shape ~e; given ~e" ds js))</div> <div> </div><div> (: dims Integer)</div><div> (define dims (vector-length ds))</div><div> </div><div> (unless (= dims (vector-length js)) (raise-index-error))</div><div> </div><div> (: new-js (Vectorof Index))</div> <div> (define new-js (make-vector dims 0))</div><div> </div><div> (let: loop : (Vectorof Index) ([i : Integer 0])</div><div> (if (< i dims)</div><div> (let: ((di : Index (vector-ref ds i))</div><div> (ji : Integer (assert (vector-ref js i) exact-integer?)))</div> <div> (if (and (<= 0 ji) </div><div> (< ji di))</div><div> (begin</div><div> (vector-set! new-js i (assert ji index?))</div><div> (loop (add1 i)))</div> <div> (raise-index-error)))</div><div> new-js)))</div><div><br></div><div class="gmail_quote">On Mon, Aug 6, 2012 at 5:47 PM, J. Ian Johnson <span dir="ltr"><<a href="mailto:ianj@ccs.neu.edu" target="_blank">ianj@ccs.neu.edu</a>></span> wrote:<br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't get the type Any, rather it doesn't know how to go from the union of vectors to a (vector a) for some a. Vector ref expects a vector, not a union of vectors, and because vectors are invariant, it cannot simplify this to (vector Integer).<br> <div class="im HOEnZb">-Ian<br> ----- Original Message -----<br> From: "Neil Toronto" <<a href="mailto:neil.toronto@gmail.com">neil.toronto@gmail.com</a>><br> </div><div class="HOEnZb"><div class="h5">To: "J. Ian Johnson" <<a href="mailto:ianj@ccs.neu.edu">ianj@ccs.neu.edu</a>><br> Cc: "dev" <<a href="mailto:dev@racket-lang.org">dev@racket-lang.org</a>><br> Sent: Monday, August 6, 2012 5:07:38 PM GMT -05:00 US/Canada Eastern<br> Subject: Re: [racket-dev] Should I expect this program to typecheck?<br> <br> I can't distinguish the elements' types in the simplified example I<br> gave. The code I'm actually working on is this:<br> <br> (: check-array-indexes (Symbol (Vectorof Index)<br> (U (Vectorof Index) (Vectorof Integer))<br> -> (Vectorof Index)))<br> (define (check-array-indexes name ds js)<br> (define (raise-index-error)<br> (error name "expected indexes for shape ~e; given ~e" ds js))<br> (define dims (vector-length ds))<br> (unless (= dims (vector-length js)) (raise-index-error))<br> (define: new-js : (Vectorof Index) (make-vector dims 0))<br> (let loop ([#{i : Nonnegative-Fixnum} 0])<br> (cond [(i . < . dims)<br> (define di (vector-ref ds i))<br> (define ji (vector-ref js i))<br> (cond [(and (0 . <= . ji) (ji . < . di))<br> (vector-set! new-js i ji)<br> (loop (+ i 1))]<br> [else (raise-index-error)])]<br> [else new-js])))<br> <br> I get type errors on every expression involving `ji', because TR has<br> determined that it has type `Any'.<br> <br> I would use a `case->' type, but I have an array transformation function<br> that receives an argument with type<br> <br> ((Vectorof Index) -> (U (Vectorof Integer) (Vectorof Index)))<br> <br> whose output has to be bounds-checked by `check-array-indexes', and I<br> can't apply a function with a case type to an argument with a union type.<br> <br> The question will of course be moot when TR has something like a `Const'<br> type constructor. I'm anticipating that, and changing the user-facing<br> array API to receive (U (Vectorof Integer) (Vectorof Index)) for array<br> indexes instead of (Listof Integer). (It should eventually be (Const<br> (Vectorof Integer)) or similar, which should be covariant.)<br> <br> So are the type errors an error in TR, or a known limitation?<br> <br> Neil ⊥<br> <br> <br> On 08/06/2012 02:25 PM, J. Ian Johnson wrote:<br> > How do you determine the difference between the two vector types is the question...<br> > -Ian<br> > ----- Original Message -----<br> > From: "Neil Toronto" <<a href="mailto:neil.toronto@gmail.com">neil.toronto@gmail.com</a>><br> > To: "<<a href="mailto:dev@racket-lang.org">dev@racket-lang.org</a>>" <<a href="mailto:dev@racket-lang.org">dev@racket-lang.org</a>><br> > Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern<br> > Subject: [racket-dev] Should I expect this program to typecheck?<br> ><br> > #lang typed/racket<br> ><br> > (: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) -> (U A B))))<br> > (define (vector-first vs)<br> > (vector-ref vs 0))<br> ><br> ><br> > I can't think of a reason this shouldn't work, but I may not be taxing<br> > my imagination enough to come up with one.<br> ><br> > Neil ⊥<br> > _________________________<br> > Racket Developers list:<br> > <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a><br> ><br> <br> <br> _________________________<br> Racket Developers list:<br> <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a><br> </div></div></blockquote></div><br>