Esempio di tipi dipendenti?

Question

Supponiamo di avere 3 oggetti, un globale MemoryStore, che ha un array di MemorySlabCacheoggetti e ognuno MemorySlabCacheha un array di MemorySlaboggetti. Un po 'come questo:

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

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

class MemorySlab {
  
}

Ma il fatto è che questo non cattura tutto. Deve anche catturare il fatto che ognuno MemorySlabCacheha una dimensione, che viene utilizzata per dire quale dimensione sono gli MemorySlaboggetti che contiene. Quindi è più simile a 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, ...)

Questo conta come un " tipo dipendente ", "un tipo la cui definizione dipende da un valore" ? Poiché il tipo di Array<MemorySlab<size>>dipende dal valore assegnato al sizecampo su MemorySlabCache. Se no, cos'è questo? Cosa ne farebbe 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 banali della digitazione dipendente.

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

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

Quindi, consenti all'utente di selezionare una dimensione della cache in fase di esecuzione, ma la dimensione della cache è ancora registrata nel tipo e il controllo del tipo assicura staticamente che tutte le operazioni abbiano senso rispetto alla dimensione, anche se la dimensione non è staticamente nota (che è una specie di un altro problema con il tuo esempio; niente in esso mostra come la dimensione tracciata sia importante successivamente).

Un problema un po 'più minore è che gli interi sono una struttura troppo facile per "falsificare" i tipi dipendenti, quindi gli esempi con loro finiscono per vendere ciò che potrebbe essere fattibile con i tipi dipendenti autentici. Ad esempio, Haskell con alcune estensioni può codificare anche qualcosa di simile al mio esempio di dimensioni della cache di runtime, anche se in realtà non ha tipi dipendenti. È possibile disporre di interi a livello di tipo noti staticamente e creare una funzione che restituisca un valore appropriato per un valore tipizzato staticamente basato su un numero intero di runtime. Tuttavia, i linguaggi basati sulla teoria dei tipi dipendenti generalmente lasciano che i tipi dipendono da valori di tipi arbitrari, come i tipi di funzione. Per queste (e altre caratteristiche correlate), il "falso" non è realmente fattibile.