Was ist die kategoriale Semantik der Subtypisierung?

Ausgehend von Curry-Howard-Lambek gab es eine schöne Anzahl von Typentheorien, -logiken und -kategorien. Ich bin gespannt, welche kategoriale Semantik Sie erhalten, wenn Sie einer Typentheorie (Zwangs-) Untertypen hinzufügen - es scheint, dass dies, wenn überhaupt, nicht sehr viel untersucht wurde.

Im Allgemeinen ruiniert das Hinzufügen von Zwangssubtypisierung zu einer Typentheorie nicht ihre meta-theoretischen Eigenschaften wie starke Normalisierung, weshalb die kategoriale Semantik meines Erachtens von tatsächlichem Interesse sein sollte!

Semantisch ist ein Zwang nur ein Morphismus c : A → B , der an den entsprechenden Stellen zur Interpretation der Terme hinzugefügt wird. Das Grundproblem dabei ist die Frage der Kohärenz : Haben Sie die Garantie, dass ein Begriff eine eindeutige Bedeutung hat, da derselbe Begriff möglicherweise an vielen möglichen Stellen im Programm verborgene Nötigungen enthalten kann?$c : A \leq B$$c : A \to B$

Eine der ersten Behandlungen dieser Ausgabe war John Reynolds '1980 erschienene Arbeit, in der unter Verwendung der Kategorietheorie implizite Konvertierungen und generische Operatoren entworfen wurden. Sie zeigt, wie Sie einem System von Nötigungen eine kategoriale Semantik geben und sicherstellen können, dass es kohärent ist.

Wenn Sie an erzwungener Subtypisierung für reiche (z. B. abhängige) Typentheorien interessiert sind, dann ist Zhaohui Luo der richtige Ansprechpartner .