Exemple de types dépendants ?

Question

Disons que vous avez 3 objets, un global MemoryStore, qui possède un éventail de MemorySlabCache objets, et chacun MemorySlabCache a une gamme de MemorySlab objets. Sorte de comme ça:

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

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

class MemorySlab {
  
}

Mais le problème est que cela ne reflète pas tout.Il faut également tenir compte du fait que chaque MemorySlabCache a une taille, qui est utilisée pour indiquer quelle taille le MemorySlab les objets qu'il contient.Alors 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, ...)

Est-ce que cela compte comme un "type dépendant", "un type dont la définition dépend d'une valeur"?Puisque le type de Array<MemorySlab<size>> dépend de la valeur attribuée à size champ sur MemorySlabCache.Si non, qu'est-ce que c'est ?Qu'est-ce qui en ferait un exemple de types dépendants ?

Answer 1

La réponse est donc sans doute « oui », ceci est un exemple de types dépendants.Cependant, le problème avec de nombreux exemples simples créés par les gens 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 de MemorySlabCache sans 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 au moment 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 connue statiquement. (ce qui est un autre problème avec votre exemple ;rien n'y montre en quoi la taille suivie compte par la suite).

Un problème un peu plus mineur est que les entiers sont une structure trop simple pour « simuler » des types dépendants, donc les exemples avec eux finissent par ne pas vendre ce qui pourrait être réalisable avec de véritables types dépendants.Par exemple, Haskell avec certaines extensions peut même encoder quelque chose de similaire à mon exemple de taille de cache d'exécution, même s'il n'a pas vraiment de types dépendants.Vous pouvez avoir des entiers au niveau du type connus statiquement 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 ces éléments (et d'autres fonctionnalités associées), le « truquage » n'est pas vraiment réalisable.