Making nested vectors with build-vector in typed/racket

Questions & Answers
1

I can't seem to get how to get the use of build-vector in the following code to pass the Racket type checker. I've reduced this from an existing untyped function that constructs an "image" as a "vector of vector of color" by reading from a file. Tried "Mutable-Vectorof" to closely match what is stated as "Expected" in the error message, but I get the same error with "Vectorof" instead too. It looks like some kind of limitation with deeper types, but the default language is /deep anyway, so not sure. Any pointers please?

Just copy-pasting the following code into Racket and hitting "Run" should produce the error.

#lang typed/racket

(struct (t) color ([a : t]
                   [r : t]
                   [g : t]
                   [b : t]))

(: mk-image (-> Integer Integer (Mutable-Vectorof (Mutable-Vectorof (color Flonum)))))
(define (mk-image width height)
  (build-vector height
                (λ ([r : Index])
                  (vector (color 0.0 0.0 0.0 0.0)))))
1 Like
2

In particular, the error on the second argument says -

Argument 2:
  Expected: (-> Index a)
  Given:    (-> Index (Mutable-Vector (color Flonum-Positive-Zero)))

It appears that the (Mutable-Vector...) part ought to match with the "a" type variable, but the checker complains. And similarly for the result vector -

Result type:     (Mutable-Vectorof a)
Expected result: (Mutable-Vectorof (Mutable-Vectorof #(struct:color (Flonum Flonum Flonum Flonum))))

Again, a ought to have matched against (Mutable-Vectorof #(struct:color (Flonum Flonum Flonum Flonum)))) which is the same as (Mutable-Vectorof (color Flonum)) but it doesn't seem to.

3

I noticed something after posting the previous reply :smiley: -

Adding the following return type annotation to the λ results in passing the type checker.

 : (Mutable-Vectorof (color Flonum))

So (Mutable-Vectorof (color Flonum)) doesn't match against the inferred (Mutable-Vector (color Flonum)). ... which also seems weird. However, I actually have a function that produces a Mutable-Vectorof in my main code.

4

Using inst with build-vector is another way of telling TR what the correct type should be:

(: mk-image (-> Integer Integer (Mutable-Vectorof (Mutable-Vectorof (color Flonum)))))
(define (mk-image width height)
  ((inst build-vector (Mutable-Vectorof (color Flonum)))
   height
   (λ ([r : Index])
     (vector (color 0.0 0.0 0.0 0.0)))))

build-vector is a parameterized type

> (:print-type build-vector)
(All (a) (-> Integer (-> Index a) (Mutable-Vectorof a)))

and inst is used to bind a to a concrete type so TR doesn't have to try to infer what it is (I've found its type inference leaves something to be desired compared to the Hindley-Milner systems I'm used to.)

5

Hah! Thanks. Yeah that works and "new" trick learnt. It sure feels like there are gaps. Here, for example, (Mutable-Vector x) should be able to match against (Mutable-Vectorof x).