Incompatibilité de type produit vectoriel croisé

Question

J'ai besoin de faire un produit vectoriel croisé en typé/raquette. Le code suivant fonctionne correctement dans #lang racket sans annotations de type. 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) 

Quand je lance le code avec des annotations de type, erreur d'incompatibilité de type se produit.

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

Il ressemble à (for/vector ([n len]) déclenche l'erreur, j'ai essayé de mettre l'annotation de type comme (for/vector ([{n: Integer} len]), mais il se termine avec l'erreur: le module d'identification non liée n. De quoi ai-je besoin pour corriger? Existe-t-il de meilleurs moyens de faire des produits vectoriels croisés?

Answer 1

Le premier problème est avec VectorTop. Cela fournit à peu près aucune information de type, donc vous devriez utiliser quelque chose de plus précis comme (Vectorof Number). En outre, en règle générale, la plupart des formulaires for dans Raquette typée doivent être annotés. Enfin, Any ne fournit pas non plus beaucoup d'informations de type, donc vous devriez aussi corriger le type de ref. Plus précisément, les erreurs de type que vous voyez avec votre code actuel sont dues au type inexact de la fonction ref. Mais une fois que vous aurez résolu cela, vous rencontrerez les autres problèmes décrits ci-dessus.

Les vérifications de type de code suivantes.

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

Si vous souhaitez que le produit croisé de vecteurs dans R^3, considèrent la formule hardcoding au lieu d'utiliser un for, et la définition d'un type pour (Vector Real Real Real). Je ne pouvais pas convertir trivialement ce programme pour utiliser (Vector Real Real Real).