如何在Idris中編寫Vect的正確類型簽名？

Question

最近我一直在探索Idris中的依賴類型。然而，我克服了一個非常煩人的問題，這是在伊德里斯，我應該用類型簽名開始我的程序。所以問題是，如何在Idris中編寫簡潔的類型簽名？

例如，

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) 

如果我評論的最後一行，編譯將鍵入檢查上述功能， 但如果我做的最後行表達，編譯會報錯。

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 

但我這樣做是爲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) 

這將是類型檢查爲好。

所以問題是，我應該如何定義類型簽名中正確長度的Vect類型？

Answer 1

我不知道如果我的解釋是正確的，但以下typechecks：

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) 

不同的是，你進入你的範圍的隱含參數n。這{n}和x: Fin x都提到相同的n。如果不在您的範圍內拉取隱含的n，idris不能假定兩個n確實是相同的，並且它會抱怨錯誤消息，它不知道n1和n是否相同。