如何在Idris中编写Vect的正确类型签名？

最近我一直在探索Idris中的依赖类型。然而，我克服了一个非常烦人的问题，这是在伊德里斯，我应该用类型签名开始我的程序。所以问题是，如何在Idris中编写简洁的类型签名？如何在Idris中编写Vect的正确类型签名？

例如，

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类型？

来源

2017-08-13 gostriderful

我不知道如果我的解释是正确的，但以下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是否相同。

来源

2017-08-14 08:35:58 Markus

如何在Idris中编写Vect的正确类型签名？

回答

相关问题