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

【问题标题】：How to write correct type signature for Vect in Idris?如何在 Idris 中为 Vect 编写正确的类型签名？
【发布时间】：2017-08-13 16:19:26
【问题描述】：

最近我一直在探索 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

但我是作为 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 类型？

【问题讨论】：

标签： dependent-type idris purely-functional

【解决方案1】：

我不确定我的解释是否正确，但请检查以下类型：

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 不能假设两个ns 确实相同，并且它会抱怨它不知道n1 和n 是否相同的错误消息。

【讨论】：