Di mana parametricity relasional dalam model hyperdoctrine atau topos dieksplorasi?

Reynolds awalnya mengusulkan semantik relasional untuk kalkulus lambda polimorfik orde kedua [1]. Namun ia kemudian menunjukkan [2] bahwa pendekatan ini tidak konsisten dengan teori himpunan klasik. Pitts menggambarkan kerangka model hyperdoctrine dan model topos [3] yang konsisten dengan logika konstruktif.

Agaknya hyperdoctrine relasional dan model topos kemudian dikembangkan. Di mana saya bisa membaca tentang mereka?

• [1] Jenis, abstraksi, dan polimorfisme parametrik
• [2] Polimorfisme bukanlah teori set
• [3] Polimorfisme diatur secara teoretis, secara konstruktif

• Untuk alasan teknis, belum ada banyak pekerjaan pada model topos parametrik. Logika internal topos adalah bentuk teori himpunan, dan pengindeksan impredikatif gaya-F dan aksioma powerset tidak kompatibel. Lihat Tipe Kekuatan Non-sepele dari Andy Pitts Tidak Dapat Menjadi Subtipe Jenis Polimorfik :

  Makalah ini membangun hubungan terbatas baru antara kalkulus lambda polimorfik dan jenis teori tipe orde tinggi yang diwujudkan dalam logika toposa. Terlihat bahwa setiap penyisipan dalam topos kategori tertutup cartesian dari tipe (tertutup) dari model kalkulus lambda polimorfik harus menempatkan tipe polimorfik jauh dari powertypes, P (X), dari topos, dalam arti bahwa P (X) adalah subtipe dari tipe polimorfik hanya dalam kasus X kosong (dan karenanya P (X) adalah terminal). Sebagai akibat wajar, kami memperoleh penguatan hasil Reynolds 'pada tidak adanya model set-teoretis polimorfisme.

  Sebagai hasilnya, meskipun Anda bisa memberikan semesta yang menafsirkan tipe F dalam logika topos, Anda tidak bisa membiarkannya berinteraksi dengan cara yang menarik dengan set semesta penuh. Namun, semuanya tidak hilang!

  1. Fakta bahwa semesta (non-parametrik) set menafsirkan Sistem F berarti bahwa Anda dapat memberikan model parametrik Sistem F dalam logika internal topos, jauh lebih mudah daripada yang Anda dapat dalam teori himpunan biasa. Pada dasarnya, Anda tidak perlu berkutat dengan PER, karena Anda bisa saja berasumsi bahwa Anda memiliki koleksi set yang sesuai. Bob Atkey menggunakan ide ini dalam makalahnya Relational Parametricity for Higher Kinds , di mana ia mengerjakan parametricity untuk dengan bekerja di kalkulus konstruksi yang impredikatif.$F_\omega$

  2. Reaksi lain terhadap hasil Pitts adalah untuk tidak bekerja dengan teori himpunan, tetapi teori tipe dependen. Karena tidak ada mantan tipe kekuatan dalam teori tipe dependen, Anda tidak perlu khawatir tentang interaksi tipe daya dan polimorfisme. Lihat Atkey, Ghani, dan Johann, A Model Parametrik Relasional dari Teori Tipe Ketergantungan .

• Namun tidak ada hambatan seperti itu untuk membangun model hyperdoctrine-ish, di mana istilah Sistem F adalah objek dari logika. Penelitian sepanjang garis ini mungkin diprakarsai oleh Abadi dan Plotkin dalam makalah seminal mereka A Logic for Parametric Polymorphism . Lars Birkedal dan kolaboratornya telah bekerja keras dalam merumuskan model kategorikal untuk ini dan logika yang serupa --- lihat khususnya Birkedal, Møgelberg, dan Model-Teori Teori Kategori dari Linear Abadi dan Plotkin Logic dari Petersen , yang memberikan logika untuk penalaran tentang Sistem linear F , ditambah bukti bahwa itu adalah suara dan lengkap sehubungan dengan kelas model kategorikal tertentu.