Les types dépendants vous offrent-ils tout ce que le sous-typage fait?

Les types et langages de programmation se concentrent un peu sur le sous-typage, mais pour autant que je sache, le sous-typage ne semble pas particulièrement fondamental. Le sous-typage vous donne-t-il plus que les types dépendants? Travailler avec des types dépendants est forcément plus de travail, donc je peux comprendre pourquoi les sous-types peuvent être utiles dans la pratique. Cependant, je suis plus intéressé par la théorie des types comme base pour les mathématiques que comme base pour les langages de programmation, dois-je prêter beaucoup d'attention au sous-typage?

Les sous-types et les types dépendants sont des concepts orthogonaux.

Le sous-typage est généralement équipé d'une notion de subsomption, selon laquelle une expression d'un type peut apparaître à l'endroit où un sur-type est attendu.

Le sous-typage est plus susceptible d'être décidable et est plus simple à gérer lors de la mise en œuvre.

La frappe dépendante est beaucoup plus expressive. Mais si jamais vous voulez considérer un groupe comme un monoïde, vous avez besoin d'une notion de subsomption pour oublier la structure supplémentaire. Souvent, comme lors de l'utilisation de Coq, une obligation de preuve triviale est générée pour faire face à ce type de coercition, donc en pratique le sous-typage n'ajoute rien. Ce qui est plus important, c'est d'avoir des façons de regrouper diverses théories pour les rendre réutilisables, comme la réutilisation de la théorie des monoïdes lorsque l'on parle de groupes. Les classes de type dans Coq sont une innovation récente pour faire de telles choses. Les modules sont une approche plus ancienne.

Si vous faites un rapide google des "types dépendants de sous-typage", vous trouverez un tas de travaux ajoutant des sous-types aux types dépendants, principalement vers l'an 2000. J'imagine que la méta-théorie est vraiment difficile, donc aucun sous-typage des types dépendants n'apparaît dans assistants de preuve.

Cependant, je suis plus intéressé par la théorie des types comme base pour les mathématiques que comme base pour les langages de programmation, dois-je prêter beaucoup d'attention au sous-typage?

Une chose supplémentaire que le sous-typage vous donne est que la subsomption implique que de nombreuses propriétés de cohérence sont valables. Une théorie de type dépendante a également besoin d'une notion de non-pertinence de la preuve pour modéliser tout ce que vous pouvez faire avec des sous-types. Par exemple, dans la théorie des types dépendants, vous pouvez approximer la formation d'un sous-ensemble avec un enregistrement dépendant:

$S$$P(x)$$x:$

$X <: Y$$x:X$$x:Y$$P(x)$$P(x)$

Une fois que vous avez cela, vous pouvez systématiquement élaborer le sous-typage en théorie des types dépendants. Voir la thèse de William Lovas pour un exemple d'ajout de sous-typage à une théorie de type dépendante (dans ce cas, Twelf).