Quelle est la sémantique catégorielle du sous-typage?

À partir de Curry-Howard-Lambek, il y a eu une belle trinité de théories de types, de logiques et de catégories. Je suis curieux de savoir quelle sémantique catégorique vous obtenez lorsque vous ajoutez un sous-typage (coercitif) à une théorie des types - il semble que cela n'ait pas été beaucoup exploré, voire pas du tout.

En général, l'ajout de sous-typage coercitif à une théorie des types ne ruine pas ses propriétés méta-théoriques telles qu'une forte normalisation, donc sa sémantique catégorique devrait être quelque chose d'intéressant, je pense!

Sémantiquement, une coercition n'est qu'un morphisme c : A → B , qui s'ajoute à l'interprétation des termes aux points appropriés. Le problème fondamental que cela crée est la question de la cohérence : avez-vous la garantie qu'un terme aura un sens unique, étant donné que le même terme peut potentiellement avoir des contraintes cachées dans de nombreux endroits possibles du programme?$c : A \leq B$$c : A \to B$

L'un des premiers traitements de ce problème a été l'article de John Reynolds de 1980, Using Category Theory to Design Implicit Conversions and Generic Operators , qui montre comment vous pouvez donner une sémantique catégorique à un système de coercitions et l'utiliser pour vous assurer qu'il est cohérent.

Si vous êtes intéressé par le sous-typage coercitif pour les théories de type riche (par exemple, dépendant), alors Zhaohui Luo est le go-to guy.