type-inference - Idris 可以推断顶级常量类型的索引吗？

Question

例如，Agda 允许我这样写:

open import Data.Vec
open import Data.Nat

myVec : Vec ℕ _
myVec = 0 ∷ 1 ∷ 2 ∷ 3 ∷ []

和 myVec将有类型 Vec ℕ 4正如预期的那样。

但是，如果我在 Idris 中尝试相同的操作:

import Data.Vect

myVec : Vect _ Nat
myVec = [0, 1, 2, 3]

我从类型检查器收到一条错误消息:

 When checking right hand side of myVec with expected type
         Vect len Nat

 Type mismatch between
         Vect 4 Nat (Type of [0, 1, 2, 3])
 and
         Vect len Nat (Expected type)

 Specifically:
         Type mismatch between
                 4
         and
                 len

有没有办法定义 myVec在 Idris 中，无需手动指定 Vect 的索引?

Answer 1

根据评论，Idris 中的顶级漏洞被普遍量化，而不是通过术语推断来填补。
我相信(但最终，开发团队中的某个人将不得不确认/否认)这样做部分是为了鼓励显式类型，因此是类型导向的开发，部分是为了对 don't-care 值有一个很好的语法接口(interface)实现如:

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和 snd可能在不同名称的标准库中，但我没有在快速搜索中找到。
编辑:最近一次投票再次引起了我的注意。如果您使用的是 Idris 2，我相信您可以使用 ?而不是 _在顶层将其填充到我的 idris 中。 _在顶层，仍然是一个已删除的、隐含的、未命名的参数。 https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-inference