IdrisのVectに正しい型の署名を書くには？

Question

最近、私はIdrisの依存型を調べています。しかし、私は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 

しかし、私はラムダ関数としてそれを行う、

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が同じであることを知らないというエラーメッセージが表示されます。