最近我一直在探索 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 类型?
最佳答案
我不确定我的解释是否正确,但进行以下类型检查:
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
相同。
关于dependent-type - 如何在 Idris 中为 Vect 编写正确的类型签名?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45662424/