Type mismatch in vector cross product

Question

I need to do vector cross product in typed/racket. The following code works fine in #lang racket without type annotations. reference

#lang typed/racket

(: cross-product (-> VectorTop VectorTop VectorTop))
(define (cross-product X Y)  
  (: len Integer)
  (define len (vector-length X))
  (for/vector ([n len]) 
    (: ref (-> VectorTop Integer Any))   
    (define (ref V i) (vector-ref V (modulo (+ n i) len)))
    (- (* (ref X 1) (ref Y 2)) (* (ref X 2) (ref Y 1)))))

(define X '#(0 1 0))
(define Y '#(0 0 -1))

(cross-product X Y)

When I run the code with type annotations, type mismatch error occurs.

• Type Checker: type mismatch
  expected: Number
  given: Any in: (ref X 1)
  
• Type Checker: type mismatch
  expected: Number
  given: Any in: (ref Y 2)
  
• Type Checker: type mismatch
  expected: Number
  given: Any in: (ref X 2)
  
• Type Checker: type mismatch
  expected: Number
  given: Any in: (ref Y 1)
  
• Type Checker: Summary: 4 errors encountered in:
  (ref X 1)
  (ref Y 2)
  (ref X 2)
  (ref Y 1)
  

It looks like (for/vector ([n len]) triggers the error, I tried putting type annotation like (for/vector ([{n: Integer} len]), but it ends up with the error: unbound identifier module in n. What do I need to correct? Are there some better ways to do vector cross product?

Answer 1

The first problem is with VectorTop. This provides pretty much no type information, so you should be using something more accurate like (Vectorof Number). Also, as a rule of thumb, most for forms in Typed Racket need to be annotated. Finally, Any doesn't provide much type information either, so you should fix the type of ref as well.

More specifically, the type errors you see with your current code are due to the inaccurate type of the ref function. But once you fix that, you'll run into the other issues described above.

The following code type checks.

#lang typed/racket

(: cross-product (-> (Vectorof Number) (Vectorof Number) (Vectorof Number)))
(define (cross-product X Y)
  (define len (vector-length X))
  (for/vector ([n len]) : Number
    (: ref (-> (Vectorof Number) Index Number))   
    (define (ref V i) (vector-ref V (modulo (+ n i) len)))
    (- (* (ref X 1) (ref Y 2)) (* (ref X 2) (ref Y 1)))))

(define X : (Vectorof Number) '#(0 1 0))
(define Y : (Vectorof Number) '#(0 0 -1))

(cross-product X Y)

If you only want the cross product of vectors in R^3, consider hardcoding the formula instead of using a for, and defining a type for (Vector Real Real Real). I was not able to trivially convert this program to use (Vector Real Real Real).