Algoritma pengecekan tipe

19

Saya memulai penelitian bibliografi pribadi tentang algoritme pemeriksaan-jenis dan ingin beberapa kiat. Apa saja algoritma pengecekan tipe, strategi dan teknik umum yang paling umum digunakan?

Saya khususnya tertarik pada algoritma pemeriksaan tipe kompleks yang diimplementasikan dalam bahasa yang diketik sangat dikenal statis seperti, misalnya, C ++, Java 5+, Scala atau yang lainnya. Yaitu, algoritma pengecekan tipe yang tidak terlalu sederhana karena pengetikan yang sangat sederhana dari bahasa yang mendasarinya (seperti Java 1.4 dan di bawah).

Saya sendiri tidak tertarik pada bahasa X, Y, atau Z tertentu. Saya tertarik pada algoritma pengecekan tipe terlepas dari bahasa yang mereka targetkan. Jika Anda memberikan jawaban seperti "bahasa L yang belum pernah Anda dengar yang diketik dengan kuat dan pengetikannya kompleks memiliki algoritma pengecekan tipe yang melakukan A, B dan C dengan memeriksa X dan Y menggunakan algoritma Z", atau "the strategi X dan Y digunakan untuk Scala dan varian Z dari A yang digunakan untuk C # keren karena fitur R, S dan T yang bekerja dengan cara itu ", maka jawabannya bagus.

algorithms programming-languages reference-request type-checking Victor Stafusa
sumber
3
Mungkin Anda harus mengedit pertanyaan ini untuk menanyakan tentang pemeriksaan jenis untuk satu bahasa tertentu. Pertanyaan-pertanyaan gaya daftar terbuka, umumnya tidak disarankan di SE (meskipun situs khusus ini belum memiliki kebijakan mengenai itu). Juga: <type-system-elitist> Sistem tipe Java tidak rumit </type-system-elitist>.
sepp2k
3
Mungkin pertanyaannya bisa diulang menjadi lebih spesifik, tetapi saya tidak berpikir itu harus ditutup.
Dave Clarke
1
@ sepp2k: Saya tahu itu agak luas, tetapi berakhir dengan cara ini karena saya tidak ingin membatasi kegunaan jawaban. BTW, saya tidak mengerti apa yang ingin Anda katakan dengan "<type-system-elitist> sistem tipe Java tidak kompleks </type-system-elitist>". Sistem tipe 1.4 dan di bawah Java sebenarnya sederhana, tetapi sedikit pun generik di Java 5, itu menjadi jauh lebih kompleks.
Victor Stafusa
2
Meminta satu bahasa tertentu akan membuat pertanyaan lebih cocok untuk situs ini, imho. Pertanyaannya mungkin harus menanyakan teknik umum.
Raphael
1
@ Viktor Alat dasar adalah Tata Bahasa Atribut . Anda mungkin tidak akan dapat melakukan setiap hal jahat yang dapat Anda bayangkan bersama mereka, tetapi mereka adalah titik awal yang baik.
Raphael

Jawaban:

13

Sebagian besar penelitian sebenarnya tidak mempublikasikan algoritme pengecekan tipe untuk bahasa pemrograman full blown. Anda akan menemukan beberapa formalisasi dari sebagian besar sistem tipe untuk bahasa pemrograman penuh, seperti pekerjaan yang dilakukan oleh Drossopoulou dan Eisenbach untuk Java atau karya Nipkov et al pada C ++ . Namun, lebih sering, Anda hanya akan menemukan sistem tipe untuk beberapa bagian inti dari bahasa (Featherweight Java adalah salah satu contoh) atau untuk konsep inti bahasa seperti pendekatan inferensi tipe lokal dari scala .

Dalam konferensi seperti POPL dan ICFP Anda akan menemukan banyak algoritma pengecekan tipe untuk jenis tertentu dari sistem tipe, dan pendekatan baru seperti pengecekan bidirectional dan tridirectional .

Secara lebih umum, Anda mungkin perlu tahu tentang algoritma Damas-Milner , inferensi tipe lokal, bidirectional dan tridirectional type checking, dan berkembang dari sana, dengan mengikuti referensi di makalah dan dengan menggunakan Google Cendekia untuk menemukan makalah yang mengutip ini dan membangunnya pendekatan yang dijelaskan. Juga, seperti yang disarankan di atas, konferensi seperti POPL, ICPF, ESOP dan bahkan ECOOP dan OOPSLA akan memiliki makalah yang relevan dengan pencarian Anda.

Dave Clarke
sumber
Afaik, sistem tipe Scala telah dikembangkan dalam proyek penelitian dan dengan demikian diterbitkan. Kompiler juga bersumber terbuka. Namun belum melihat ke dalam.
Raphael
Tidak perlu bagiku untuk menyimpulkan; Saya tahu bahwa ada makalah yang diterbitkan tentang sistem tipe Scala. Klaim ini mudah diperiksa dengan mencari . Juga, saya menghitung kode sumber kompiler sebagai publikasi yang cukup pada algoritma (asalkan itu termasuk dalam sumber; Saya berasumsi demikian tetapi tidak memeriksa). Pernyataan awal saya ambigu, benar, tetapi reaksi Anda tampaknya tidak beralasan.
Raphael
2

Alat dasar adalah Tata Bahasa Atribut . Anda mungkin tidak akan dapat melakukan setiap hal jahat yang dapat Anda bayangkan bersama mereka, tetapi mereka adalah titik awal yang baik.

Pada dasarnya, Anda dapat berjalan di atas pohon sintaksis abstrak program top-down dan / atau bottom-up dan memberikan informasi sekitar. Jadi, misalnya, Anda bisa meneruskan informasi tipe cakupan global (misalnya kelas dan anggotanya) ke bawah dan menentukan jenis ekspresi secara rekursif, yaitu bottom-up, meneruskan tipe yang dihasilkan ke atas.

Temukan beberapa penjelasan dan contoh dalam slide di sini (Bab 5).

Raphael
sumber
Apakah ada yang punya referensi yang lebih baik? Saya kira saya perlu membeli Dragonbook atau Wilhelm / Maurer suatu hari ini ...
Raphael
1
Alat JastAdd adalah sistem kompiler kompiler modern yang sangat baik berdasarkan tata bahasa atribut referensi. Kami telah menggunakannya di sejumlah proyek.
Dave Clarke