Create a zero length vector

Question

Given this type for vectors, what's the way to create a zero length vector of a particular type of items?

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

VectNil String and all the variations I've tried in the REPL failed. Is it not correct to expect VectNil to work like the default constructor of the generic List in C# does?

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

Answer 1

VecNil is value constructor and it accepts implicit type parameter. Here you can see it in REPL:

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

Idris infers values of those implicit parameters from the context. But sometimes context does not have enough information:

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

You can explicitly provide value for implicit parameter using braces:

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

Or use the the operator to add a type annotation:

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

In larger programs, Idris is able to infer the type based on its use site.