Jaka jest kategoryczna semantyka podtypów?

17

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.

Darius Jahandarie
źródło

Odpowiedzi:

17

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?do:ZAbdo:ZAb

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.

Neel Krishnaswami
źródło
Papier Johna Reynoldsa wygląda świetnie, dzięki! (Słyszałem kiedyś, że Philip Wadler powiedział, że John Reynolds jest o 10 lat wcześniej w badaniach ...) Właściwie to znam Zhaohui Luo, ale to, co od niego przeczytałem, wydawało się przede wszystkim pracować z teoria typów i nie badanie innych kątów.
Darius Jahandarie