[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 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 <ray.racine at gmail.com> 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 <ianj at 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.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
>> >
>>
>>
>> _________________________
>>   Racket Developers list:
>>   http://lists.racket-lang.org/dev
>
>
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev
>