Create a zero-length vector
Given this type for vectors, how do I create a zero-length vector for a specific type of elements?
data Vect : Nat -> Type -> Type where
VectNil : Vect 0 ty
(::) : ty -> Vect size ty -> Vect (S size) ty
VectNil String and all the options I tried in the REPL failed. Is it wrong to expect VectNil to work the way the default generic list constructor in C # does?
new List<string> (); // creates a zero length List of string
source to share
VecNil
is a value constructor and it takes an implicit parameter . You can see it in the REPL here:
*x> :set showimplicits
*x> :t VectNil
Main.VectNil : {ty : Type} -> Main.Vect 0 ty
Idris passes the values of these implicit parameters from the context. But sometimes the context lacks information:
*x> VectNil
(input):Can't infer argument ty to Main.VectNil
You can explicitly provide a value for an implicit parameter using curly braces:
*x> VectNil {ty=String}
Main.VectNil {ty = String} : Main.Vect 0 String
Or use an operatorthe
to add an annotation like:
*x> the (Vect 0 String) VectNil
Main.VectNil : Main.Vect 0 String
In larger programs, Idris can infer the type based on his site.
source to share