Exemplo de tipos dependentes?

Question

Digamos que você tenha 3 objetos, um global MemoryStore, que possui uma matriz de MemorySlabCacheobjetos, e cada MemorySlabCacheum possui uma matriz de MemorySlabobjetos. Mais ou menos assim:

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

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

class MemorySlab {
  
}

Mas o fato é que isso não captura tudo. Ele também precisa capturar o fato de que cada MemorySlabCacheum tem um tamanho, que é usado para informar o tamanho dos MemorySlabobjetos que contém. Então é mais assim:

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

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

class MemorySlab<size: Integer> {
  
}

Em seguida, criamos nossos 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, ...)

Isso conta como um " tipo dependente ", "um tipo cuja definição depende de um valor" ? Visto que o tipo de Array<MemorySlab<size>>depende do valor atribuído ao sizecampo em MemorySlabCache. Se não, o que é isso? O que o tornaria um exemplo de tipos dependentes?

Answer 1

Portanto, a resposta é indiscutivelmente "sim", este é um exemplo de tipos dependentes. No entanto, o problema com muitos exemplos simples que as pessoas criam para isso é que eles não demonstram aspectos não triviais da digitação dependente.

Indiscutivelmente o seu é melhor nesse aspecto, porque o tipo em questão depende de um valor arbitrário em MemorySlabCache. No entanto, você nunca usa um MemorySlabCachesem um valor estaticamente conhecido. Portanto, um exemplo mais interessante seria:

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

Assim, você permite que o usuário selecione um tamanho de cache em tempo de execução, mas o tamanho do cache ainda é registrado no tipo, e o verificador de tipo garante estaticamente que todas as operações façam sentido com relação ao tamanho, mesmo que o tamanho não seja estaticamente conhecido (que é outro tipo de problema com o seu exemplo; nada nele mostra como o tamanho rastreado importa posteriormente).

Um problema um pouco menor é que os inteiros são uma estrutura muito fácil para 'falsificar' tipos dependentes, então exemplos com eles acabam vendendo mal o que poderia ser viável com tipos dependentes genuínos. Por exemplo, Haskell com algumas extensões pode codificar até mesmo algo semelhante ao meu exemplo de tamanho de cache de tempo de execução, embora ele realmente não tenha tipos dependentes. Você pode ter números inteiros de nível de tipo conhecidos estaticamente e criar uma função que retorne um valor apropriado para um valor digitado estaticamente com base em um número inteiro de tempo de execução. No entanto, as linguagens baseadas na teoria dos tipos dependentes geralmente permitem que os tipos dependam de valores de tipos arbitrários, como tipos de função. Para esses (e outros recursos relacionados), 'fingir' não é realmente viável.