Beispiel für abhängige Typen?

Question

Angenommen, Sie haben drei Objekte, ein globales MemoryStore, das eine Reihe von hat MemorySlabCache Objekte und jedes MemorySlabCache hat eine Reihe von MemorySlab Objekte. Irgendwie so was:

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

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

class MemorySlab {
  
}

Aber die Sache ist, dass dies nicht alles erfasst.Es muss auch die Tatsache erfasst werden, dass jeder MemorySlabCache hat eine Größe, die verwendet wird, um anzugeben, welche Größe das hat MemorySlab welche Objekte darin enthalten sind.So ist es mehr so was:

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

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

class MemorySlab<size: Integer> {
  
}

Dann erstellen wir unsere Caches:

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

Zählt dies als „abhängiger Typ", „ein Typ, dessen Definition von einem Wert abhängt“?Da die Art der Array<MemorySlab<size>> hängt von dem zugewiesenen Wert ab size Feld an MemorySlabCache.Wenn nicht, was ist das?Was würde es zu einem Beispiel für abhängige Typen machen?

Answer 1

Die Antwort lautet also wohl „Ja“, dies ist ein Beispiel für abhängige Typen.Das Problem bei vielen einfachen Beispielen, die dafür erstellt werden, besteht jedoch darin, dass sie nicht triviale Aspekte der abhängigen Typisierung nicht demonstrieren.

Wahrscheinlich ist Ihres in dieser Hinsicht besser, da der betreffende Typ von einem willkürlichen Wert in abhängt MemorySlabCache.Sie verwenden jedoch niemals a MemorySlabCache ohne einen statisch bekannten Wert.Ein interessanteres Beispiel wäre also:

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

Sie ermöglichen dem Benutzer also, zur Laufzeit eine Cachegröße auszuwählen, die Cachegröße wird jedoch weiterhin im Typ aufgezeichnet, und der Typprüfer stellt statisch sicher, dass alle Vorgänge im Hinblick auf die Größe sinnvoll sind, auch wenn die Größe statisch nicht bekannt ist (was bei Ihrem Beispiel ein weiteres Problem darstellt;nichts darin zeigt, wie wichtig die verfolgte Größe später ist).

Ein etwas kleineres Problem besteht darin, dass Ganzzahlen eine zu einfache Struktur sind, um abhängige Typen zu „fälschen“, sodass Beispiele mit ihnen letztendlich nicht das verkaufen, was mit echten abhängigen Typen machbar sein könnte.Beispielsweise kann Haskell mit einigen Erweiterungen sogar etwas Ähnliches wie in meinem runtime-cache-size-Beispiel codieren, obwohl es nicht wirklich über abhängige Typen verfügt.Sie können statisch bekannte Ganzzahlen auf Typebene haben und eine Funktion erstellen, die Ihnen einen geeigneten Wert für einen statisch typisierten Wert basierend auf einer Laufzeit-Ganzzahl zurückgibt.Sprachen, die auf der Theorie abhängiger Typen basieren, lassen jedoch im Allgemeinen zu, dass Typen von Werten beliebiger Typen, wie z. B. Funktionstypen, abhängen.Für diese (und andere verwandte Merkmale) ist eine „Fälschung“ nicht wirklich machbar.