[racket-dev] Should I expect this program to typecheck?

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.toronto at gmail.com>
To: "J. Ian Johnson" <ianj at ccs.neu.edu>
Cc: "dev" <dev at 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.toronto at gmail.com>
> To: "<dev at racket-lang.org>" <dev at 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
>