Какова категориальная семантика подтипов?

Начиная с Curry-Howard-Lambek, было триединство теорий типов, логик и категорий. Мне любопытно, какую категоричную семантику вы получаете, когда добавляете (принудительный) подтип в теорию типов - кажется, что это не очень изучалось, если вообще.

В целом, добавление коэрцитивного подтипирования в теорию типов не разрушает ее мета-теоретические свойства, такие как сильная нормализация, поэтому я считаю, что ее категориальная семантика должна представлять реальный интерес!

Семантически, принуждение - это просто морфизм , который добавляется к интерпретации терминов в соответствующих точках. Основной проблемой, которую это создает, является проблема согласованности : гарантируется ли вам, что термин будет иметь уникальное значение, учитывая, что в этом же термине могут быть принудительные скрытые действия во многих возможных местах программы?$c : A \leq B$$c : A \to B$

Одним из первых способов решения этой проблемы была статья Джона Рейнольдса 1980 года « Использование теории категорий для проектирования неявных преобразований и универсальных операторов» , в которой показано, как можно дать категориальную семантику системе приведения и использовать ее для обеспечения ее согласованности.

Если вы заинтересованы в принудительном подтипировании для теорий богатых (например, зависимых) типов, то Чжаохуэй Ло - самый подходящий парень.