Create a zero length vector

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

Create a zero length vector

1 Answers