¿Ejemplo de tipos dependientes?

Question

Supongamos que tiene 3 objetos, uno global MemoryStore, que tiene una matriz de MemorySlabCacheobjetos, y cada uno MemorySlabCachetiene una matriz de MemorySlabobjetos. Algo así:

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

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

class MemorySlab {
  
}

Pero la cosa es que esto no captura todo. También necesita capturar el hecho de que cada uno MemorySlabCachetiene un tamaño, que se utiliza para indicar el tamaño de los MemorySlabobjetos que contiene. Entonces es más así:

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, ...)

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

Answer 1

Entonces, la respuesta es posiblemente "sí", este es un ejemplo de tipos dependientes. Sin embargo, el problema con muchos ejemplos simples que las personas crean para esto es que no demuestran aspectos no triviales de la escritura dependiente.

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

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

Por lo tanto, permite que el usuario seleccione un tamaño de caché en tiempo de ejecución, pero el tamaño de caché aún se registra en el tipo, y el verificador de tipo asegura estáticamente que todas las operaciones tienen sentido con respecto al tamaño, aunque el tamaño no se conoce estáticamente. (que es otro problema con su ejemplo; nada en él muestra cómo importa el tamaño de seguimiento 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 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 realmente 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.