ベクタークロスプロダクトのタイプミスマッチ

Question

ベクタークロスプロダクトをタイプ/ラケットで行う必要があります。次のコードは、型の注釈なしで#lang racketで正常に動作します。 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) 

私は型注釈を使用してコードを実行し、型の不一致エラーが発生します。 (for/vector ([n len])がエラーをトリガと同様に

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

に見え、私は(for/vector ([{n: Integer} len])のように型注釈を入れてみましたが、それはエラーで終わる：Nで結合していない識別子モジュール。修正するために何が必要ですか？ベクタークロスプロダクトを行うためのより良い方法がいくつかありますか？

Answer 1

最初の問題はVectorTopです。これは型情報がほとんどないので、(Vectorof Number)のようなより正確なものを使うべきです。また、経験則として、Typed Racketのほとんどの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)の型を定義することを検討してください。私はこのプログラムをtrivially (Vector Real Real Real)を使用するように変換することができませんでした。