Esempio di tipi dipendenti?

Question

Dì che hai 3 oggetti, un MemoryStore globale, che ha una matrice di oggetti MemorySlabCache e ogni MemorySlabCache ha una matrice di oggetti MemorySlab. Ordina di in questo modo:

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

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

class MemorySlab {
  
}

.

Ma la cosa è, questo non cattura tutto.Ha inoltre bisogno di catturare il fatto che ogni MemorySlabCache ha una dimensione, che viene utilizzata per dire quale dimensione gli oggetti MemorySlab sono contiene.Quindi è più come questo:

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

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

class MemorySlab<size: Integer> {
  
}

.

Quindi creiamo le nostre cache:

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

.

conta come un "< tipo dipendente ", "un tipo di cuiLa definizione dipende da un valore "?Poiché il tipo di Array<MemorySlab<size>> dipende dal valore assegnato al campo size su MemorySlabCache.Se no, cos'è questo?Cosa farebbe in un esempio di tipi dipendenti?

Answer 1

Quindi, la risposta è probabilmente "sì", questo è un esempio di tipi dipendenti. Tuttavia, il problema con molti semplici esempi che le persone creano per questo è che non dimostrano aspetti non banale della digitazione dipendente.

Probabilmente il tuo è meglio in questo senso, perché il tipo in questione dipende da un valore arbitrario in MemorySlabCache. Tuttavia, non si utilizza mai un MemorySlabCache senza un valore staticamente noto. Quindi un esempio più interessante sarebbe come:

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

.

Quindi, si consente all'utente di selezionare una dimensione della cache in fase di runtime, ma la dimensione della cache è ancora registrata nel tipo e il tipo di controllo garantisce che tutte le operazioni abbiano senso rispetto alle dimensioni, anche se la dimensione è Non conosciuto staticamente (il che è un altro problema con il tuo esempio; nulla in esso mostra come è importante la dimensione cingolata successivamente).

Un problema un po 'più minore è che i numeri interi sono troppo facili da una struttura per "finto" i tipi dipendenti per, quindi esempi con loro finiscono sotto la vendita di ciò che potrebbe essere fattibile con tipi dipendenti in genuini. Ad esempio, Haskell con alcune estensioni può codificare anche qualcosa di simile al mio esempio di dimensione della cache runtime, anche se non dispone di tipi dipendenti. È possibile avere numeri interi di livello di tipo conosciuti e creare una funzione che restituisce un valore appropriato per un valore digitato staticamente basato su un numero intero di runtime. Tuttavia, le lingue basate sulla teoria dei tipi dipendenti generalmente lasciano i tipi dipendono da valori dei tipi arbitrari, come i tipi di funzione. Per queste (e altre caratteristiche correlate), "faking" non è realmente fattibile.