依存型の例?

Question

3 つのオブジェクト (グローバル) があるとします。 MemoryStore, 、配列があります MemorySlabCache オブジェクトとそれぞれの MemorySlabCache の配列があります MemorySlab オブジェクト。 ある種の このような：

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab> = []
}

class MemorySlab {
  
}

しかし問題は、これですべてが把握できるわけではないということです。また、それぞれの事実を捉える必要もあります。 MemorySlabCache にはサイズがあり、そのサイズを示すために使用されます。 MemorySlab オブジェクトが含まれています。っていうことは もっと このような：

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab<size>> = []
}

class MemorySlab<size: Integer> {
  
}

次に、キャッシュを作成します。

let 4bytes = new MemorySlabCache(size: 4)
let 8bytes = new MemorySlabCache(size: 8)
...
let 32bytes = new MemorySlabCache(size: 32)
...
store.caches.push(4bytes, 8bytes, ..., 32bytes, ...)

これは「」としてカウントされますか?依存型", 「定義が値に依存する型」?のタイプなので、 Array<MemorySlab<size>> に割り当てられた値に依存します。 size フィールドオン MemorySlabCache. 。そうでない場合、これは何ですか?それが依存型の例となるのは何でしょうか?

Answer 1

したがって、答えはおそらく「はい」です。これは依存型の例です。ただし、このために作成される単純な例の多くには、依存型入力の重要な側面が示されていないという問題があります。

問題の型は任意の値に依存するため、おそらくこの点ではあなたの方が優れています。 MemorySlabCache. 。ただし、決して使用しないでください。 MemorySlabCache 静的に既知の値はありません。したがって、より興味深い例は次のようになります。

let cacheSize = readInteger(stdin)
store.caches.push(new MemorySlabCache(cacheSize))

したがって、ユーザーが実行時にキャッシュ サイズを選択できるようにしますが、キャッシュ サイズは引き続き型に記録され、サイズが静的に不明であっても、型チェッカーはすべての操作がサイズに関して意味があることを静的に保証します。 (これはあなたの例の一種の別の問題です。その中には、追跡されたサイズが後でどのように重要になるかを示すものは何もありません)。

もう少し小さな問題は、整数は依存型を「偽装」するには構造が簡単すぎるため、整数を使用した例では、本物の依存型で実現できる可能性を売りにしてしまうことです。たとえば、いくつかの拡張機能を備えた Haskell は、実際には依存型を持たないにもかかわらず、ランタイム キャッシュ サイズの例に似たものでもエンコードできます。静的に既知の型レベルの整数を使用し、実行時の整数に基づいて静的に型指定された値に適切な値を返す関数を作成できます。ただし、依存型理論に基づいた言語では、通常、型が関数型などの任意の型の値に依存します。これら (およびその他の関連機能) については、「偽装」は現実的には不可能です。