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

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 с некоторыми расширениями может кодировать даже что-то похожее на мой пример размера кэша времени выполнения, даже если на самом деле он не имеет зависимых типов. Вы можете иметь статически известные целые числа уровня типа и создать функцию, которая возвращает вам соответствующее значение для статически типизированного значения на основе целого числа времени выполнения. Однако языки, основанные на теории зависимых типов, обычно позволяют типам зависеть от значений произвольных типов, таких как типы функций. Для этих (и других связанных функций) «подделка» практически невозможна.