35

私は依存型に不慣れで、2 つの違いについて混乱しています。通常、型は別の型によってパラメーター化され、何らかの値によってインデックス付けされていると言う人がいるようです。しかし、依存型付き言語では、型と用語の間に区別はありませんか? パラメータとインデックスの違いは基本的なものですか? プログラミングと定理証明の両方で意味の違いを示す例を教えてください。

4

2 に答える 2

47

型のファミリーを見ると、それが持つ各引数がパラメーターなのかインデックスなのか疑問に思うかもしれません。

パラメーターは、その型がある程度汎用的であることを示すだけであり、指定された引数に関してパラメーター的に動作します。

これが意味するのは、たとえば、 、 、 などのどれを考慮しても、型は同じ形状を持つList Tということです。Tnilcons t0 nilcons t1 (cons t2 nil)Tt0t1t2

一方、インデックスは、そのタイプで見つけることができる住民に影響を与える可能性があります! そのため、型のファミリにインデックスを付けると言います。つまり、各インデックスは、(型のファミリ内の) どの型を見ているかを示します (その意味で、パラメーターは、すべてのインデックスが指す縮退したケースです)。同じ「形状」のセットに)。

たとえば、タイプ ファミリFin nまたはサイズの有限集合にはn、選択した に応じて非常に異なる構造が含まれますn。

インデックス0は空のセットにインデックスを付けます。インデックス1は、1 つの要素を持つセットにインデックスを付けます。

その意味で、インデックスの値の知識は重要な情報を運ぶ可能性があります! 通常、インデックスを確認することで、使用されているコンストラクターと使用されていないコンストラクターを知ることができます。これが依存型言語でのパターン マッチングが実行不可能なパターンを排除し、パターンのトリガーから情報を抽出する方法です。

これが、インダクティブ ファミリを定義するときに、通常、型全体のパラメーターを定義できるのに、コンストラクターごとにインデックスを指定する必要がある理由です (コンストラクターごとに、それが存在するインデックスを指定できるため)。

たとえば、次のように定義できます。

F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0

ここで、Tはパラメーターで、0と1はインデックスです。xあなたがタイプのいくつかを受け取ったとき、それF T nが何でTあるかを見ても、それについて何も明らかになりませんx。しかし、見ると次のnことがわかります。

  • そうでxなければならない、C1またはC3いつnですか0
  • それはいつに違いxないC2n1
  • そうでxなければ矛盾から偽造されたに違いない

同様に、yの 型を受け取った場合、とF T 0に対するパターン マッチのみが必要であることがわかります。C1C3

于 2014-07-06T23:27:36.717 に答える
1

以下は、何らかの値によってパラメーター化された型の例です。

open import Data.Nat

infixr 4 _∷_

data ≤List (n : ℕ) : Set where
  []  : ≤List n
  _∷_ : {m : ℕ} -> m ≤ n -> ≤List n -> ≤List n

1≤3 : 1 ≤ 3
1≤3 = s≤s z≤n

3≤3 : 3 ≤ 3
3≤3 = s≤s (s≤s (s≤s z≤n))

example : ≤List 3
example = 3≤3 ∷ 1≤3 ∷ []

これは、すべての要素が以下のリストの一種ですn。一般的な直感は次のとおりです。型のすべての居住者に対して何らかのプロパティが保持される場合、それをパラメーターに抽象化できます。機械的な規則もあります。これは * からの引用です。ぜひお読みください。

于 2014-07-06T23:25:20.450 に答える