Exemplo de Dependentes de Tipos?

Question

Digamos que você tem 3 objetos, um global MemoryStore, que tem uma matriz de MemorySlabCache objetos, e cada MemorySlabCache tem uma matriz de MemorySlab os objetos. Tipo de como esta:

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

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

class MemorySlab {
  
}

Mas a coisa é, isso não capturar tudo.Ele também precisa capturar o fato de que cada MemorySlabCache tem um tamanho, que é utilizado para indicar o tamanho do MemorySlab são objetos que ele contém.Por isso é mais como esta:

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

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

class MemorySlab<size: Integer> {
  
}

Em seguida, criamos nossos esconderijos:

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 "dependente do tipo de", "um tipo cuja definição depende de um valor"?Uma vez que o tipo de Array<MemorySlab<size>> é dependente do valor atribuído à size campo MemorySlabCache.Se não, o que é isso?O que gostaria de fazer em um exemplo de dependentes de tipos?

Answer 1

Então, a resposta é provavelmente "sim," este é um exemplo de dependentes de tipos.No entanto, o problema com um monte de exemplos simples que as pessoas criam para isso é que eles não demonstram não-trivial aspectos de dependentes de digitação.

Indiscutivelmente, o seu é melhor, a este respeito, uma vez que o tipo em questão depende de um valor arbitrário em MemorySlabCache.No entanto, você nunca use um MemorySlabCache sem um estaticamente valor conhecido.Portanto, mais um exemplo interessante de como 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 tipo de verificador estaticamente garante que todas as operações fazem sentido com relação ao tamanho, mesmo que o tamanho não é estaticamente conhecido (o que é outro problema com o seu exemplo;nada, ela mostra como as controladas tamanho importa posteriormente).

Um pouco mais menor problema é que os números inteiros são muito fáceis de uma estrutura para 'falso' dependentes de tipos para, então, exemplos com terminam em vender o que pode ser viável com a genuína dependentes de tipos.Por exemplo, Haskell com algumas extensões, pode codificar até mesmo algo semelhante ao meu tempo de execução, tamanho do cache exemplo, apesar de realmente não ter dependentes de tipos.Você pode ter estaticamente tipo conhecido a nível de números inteiros, e criar uma função que retorna um valor apropriado para uma estaticamente tipada valor com base em um tempo de execução de inteiros.No entanto, linguagens baseadas em dependentes do tipo de teoria, geralmente, deixe tipos dependem de valores de tipos arbitrários, como a função de tipos.Para estes (e outros recursos relacionados), 'fingindo' não é realmente viável.