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

17

À 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!

Darius Jahandarie
la source

Réponses:

17

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:UNEBc:UNEB

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.

Neel Krishnaswami
la source
Le papier John Reynolds a fière allure, merci! (J'ai entendu Philip Wadler dire une fois que John Reynolds avait tendance à avoir environ 10 ans d'avance sur la recherche ...) Je connais en fait Zhaohui Luo, mais ce que j'ai lu de lui semble fonctionner principalement avec la théorie des types et ne pas explorer les autres angles.
Darius Jahandarie