Idris 可以推断顶级常量类型的索引吗? [英] Can Idris infer indices in types of top-level constants?

问题描述

例如，Agda 允许我这样写:

For example, Agda allows me to write this:

open import Data.Vec
open import Data.Nat

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

和 myVec 将按预期具有 Vec ℕ 4 类型.

and myVec will have type Vec ℕ 4 as expected.

但如果我在 Idris 中尝试同样的方法:

But if I try the same in Idris:

import Data.Vect

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

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

I get an error message from the 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

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

Is there a way to define myVec in Idris without manually specifying the index of the Vect?

推荐答案

根据评论，Idris 中的顶级漏洞被普遍量化，而不是通过术语推断来填补.

Per the comments, top-level holes in Idris was universally quantified, instead of being filled via term inference.

我相信(但是，最终开发团队的某个人必须确认/否认)这样做部分是为了鼓励显式类型，因此是类型导向的开发，部分是为了有一个很好的语法，不要-接口实现中的关心值，例如:

I believe (but, ultimately someone from the development team would have to confirm / deny) that this was done partially to encourage explicit types, and thus type-directed development, and partially to have a nice syntax for don't-care values in interface implementations like:

Uninhabited v => Uninhabited (_, v) where
    uninhabited (_, void) = uninhabited void

下划线的这种无关紧要的用法是从它在模式中的使用中采用的，而不是在表达式中的使用.

This don't-care use of the underscore is adopted from it's use in patterns, rather than it's use in expressions.

对于这样的事情(这不完全是您想要的，但它对常量的更改很健壮)，您可以使用显式存在:

For something like this (it's not exactly what you want, but it is robust against changes to the constant), you can use an explicit existential:

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 可能以不同的名称在标准库中，但我没有在快速搜索中找到.

fst and snd might be in the standard library under different names, but I didn't find then in a quick search.

最近一次投票再次引起了我的注意.如果您使用的是 Idris 2，我相信您可以在顶层使用 ? 而不是 _ 来填充我的 idris._ 在顶层，仍然是一个擦除的、隐式的、未命名的参数.https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-in​​ference

An upvote recently drew this answer to my attention again. If you are using Idris 2, I believe you can use a ? instead of a _ at the top level to have it filled in my idris. _ at the top level, is an erased, implicit, unnamed parameter, still. https://idris2.readthedocs.io/en/latest/implementation/overview.html#additional-type-inference

这篇关于Idris 可以推断顶级常量类型的索引吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！