向量交叉积中的类型失配

Question

我需要做向量交叉积在类型化/球拍。以下代码在没有类型注释的#lang racket中运行良好。参考文献

#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)

当我运行带有类型注释的代码时，会发生类型不匹配错误。

• 类型检查器:类型错配 预期数:数目 给予:任何in：(参考文献X1)
• 类型检查器:类型错配 预期数:数目 给予:任何in：(参考文献Y2)
• 类型检查器:类型错配 预期数:数目 给予:任何in：(参考文献X2)
• 类型检查器:类型错配 预期数:数目 给予:任何in：(参考文献Y1)
• 类型检查器:摘要:在下列文件中遇到4个错误： (参考文献X1) (参考文献Y2) (参考文献X2) (参考文献Y1)

看起来(for/vector ([n len])触发了错误，我尝试了像(for/vector ([{n: Integer} len])这样的类型注释，但是它最终导致了错误:在n中没有绑定标识符模块。我需要纠正什么？有什么更好的方法来做向量交叉积吗？

Answer 1

第一个问题是VectorTop。这几乎没有提供任何类型信息，所以您应该使用一些更精确的信息，比如(Vectorof Number)。此外，作为一个经验规则，大多数for形式的类型化球拍需要注释。最后，Any也没有提供太多的类型信息，所以您也应该修复ref的类型。

更具体地说，您在当前代码中看到的类型错误是由于ref函数的不准确类型造成的。但是，一旦修复了这个问题，就会遇到上面描述的其他问题。

下面的代码类型检查。

#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)

如果您只想要R^3中向量的交叉积，请考虑硬编码公式，而不是使用for，并为(Vector Real Real Real)定义一个类型。我无法将这个程序转换成使用(Vector Real Real Real)。