依存型の例？

Sep 14 2020

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。そうでない場合、これは何ですか？何が依存型の例になりますか？

回答

4 DanDoel Sep 15 2020 at 00:59

したがって、答えは間違いなく「はい」です。これは依存型の例です。ただし、このために作成される多くの単純な例の問題は、依存型の重要な側面を示していないことです。

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

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

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

もう少し小さな問題は、整数は構造が簡単すぎて依存型を「偽造」できないことです。そのため、整数を使用した例では、本物の依存型で実行可能なものを販売することになります。たとえば、いくつかの拡張機能を備えたHaskellは、実際には依存型がない場合でも、runtime-cache-sizeの例に似たものでもエンコードできます。静的に既知の型レベルの整数を使用して、実行時の整数に基づいて静的に型指定された値に適切な値を返す関数を作成できます。ただし、依存型理論に基づく言語では、通常、型は関数型などの任意の型の値に依存します。これら（およびその他の関連機能）の場合、「偽造」は実際には実行可能ではありません。