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 <i...@ccs.neu.edu> 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" <neil.toro...@gmail.com>
> To: "J. Ian Johnson" <i...@ccs.neu.edu>
> Cc: "dev" <dev@racket-lang.org>
> 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" <neil.toro...@gmail.com>
> > To: "<dev@racket-lang.org>" <dev@racket-lang.org>
> > 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
