Comment écrire une signature de type correcte pour Vect dans Idris?

Question

Récemment, j'ai exploré les types dépendants dans Idris. Cependant, je surmonte un problème qui est assez gênant, ce qui est dans Idris, je devrais commencer mon programme avec la signature de type. Donc, le problème est, Comment puis-je écrire une signature de type concis dans Idris?

Par exemple,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String)) 
get_member store idx = Vect.mapMaybe maybe_member (Vect.fromList idx) 
    where 
    maybe_member : (x : Fin n) -> Maybe (Nat, String) 
-- The below line should be type corrected 
-- maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store) 

Si je commente la dernière ligne, la compilation tapera vérifier la fonction ci-dessus, mais si je fais la dernière ligne que l'expression, la compilation se plaindra.

When checking right hand side of VecSort.get_member, maybe_member with expected type 
     Maybe (Nat, String) 
When checking an application of function Data.Vect.index: 
     Type mismatch between 
       Vect n1 String (Type of store) 
     and 
       Vect n String (Expected type) 

     Specifically: 
       Type mismatch between 
         n1 
       and 
         n 

Mais je le fais en fonction lambda,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String)) 
get_member store idx = Vect.mapMaybe (\x => Just (Data.Fin.finToNat x, Vect.index x store)) (Vect.fromList idx) 

il sera de type vérifier aussi bien. Donc la question est, comment dois-je définir le type Vect avec la longueur correcte dans la signature de type?

Answer 1

Je ne sais pas si mon explication est correcte, mais les typable suivants:

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String)) 
get_member store idx {n} = Vect.mapMaybe (maybe_member) (Vect.fromList idx) 
    where 
     maybe_member : (x : Fin n) -> Maybe (Nat, String) 
     maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store) 

La différence est que vous obtenez le paramètre implicite n dans votre champ. Ce {n} et x: Fin x font référence aux mêmes n. Sans tirer le n implicite dans votre portée, idris ne peut pas supposer que les deux n sont en effet les mêmes, et il va se plaindre avec le message d'erreur qu'il ne sait pas si n1 et n sont les mêmes.