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
