名前付きV無名のデータ型の引数は<a href="https://www.manning.com/books/type-driven-development-with-idris" rel="nofollow">Type Driven Development with Idris</a>の6章からのコードで

Question

は、私はこのコードで困惑した非常に少なくする必要があるで

data DataStore : Type -> Type where 
    MkData : (size : Nat) -> 
      (items : Vect size schema) -> 
      DataStore schema 

私はschemaは未定義ているように見えるので、それがコンパイルされないかもしれないと思いましたか、どうにかして最初のパラメータDataStoreに結びついてください。しかし、それが正常にロードし、そのように使用することができます。

*DataStore> the (DataStore String) $ MkData 2 ["Fred", "Wilma"] 
MkData 2 ["Fred", "Wilma"] : DataStore String 

私はDataStoreへの最初の引数はそうのようschema命名される必要があるであろうことを考えた：

data DataStore : (schema : Type) -> Type where 
    MkData : (size : Nat) -> 
      (items : Vect size schema) -> 
      DataStore schema 

この定義にも同様に使用することができます最初のもの。

私は、2つの定義の間に意味の違いがあり、誰かが私の間違った直感で私を助けることができるかどうか疑問に思っています。schemaは定義されていません。

Answer 1

ここでは2つのことが起こっています。最初は暗黙の引数です。関数の引数として使用される小文字の名前は、常に暗黙の引数に変換されます。例えば、関数合成演算子：

Idris> :t (.) 
(.) : (b -> c) -> (a -> b) -> a -> c 
Idris> :set showimplicits 
Idris> :t (.) 
Prelude.Basics.(.) : {c : Type} -> {a : Type} -> {b : Type} -> (b -> c) -> (a -> b) -> a -> c 

はCOMPOSEのタイプはそのタイプシグネチャ内の任意の場所で宣言されていない変数A、B、およびCを含みます。 Idrisはそれらを暗黙的な引数にします。これらの引数は全て統一によって推論しようとするタイプTypeです。 {curly brackets}は、暗黙的な引数を明示的に指定する構文です。あなたはいつもインタプリタの中で:set showimplicitsを見ることができます。 DataStoreの例では、schemaは暗黙の変数です。あなたがそれらを持っている関数を呼び出すとき

また、暗黙に指定することができます。

二つ目は data宣言で型コンストラクタのタイプの変数は、その型以外のものの上にスコープしないことである

λΠ> MkData {schema = String} 2 ["hi", "Steven"] 
MkData 2 ["hi", "Steven"] : DataStore String 

コンストラクタ。 DataStore : (schema : Type) -> Typeの "schema"がMkDataのタイプシグニチャのスコープに含まれていないため、DataStoreの2番目の定義は元のものとまったく同じです。