Beispiel für abhängige Typen?

Question

Angenommen, Sie haben 3 Objekte, ein globales Objekt MemoryStoremit einem Array von MemorySlabCacheObjekten und jedes MemorySlabCachemit einem Array von MemorySlabObjekten. So ähnlich:

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

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

class MemorySlab {
  
}

Aber die Sache ist, das erfasst nicht alles. Es muss auch die Tatsache erfasst werden, dass jedes MemorySlabCacheeine Größe hat, anhand derer MemorySlabfestgestellt wird, welche Größe die Objekte enthalten. Also ist es eher so:

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 der Typ des Array<MemorySlab<size>>abhängig von dem dem sizeFeld zugewiesenen Wert ist 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 Menschen dafür erstellen, ist jedoch, dass sie keine nicht trivialen Aspekte der abhängigen Typisierung demonstrieren.

Ihre ist in dieser Hinsicht wohl besser, da der betreffende Typ von einem beliebigen Wert in abhängt MemorySlabCache. Sie verwenden jedoch niemals a MemorySlabCacheohne einen statisch bekannten Wert. Ein interessanteres Beispiel wäre also:

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

Sie erlauben dem Benutzer also, zur Laufzeit eine Cache-Größe auszuwählen, die Cache-Größe wird jedoch weiterhin im Typ aufgezeichnet, und die Typprüfung stellt statisch sicher, dass alle Vorgänge in Bezug auf die Größe sinnvoll sind, obwohl die Größe statisch nicht bekannt ist (Dies ist ein weiteres Problem in Ihrem Beispiel. Nichts zeigt, wie wichtig die nachverfolgte Größe anschließend ist.)

Ein etwas kleineres Problem ist, dass Ganzzahlen eine zu einfache Struktur sind, um abhängige Typen zu "fälschen", sodass Beispiele mit ihnen unter dem Verkauf dessen liegen, was mit echten abhängigen Typen machbar sein könnte. Zum Beispiel kann Haskell mit einigen Erweiterungen sogar etwas Ähnliches wie mein Beispiel für die Laufzeit-Cache-Größe codieren, obwohl es nicht wirklich abhängige Typen hat. 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. Bei Sprachen, die auf der Theorie abhängiger Typen basieren, können Typen jedoch im Allgemeinen von Werten beliebiger Typen wie Funktionstypen abhängen. Für diese (und andere verwandte Funktionen) ist "Fälschung" nicht wirklich machbar.