Search code examples
idris

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
Solution

  • 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.