Jaka jest kategoryczna semantyka podtypów?

Począwszy od Curry-Howarda-Lambka, pojawiła się niezła trójca typów teorii, logiki i kategorii. Jestem ciekawy, jaką semantyczną kategorię uzyskujesz, gdy dodajesz (przymus) podtyp do teorii typów - wygląda na to, że nie zostało to zbytnio zbadane, jeśli w ogóle.

Ogólnie rzecz biorąc, dodanie przymusowego podtypu do teorii typów nie rujnuje jego metaoretycznych właściwości, takich jak silna normalizacja, więc jego kategoryczna semantyka powinna być czymś, co powinno być przedmiotem zainteresowania.

Semantycznie przymus jest tylko morfizmem , który dodaje się do interpretacji terminów w odpowiednich punktach. Podstawowym problemem, jaki to stwarza, jest kwestia spójności : czy masz gwarancję, że termin będzie miał unikalne znaczenie, biorąc pod uwagę, że ten sam termin może potencjalnie mieć koercje ukryte w wielu możliwych miejscach w programie?$c : A \leq B$$c : A \to B$

Jednym z pierwszych sposobów podejścia do tego problemu był artykuł Johna Reynoldsa z 1980 r., „ Wykorzystanie teorii kategorii do projektowania niejawnych konwersji i operatorów ogólnych” , który pokazuje, w jaki sposób można nadać systemowej koercji kategoryczną semantykę i wykorzystać ją, aby zapewnić jej spójność.

Jeśli jesteś zainteresowany przymusowym subtypingiem dla bogatych (np. Zależnych) teorii typu, to Zhaohui Luo jest facetem na pierwszym miejscu.