¿Cuál es la semántica categórica del subtipo?

17

A partir de Curry-Howard-Lambek, ha habido una buena trinidad de teorías de tipos, lógicas y categorías. Tengo curiosidad por saber qué semántica categórica obtienes al agregar subtipos (coercitivos) a una teoría de tipos; parece que esto no se ha explorado mucho, si es que lo ha hecho.

En general, agregar un subtipo coercitivo a una teoría de tipos no arruina sus propiedades meta-teóricas, como una fuerte normalización, ¡creo que su semántica categórica debería ser algo de interés real!

Darius Jahandarie
fuente

Respuestas:

17

Semánticamente, una coerción es solo un morfismo c : A B , que se agrega a la interpretación de términos en los puntos apropiados. El problema básico que esto crea es el tema de la coherencia : ¿está garantizado que un término tendrá un significado único, dado que el mismo término puede tener coerciones ocultas en muchos lugares posibles del programa?C:UNsiC:UNsi

Uno de los primeros tratamientos de este tema fue el artículo de 1980 de John Reynolds, Uso de la teoría de categorías para diseñar conversiones implícitas y operadores genéricos , que muestra cómo puede dar una semántica categórica a un sistema de coerción y usarlo para garantizar que sea coherente.

Si está interesado en el subtipo coercitivo para teorías de tipo rico (por ejemplo, dependiente), entonces Zhaohui Luo es el tipo ideal.

Neel Krishnaswami
fuente
El papel de John Reynolds se ve genial, ¡gracias! (Escuché que Philip Wadler dijo una vez que John Reynolds tiende a adelantarse 10 años en investigación ...) De hecho, estoy familiarizado con Zhaohui Luo, pero lo que leí de él parecía estar trabajando principalmente con Teoría de tipos y no explorar los otros ángulos.
Darius Jahandarie