Gdzie badana jest parametryczna relacja w modelach hiperdoktryny lub toposu?

Reynolds pierwotnie zaproponował semantykę relacyjną dla polimorficznego rachunku lambda drugiego rzędu [1]. Później jednak wykazał [2], że to podejście było niespójne z klasyczną teorią zbiorów. Pitts opisał ramy modeli hiperdoktryn i modeli topos [3], które są spójne z logiką konstruktywną.

Następnie opracowano przypuszczalnie relacyjne modele hiperdoktryny i toposu. Gdzie mogę o nich przeczytać?

• [1] Typy, abstrakcja i polimorfizm parametryczny
• [2] Polimorfizm nie jest teoretyczny
• [3] Polimorfizm jest ustawiony teoretycznie, konstruktywnie

• Ze względów technicznych niewiele było pracy nad parametrycznymi modelami toposów. Wewnętrzna logika toposu jest formą teorii mnogości, a indeksowanie impredykatywne w stylu F i aksjomat zestawu mocy są niezgodne. Zobacz nietrywialne typy mocy Andy'ego Pittsa nie mogą być podtypami typów polimorficznych :

  Artykuł ten ustanawia nową, ograniczającą relację między polimorficznym rachunkiem lambda a rodzajem teorii wyższego rzędu, który jest ujęty w logice toposów. Wykazano, że każde osadzenie w toposie kartezjańskiej zamkniętej kategorii (zamkniętych) typów modelu polimorficznego rachunku lambda musi odkładać typy polimorficzne z dala od powertypes, P (X), toposu, w tym sensie że P (X) jest podtypem typu polimorficznego tylko w przypadku, gdy X jest pusty (a zatem P (X) jest końcowy). Jako następstwa uzyskujemy wzmocnienie wyniku Reynoldsa na nieistnieniu set-teoretycznych modeli polimorfizmu.

  W rezultacie, chociaż możesz dać wszechświatowi interpretując typy F w logice toposu, nie możesz pozwolić, aby oddziaływał w interesujący sposób z pełnym wszechświatem zbiorów. Jednak nie wszystko jest stracone!

  1. Fakt, że (nieparametryczny) wszechświat zestawów interpretujących System F oznacza, że ​​możesz podać parametryczny model Systemu F w wewnętrznej logice toposu, o wiele łatwiej niż w zwykłej teorii zbiorów. Zasadniczo, nie musisz grzebać w PER, ponieważ możesz po prostu założyć, że masz odpowiednią kolekcję zestawów. Bob Atkey wykorzystał tę ideę w swoim artykule Relational Parametricity for Higher Kinds , w którym opracował parametryczność dla , pracując w rachunku impredykcyjnym konstrukcji.$F_\omega$

  2. Inną reakcją na wynik Pittsa jest nie praca z teorią zbiorów, ale teorią typów zależnych. Ponieważ w teorii typów zależnych nie ma żadnego typu mocy, nie musisz się martwić interakcją typów mocy i polimorfizmem. Zobacz: Atkey, Ghani i Johann: Relatywnie parametryczny model teorii typów zależnych .

• Jednak nie ma takich przeszkód w budowaniu modeli hiperdoktrynowych, w których pojęcia Systemu F są obiektami logiki. Badania w tym kierunku zapoczątkowali prawdopodobnie Abadi i Plotkin w swoim przełomowym artykule A Logic for Parametric Polymorphism . Lars Birkedal i jego współpracownicy ciężko pracowali nad sformułowaniem modeli kategorialnych dla tej i podobnej logiki - patrz w szczególności Birkedal, Møgelberg i Modele teoretyczne modeli liniowych Abadi i Plotkin Logic z kategorii Petersena , co daje logikę uzasadnienia dla liniowego układu F , plus dowód, że jest solidny i kompletny w odniesieniu do pewnej klasy modeli jakościowych.