Apa sistem tipe terkuat yang diketahui yang kesimpulannya dapat ditentukan?

Sudah diketahui bahwa inferensi tipe Hindley-Milner ( -kalkulus yang diketik sederhana dengan polimorfisme) memiliki inferensi tipe yang dapat decidable: Anda dapat merekonstruksi tipe prinsip untuk program apa pun tanpa anotasi apa pun.$\lambda$

Menambahkan typeclasses bergaya Haskell tampaknya mempertahankan decidability ini, tetapi penambahan lebih lanjut membuat kesimpulan tanpa anotasi tidak dapat diputuskan (keluarga tipe, GADTs, tipe-dependen, tipe Rank-N, Sistem , dll.)$\omega$

Saya bertanya-tanya: apa jenis sistem terkuat yang diketahui dengan inferensi yang sepenuhnya dapat ditentukan? Ini akan terletak di suatu tempat antara Hindley-Milner (benar-benar dapat didekati) dan tipe-dependen (benar-benar tidak dapat dipastikan). Apakah ada aspek DTS yang dapat ditambahkan yang mempertahankan kepantasan inferensi? Penelitian apa yang telah dilakukan untuk melihat sejauh mana hal ini dapat didorong?

Saya menyadari bahwa tidak ada satu pun sistem terkuat, bahwa ada kemungkinan kecil, perubahan tambahan yang tak terbatas yang dapat ditambahkan ke HM menjaga kesimpulan. Tetapi ada kemungkinan beberapa kandidat praktis dari sistem yang telah ditemukan.

Sunting: mengingat bahwa tidak ada sistem "terkuat", saya akan menerima jawaban yang menguraikan sistem terkenal yang memperluas Hindley Milner dengan inferensi yang dapat ditentukan. Contohnya bisa tipe cair, peringkat-2, dll.

[EDIT: Voilà beberapa kata di masing-masing]

Ada beberapa cara untuk memperluas inferensi tipe HM. Jawaban saya didasarkan pada banyak, lebih atau kurang berhasil, upaya menerapkan beberapa di antaranya. Yang pertama saya temukan adalah polimorfisme parametrik . Tipe sistem yang mencoba memperluas HM ke arah ini cenderung ke arah Sistem F dan karenanya memerlukan anotasi tipe. Dua ekstensi penting ke arah ini yang saya temui adalah:

• HMF, memungkinkan inferensi tipe untuk semua tipe Sistem-F, yang berarti Anda dapat memiliki kuantifikasi universal "di tengah" suatu tipe, penampilan mereka tidak secara implisit terletak pada ruang lingkup tertinggi seperti untuk tipe polimorfik HM. Makalah ini dengan jelas menyatakan bahwa tidak ada aturan yang jelas tentang berapa banyak dan di mana anotasi jenis mungkin diperlukan. Juga jenis-jenisnya adalah Sistem F, istilah biasanya tidak memiliki tipe utama.

• MLF tidak hanya perpanjangan dari HM, itu juga perpanjangan dari Sistem F yang mendapatkan kembali properti tipe utama dari HM dengan memperkenalkan semacam kuantifikasi terbatas atas jenis. Sebuah perbandingan telah dibuat oleh penulis, MLF benar-benar lebih kuat daripada HMF dan penjelasan hanya diperlukan untuk parameter yang digunakan secara polimorfik.

Cara lain untuk memperluas HM adalah melalui variasi domain kendala.

• HM (X) adalah Hindley-Milner yang diparameterisasi menggunakan domain kendala X. Dalam pendekatan ini, algoritma HM menghasilkan kendala yang dikirim ke pemecah domain untuk X. Untuk HM biasa, pemecah domain adalah prosedur unifikasi dan domain terdiri dari himpunan istilah membangun dari jenis dan variabel jenis.
  Contoh lain untuk X dapat berupa batasan-batasan yang diekspresikan dalam bahasa aritmatika Presburger (di mana inferensi / pengecekan tipe kasus dapat ditentukan) atau dalam bahasa aritmatika Peano (tidak lagi dapat dipercayakan). X bervariasi di sepanjang spektrum teori, masing-masing dengan persyaratannya sendiri mengenai jumlah dan lokalisasi anotasi jenis yang diperlukan dan mulai dari tidak sama sekali hingga semuanya.

• Kelas tipe Haskell juga merupakan jenis ekstensi dari domain kendala dengan menambahkan predikat tipe formulir MyClass(MyType)(artinya ada instance MyClass untuk tipe MyType).
  Kelas tipe mempertahankan tipe inferensi karena pada dasarnya mereka adalah konsep (hampir) ortogonal yang mereka terapkan pada polimorfisme adhoc .
  Sebagai contoh, ambil simbol valtipe val :: MyClass a => ayang Anda dapat memiliki instance MyClass A, MyClass Bdll. Ketika Anda merujuk simbol itu dalam kode Anda, itu sebenarnya karena inferensi tipe sudah dilakukan sehingga kompiler dapat menyimpulkan instance kelas yang akan digunakan. Ini berarti bahwa tipe valtergantung pada konteks di mana ia digunakan. Itu juga mengapa menjalankan satu valpernyataan mengarah keambiguous type error : kompilator tidak dapat menyimpulkan tipe apa pun berdasarkan konteksnya.

Untuk sistem tipe yang lebih maju seperti GADT, keluarga tipe, tipe Dependent, System (F) ω, dll., Tipe bukan lagi "tipe" mereka menjadi objek komputasi yang kompleks. Misalnya itu berarti bahwa dua jenis yang tidak terlihat sama tidak selalu berbeda. Jadi tipe kesetaraan menjadi tidak sepele (sama sekali).

Untuk memberi Anda contoh kompleksitas aktual, mari pertimbangkan jenis dependen daftar: di NList a nmana ajenis objek dalam daftar dan npanjangnya.
Fungsi append akan memiliki tipe append :: NList a n -> NList a m -> NList a (n + m)dan fungsi zip akan menjadi zip :: NList a n -> NList b n -> NList (a, b) n.
Bayangkan sekarang kita memiliki lambda \a: NList t n, b: NList t m -> zip (append a b) (append b a). Di sini argumen pertama dari zip adalah tipe NList t (n + m)dan tipe kedua NList t (m + n).
Hampir sama, tetapi kecuali pemeriksa tipe tahu bahwa "+" berpindah pada bilangan asli, ia harus menolak fungsi karena (n + m) tidak secara harfiah (m + n). Ini bukan lagi tentang tipe inferensi / pengecekan tipe, ini tentang pembuktian teorema.

Jenis cairan tampaknya melakukan beberapa inferensi tipe dependen. Tapi seperti yang saya pahami, ini bukan tipe dependen, lebih seperti tipe HM biasa yang inferensi tambahannya dibuat untuk menghitung batas statis.

Saya harap ini membantu.