最近我一直在探索 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
是相同的。