¿Ejemplo de tipos dependientes?

Question

Digamos que tienes 3 objetos, un global MemoryStore, que tiene una serie de MemorySlabCache objetos y cada uno MemorySlabCache tiene una variedad de MemorySlab objetos. Algo así como como esto:

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

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

class MemorySlab {
  
}

Pero la cuestión es que esto no lo captura todo.También debe captar el hecho de que cada MemorySlabCache tiene un tamaño, que se utiliza para saber de qué tamaño MemorySlab objetos que contiene.Entonces es más como esto:

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

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

class MemorySlab<size: Integer> {
  
}

Luego creamos nuestros cachés:

let 4bytes = new MemorySlabCache(size: 4)
let 8bytes = new MemorySlabCache(size: 8)
...
let 32bytes = new MemorySlabCache(size: 32)
...
store.caches.push(4bytes, 8bytes, ..., 32bytes, ...)

¿Esto cuenta como "tipo dependiente", "un tipo cuya definición depende de un valor"?Dado que el tipo de Array<MemorySlab<size>> depende del valor asignado a la size campo en MemorySlabCache.Si no, ¿qué es esto?¿Qué lo convertiría en un ejemplo de tipos dependientes?

Answer 1

Entonces, podría decirse que la respuesta es "sí", este es un ejemplo de tipos dependientes.Sin embargo, el problema con muchos ejemplos simples que la gente crea para esto es que no demuestran aspectos no triviales de la tipificación dependiente.

Podría decirse que el suyo es mejor a este respecto, porque el tipo en cuestión depende de un valor arbitrario en MemorySlabCache.Sin embargo, nunca se utiliza un MemorySlabCache sin un valor estáticamente conocido.Entonces un ejemplo más interesante sería como:

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

Por lo tanto, permite al usuario seleccionar un tamaño de caché en tiempo de ejecución, pero el tamaño de la caché aún se registra en el tipo, y el verificador de tipos garantiza estáticamente que todas las operaciones tengan sentido con respecto al tamaño, aunque el tamaño no se conozca estáticamente. (que es otro problema con su ejemplo;nada en él muestra cómo el tamaño rastreado importa posteriormente).

Un problema algo menor es que los números enteros son una estructura demasiado fácil para "falsificar" tipos dependientes, por lo que los ejemplos con ellos terminan vendiendo menos de lo que podría ser factible con tipos dependientes genuinos.Por ejemplo, Haskell con algunas extensiones puede codificar incluso algo similar a mi ejemplo de tamaño de caché en tiempo de ejecución, aunque en realidad no tiene tipos dependientes.Puede tener enteros de nivel de tipo conocidos estáticamente y crear una función que le devuelva un valor apropiado para un valor escrito estáticamente basado en un entero de tiempo de ejecución.Sin embargo, los lenguajes basados ​​en la teoría de tipos dependientes generalmente permiten que los tipos dependan de valores de tipos arbitrarios, como los tipos de funciones.Para estas (y otras características relacionadas), "falsificar" no es realmente factible.