在 Idris 中检查向量的类型

Question

从 REPL 中，如何不确保 a 列表确实被解释为向量？

例如，如果我输入：

:t Vect

我得到Vect : Nat -> Type -> Type，如果我输入，这绝对有意义

:t Vect 2

我得到Vect : Type -> Type，这又是绝对有意义的。但我现在试试：

:t Vect 2 [1,2]

并得到一个错误

Can't disambiguate since no name has a suitable type: 
         Prelude.List.::, Prelude.Stream.::, Data.Vect.::

我希望看到的是[1,2] : Vect 2 Int。我做错了什么？在尝试将列表解释为向量时，我在使用函数 the 时也遇到了问题。

有什么建议吗？

Answer 1

the : (a : Type) -> a -> a 接受一个类型和该类型的值并返回该值。因此，如果无法从上下文中推断出目标类型，例如在 REPL 中，您可以使用 the (Vect 2 Int) [1,2] 来指定您对 [1,2] 的含义。

(Vect 2 [1,2] 尝试使用List、Stream 或Vect [1,2] 作为Vect 2 : Type -> Type 中的参数。但与例如Int 不同，列表[1,2] 不是@987654332 @，所以这会给你这个错误。）