Erstellen Sie eine Null Länge Vektor

Question

Angesichts dieser Art für Vektoren, was ist die Möglichkeit, eine Null Länge Vektor einer bestimmten Art von Elementen zu erstellen?

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

VectNil String und alle Variationen ich nicht in der REPL ausprobiert habe. Ist es nicht richtig zu erwarten, dass VectNil wie der Standardkonstruktor der generischen Liste in C# funktioniert?

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

Answer 1

VecNil ist Wert Konstruktor und akzeptiert implicit Typparameter. Hier können Sie es in REPL sehen:

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

Idris leitet Werte dieser impliziten Parameter aus dem Kontext. Aber manchmal Kontext nicht genügend Informationen:

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

Sie können explizit Wert für implizite Parameter mit Klammern bieten:

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

Oder use the the operator eine Art Anmerkung hinzuzufügen:

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

In Bei größeren Programmen ist Idris in der Lage, den Typ anhand seiner Verwendungsstelle abzuleiten.