長さゼロのベクトルを作成する

Question

ベクトルの場合、特定のタイプのアイテムの長さゼロベクトルを作成する方法は何ですか？

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

VectNil文字列と私はREPLで試したすべてのバリエーションに失敗しました。 期待通りではありませんVectNilは、C＃のジェネリックリストのデフォルトコンストラクタのように機能しますか？

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

Answer 1

VecNil値コンストラクタであり、implicit型パラメータを受け付けます。ここではREPLでそれを見ることができます：

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

Idrisはコンテキストからの暗黙のパラメータの値を推測します。しかし、時にはコンテキストは、十分な情報を持っていませんで

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

：型注釈を追加する

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

またはuse the the operator：

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

あなたは明示的に括弧を使用して、暗黙のパラメータの値を提供することができますより大きなプログラムでは、Idrisはその使用サイトに基づいてタイプを推論することができます。