idris - 创建零长度向量

Question

鉴于向量的这种类型，创建特定类型项目的零长度向量的方法是什么？

data Vect : Nat -> Type -> Type where
  VectNil : Vect 0 ty
  (::) : ty -> Vect size ty -> Vect (S size) ty

VectNil String 和我在 REPL 中尝试的所有变体都失败了。期望 VectNil 像 C# 中通用 List 的默认构造函数那样工作是不正确的吗？

new List<string> (); // creates a zero length List of string

Answer 1

VecNil 是值构造函数，它接受 implicit类型参数。在这里你可以在 REPL 中看到它:

*x> :set showimplicits 
*x> :t VectNil 
 Main.VectNil : {ty : Type} -> Main.Vect 0 ty

Idris 从上下文中推断出这些隐式参数的值。但有时上下文没有足够的信息:

*x> VectNil
(input):Can't infer argument ty to Main.VectNil

您可以使用大括号显式地为隐式参数提供值:

*x> VectNil {ty=String}
Main.VectNil {ty = String} : Main.Vect 0 String

或use the the operator添加类型注释:

*x> the (Vect 0 String) VectNil 
Main.VectNil  : Main.Vect 0 String

在较大的程序中，Idris 能够根据其使用位置推断类型。