2

インデックス付きまたはパラメーター化された型から用語を取得し、その型パラメーターを返すヘルパー関数を作成したいと考えています。

showLen : {len :  ℕ} {A : Set} -> Vec A len -> ℕ
showLen ? = len

showType : {len :  ℕ} {A : Set} -> Vec A len -> Set
showType ? = A

これは可能ですか？(どのようshowType []に問題が発生するかはわかりますが、Type がインデックス化されている場合はどうなりますか?)

4

1 に答える 1

8

暗黙の引数を取り除けば、これを非常に簡単に実装できます。

showLen : (len : ℕ) (A : Set) → Vec A len → ℕ
showLen len _ _ = len

実際、両方を同時に行うことができます。

open import Data.Product

showBoth : (len : ℕ) (A : Set) → Vec A len → ℕ × Set
showBoth len A _ = len , A

現在、暗黙の引数は、コンパイラが独自に埋めようとするという事実を除けば、通常の引数と同じです。必要に応じて、いつでもこの動作をオーバーライドできます。

非表示の引数を持つ関数を実装したい場合、何らかの理由でそれらにアクセスする必要がある場合は、次のように中括弧内で言及することで実現できます。

replicate : {n : ℕ} {A : Set} → A → Vec A n
replicate {zero}  _ = []
replicate {suc _} x = x ∷ replicate x

次に、関数を呼び出して隠し引数を指定する必要がある場合、プロセスは似ています。

vec : Vec ℕ 4
vec = replicate {4} 0

さて、これをshowBoth上記に適用するだけです：

showBoth : {len : ℕ} {A : Set} → Vec A len → ℕ × Set
showBoth {len} {A} _ = len , A

ここで、引数の順序が間違っているとします。たとえば、引数でAはなく引数を明示的に指定したい場合は、次のようnにする必要があります。

vec₂ : Vec ℕ 4
vec₂ = replicate {_} {ℕ} 0

ここで、 n番目の暗黙の引数を入力する必要がある場合、これはすぐに面倒になります。そのため、Agda はそれらを名前で参照するオプションを提供します。

vec₃ : Vec ℕ 4
vec₃ = replicate {A = ℕ} 0

これは、型シグネチャで指定された名前を使用します。関数を定義するときにこれを使用することもできます。

showType : {len : ℕ} {A : Set} → Vec A len → Set
showType {A = Type} _ = Type
于 2013-08-22T22:28:21.663 に答える