根据评论,伊德里斯的顶级漏洞被普遍量化,而不是通过术语推理来填补。
我相信(但是,最终开发团队中的某个人必须确认/否认)这样做部分是为了鼓励显式类型,从而鼓励类型导向的开发,部分是为了为无关值提供一个很好的语法接口实现如:
Uninhabited v => Uninhabited (_, v) where
uninhabited (_, void) = uninhabited void
下划线的这种不关心的使用是从它在模式中的使用中采用的,而不是它在表达式中的使用。
对于这样的东西(这不完全是你想要的,但它对常量的改变是鲁棒的),你可以使用显式的存在:
fst : DPair t _ -> t
fst (x ** _) = x
snd : (s : DPair _ p) -> p (fst s)
snd (_ ** prf) = prf
myVecEx : (n ** Vect n Nat)
myVecEx = (_ ** [0, 1, 2, 3])
myVec : Vect (fst myVecEx) Nat
myVec = snd myVecEx
fst
and snd
可能在标准库中以不同的名称存在,但我在快速搜索中没有找到。
编辑:最近的一次投票再次引起了我对这个答案的注意。如果您使用 Idris 2,我相信您可以使用?
代替_
在顶层将其填充到我的 idris 中。_
在顶层,仍然是一个被删除的、隐式的、未命名的参数。https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-inference https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-inference