#lang typed/racket (: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) -> (U A B)))) (define (vector-first vs) (vector-ref vs 0))
I doubt this will typecheck without more work in the typechecker. The issue is that it should work for a union type of as many vectors as you want. If there was a readable-vector type it would be trivial as subtyping would do all of the real work. As (U (ReadVector A) (ReadVector B)) <: (ReadVector (U A B)). But that cannot be done with real vectors, as they are invariant. On Mon, Aug 6, 2012 at 5:15 PM, Ray Racine <[email protected]> wrote: > > This type checks. Not sure if it is the "same thing" as the original > however. > > (: check-array-indexes (Symbol > (Vectorof Index) > (U (Vectorof Index) (Vectorof Integer)) > -> (Vectorof Index))) > (define (check-array-indexes name ds js) > > (define (raise-index-error) > (error name "expected indexes for shape ~e; given ~e" ds js)) > > (: dims Integer) > (define dims (vector-length ds)) > > (unless (= dims (vector-length js)) (raise-index-error)) > > (: new-js (Vectorof Index)) > (define new-js (make-vector dims 0)) > > (let: loop : (Vectorof Index) ([i : Integer 0]) > (if (< i dims) > (let: ((di : Index (vector-ref ds i)) > (ji : Integer (assert (vector-ref js i) exact-integer?))) > (if (and (<= 0 ji) > (< ji di)) > (begin > (vector-set! new-js i (assert ji index?)) > (loop (add1 i))) > (raise-index-error))) > new-js))) > > On Mon, Aug 6, 2012 at 5:47 PM, J. Ian Johnson <[email protected]> wrote: >> >> 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). >> -Ian >> ----- Original Message ----- >> From: "Neil Toronto" <[email protected]> >> To: "J. Ian Johnson" <[email protected]> >> Cc: "dev" <[email protected]> >> Sent: Monday, August 6, 2012 5:07:38 PM GMT -05:00 US/Canada Eastern >> Subject: Re: [racket-dev] Should I expect this program to typecheck? >> >> I can't distinguish the elements' types in the simplified example I >> gave. The code I'm actually working on is this: >> >> (: check-array-indexes (Symbol (Vectorof Index) >> (U (Vectorof Index) (Vectorof Integer)) >> -> (Vectorof Index))) >> (define (check-array-indexes name ds js) >> (define (raise-index-error) >> (error name "expected indexes for shape ~e; given ~e" ds js)) >> (define dims (vector-length ds)) >> (unless (= dims (vector-length js)) (raise-index-error)) >> (define: new-js : (Vectorof Index) (make-vector dims 0)) >> (let loop ([#{i : Nonnegative-Fixnum} 0]) >> (cond [(i . < . dims) >> (define di (vector-ref ds i)) >> (define ji (vector-ref js i)) >> (cond [(and (0 . <= . ji) (ji . < . di)) >> (vector-set! new-js i ji) >> (loop (+ i 1))] >> [else (raise-index-error)])] >> [else new-js]))) >> >> I get type errors on every expression involving `ji', because TR has >> determined that it has type `Any'. >> >> I would use a `case->' type, but I have an array transformation function >> that receives an argument with type >> >> ((Vectorof Index) -> (U (Vectorof Integer) (Vectorof Index))) >> >> whose output has to be bounds-checked by `check-array-indexes', and I >> can't apply a function with a case type to an argument with a union type. >> >> The question will of course be moot when TR has something like a `Const' >> type constructor. I'm anticipating that, and changing the user-facing >> array API to receive (U (Vectorof Integer) (Vectorof Index)) for array >> indexes instead of (Listof Integer). (It should eventually be (Const >> (Vectorof Integer)) or similar, which should be covariant.) >> >> So are the type errors an error in TR, or a known limitation? >> >> Neil ⊥ >> >> >> On 08/06/2012 02:25 PM, J. Ian Johnson wrote: >> > How do you determine the difference between the two vector types is the >> > question... >> > -Ian >> > ----- Original Message ----- >> > From: "Neil Toronto" <[email protected]> >> > To: "<[email protected]>" <[email protected]> >> > Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern >> > Subject: [racket-dev] Should I expect this program to typecheck? >> > >> > #lang typed/racket >> > >> > (: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) -> (U A B)))) >> > (define (vector-first vs) >> > (vector-ref vs 0)) >> > >> > >> > I can't think of a reason this shouldn't work, but I may not be taxing >> > my imagination enough to come up with one. >> > >> > Neil ⊥ >> > _________________________ >> > Racket Developers list: >> > http://lists.racket-lang.org/dev >> > >> >> >> _________________________ >> Racket Developers list: >> http://lists.racket-lang.org/dev > > > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev > _________________________ Racket Developers list: http://lists.racket-lang.org/dev
