Exemple de types dépendants?

Question

Supposons que vous ayez 3 objets, un global MemoryStore, qui a un tableau d' MemorySlabCacheobjets, et chacun MemorySlabCachea un tableau d' MemorySlabobjets. Un peu comme ça:

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

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

class MemorySlab {
  
}

Mais le fait est que cela ne capture pas tout. Il doit également capturer le fait que chacun MemorySlabCachea une taille, qui est utilisée pour indiquer la taille des MemorySlabobjets qu'il contient. Donc c'est plus comme ça:

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

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

class MemorySlab<size: Integer> {
  
}

Ensuite, nous créons nos 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, ...)

Cela compte-t-il comme un " type dépendant ", "un type dont la définition dépend d'une valeur" ? Étant donné que le type de Array<MemorySlab<size>>dépend de la valeur attribuée au sizechamp sur MemorySlabCache. Sinon, qu'est-ce que c'est? Qu'est-ce qui en ferait un exemple de types dépendants?

Answer 1

Donc, la réponse est sans doute «oui», c'est un exemple de types dépendants. Cependant, le problème avec beaucoup d'exemples simples que les gens créent pour cela est qu'ils ne démontrent pas les aspects non triviaux du typage dépendant.

Le vôtre est sans doute meilleur à cet égard, car le type en question dépend d'une valeur arbitraire dans MemorySlabCache. Cependant, vous n'utilisez jamais a MemorySlabCachesans valeur statiquement connue. Un exemple plus intéressant serait donc:

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

Ainsi, vous autorisez l'utilisateur à sélectionner une taille de cache lors de l'exécution, mais la taille du cache est toujours enregistrée dans le type, et le vérificateur de type garantit statiquement que toutes les opérations ont un sens par rapport à la taille, même si la taille n'est pas statiquement connue (ce qui est un autre problème avec votre exemple; rien dans celui-ci ne montre comment la taille suivie est importante par la suite).

Un problème un peu plus mineur est que les entiers sont une structure trop facile pour «faux» les types dépendants, donc les exemples avec eux finissent par vendre ce qui pourrait être faisable avec de véritables types dépendants. Par exemple, Haskell avec certaines extensions peut encoder même quelque chose de similaire à mon exemple de taille de cache à l'exécution, même s'il n'a pas vraiment de types dépendants. Vous pouvez avoir des entiers de niveau de type statiquement connus et créer une fonction qui vous renvoie une valeur appropriée pour une valeur typée statiquement basée sur un entier d'exécution. Cependant, les langages basés sur la théorie des types dépendants laissent généralement les types dépendre de valeurs de types arbitraires, comme les types de fonctions. Pour ceux-ci (et d'autres fonctionnalités connexes), «truquer» n'est pas vraiment possible.