Пример зависимых типов?

Question

Допустим, у вас есть 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.Если нет, то что это?Что бы превратить это в пример зависимых типов?

Answer 1

Итак, ответ, возможно, "да", это пример зависимых типов.Однако проблема с большим количеством простых примеров, которые люди создают для этого, заключается в том, что они не демонстрируют нетривиальные аспекты зависимого ввода.

Возможно, ваш вариант лучше в этом отношении, потому что рассматриваемый тип зависит от произвольного значения в MemorySlabCache.Однако вы никогда не используете MemorySlabCache без статически известного значения.Таким образом, более интересным примером было бы что-то вроде:

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

Итак, вы разрешаете пользователю выбирать размер кэша во время выполнения, но размер кэша по-прежнему записывается в тип, а средство проверки типов статически гарантирует, что все операции имеют смысл в отношении размера, даже если размер статически неизвестен (что является своего рода еще одной проблемой в вашем примере;ничто в нем не показывает, какое значение впоследствии имеет отслеживаемый размер).

Несколько более незначительная проблема заключается в том, что целые числа - слишком простая структура для "подделки" зависимых типов, поэтому примеры с ними в конечном итоге недооценивают то, что могло бы быть осуществимо с подлинными зависимыми типами.Например, Haskell с некоторыми расширениями может кодировать даже что-то похожее на мой пример с размером кэша во время выполнения, хотя на самом деле у него нет зависимых типов.Вы можете иметь статически известные целые числа уровня типа и создать функцию, которая возвращает вам соответствующее значение для статически типизированного значения на основе целого числа во время выполнения.Однако языки, основанные на теории зависимых типов, обычно допускают зависимость типов от значений произвольных типов, таких как типы функций.Для этих (и других связанных с ними функций) "подделка" на самом деле неосуществима.