Idris能否推断出顶级常数类型的指数？

Question

例如,Agda允许我写这个:

open import Data.Vec
open import Data.Nat

myVec : Vec ? _
myVec = 0 ? 1 ? 2 ? 3 ? []

并且myVec将有型Vec ? 4如预期.

但如果我在伊德里斯尝试相同的话:

import Data.Vect

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

我收到来自typechecker的错误消息:

 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

根据评论，伊德里斯的顶级漏洞被普遍量化，而不是通过术语推理来填补。

我相信（但是，最终开发团队中的某个人必须确认/否认）这样做部分是为了鼓励显式类型，从而鼓励类型导向的开发，部分是为了为无关值提供一个很好的语法接口实现如：

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，我相信您可以在顶层 使用 a?而不是 a来将其填充到我的 idris 中。在顶层，仍然是一个被删除的、隐式的、未命名的参数。 https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-in​​ference__