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

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20120806/93fb8e73/attachment-0001.html>