Penelitian tentang inferensi tipe berbasis situs panggilan?

9

Saya mencoba untuk mempelajari lebih lanjut tentang pengecekan seluruh tipe program dan sistem inferensia tipe yang menggunakan informasi dari situs pemanggilan fungsi untuk menghitung informasi jenis (selain pendekatan standar menggunakan fungsi tubuh). Sebagai contoh, algoritma seperti itu mungkin menggunakan pemanggilan fungsi foo(1)untuk menyimpulkan bahwa fungsi dalam foomengambil argumen integer. Jelas ini akan menyulitkan inferensi banyak dan membuat pemeriksaan menjadi non-modular.

Bagaimanapun, saya belum beruntung menemukan penelitian tentang pendekatan ini, mungkin karena saya tidak tahu terminologi yang tepat untuk menggambarkan apa yang saya bicarakan. Ada petunjuk?

pl.programming-languages type-theory type-inference type-systems Derek Thurn
sumber
Apa yang Anda gambarkan memiliki petunjuk tentang inferensi tipe dua arah, kecuali saya salah. Namun, menguraikan apa yang Anda coba lakukan dapat menjelaskan.
Dominic Mulligan
Apakah Anda bertanya karena Anda mencari cara untuk mengkhususkan fungsi polimorfik?
nponeccop
Saya kebanyakan hanya mencoba untuk belajar lebih banyak tentang sistem tipe, dan ya, saya berpikir sebagian besar tentang bagaimana menangani fungsi polimorfik (dan pemanggilan metode dalam bahasa OO, hal yang sama). Saya mencoba mengidentifikasi istilah yang tepat untuk ini sehingga saya dapat membacanya.
Derek Thurn

Jawaban:

11

Hampir semua sistem dengan inferensi tipe menggunakan informasi situs panggilan untuk melakukan ini. Contohnya termasuk ML Standar, OCaml, F #, dan Haskell. Banyak bahasa lain menggunakan informasi situs panggilan untuk menyimpulkan instantiation parameter tipe, seperti Java, C #, Scala, dan Typed Racket. Ini sering kali disebut dengan nama "Local Type Inference".

Saya hanya akan menggambarkan apa yang Anda cari sebagai "Ketik Inferensi", dan Anda mungkin harus mulai dengan mencari apa yang dikenal sebagai sistem "Hindley-Milner". Halaman Wikipedia memberikan pengantar yang masuk akal, dan menunjuk ke makalah asli.

Tempat untuk memulai Inferensi Jenis Lokal adalah kertas asli Pierce dan Turner, paling baik dibaca dalam versi TOPLAS 2000 ( ACM , PDF ).

Sam Tobin-Hochstadt
sumber
Kertas Pierce dan Turner sangat mencerahkan, terima kasih. Apakah Anda mengetahui penerapan minimal algoritma yang dijelaskan dalam kode? Saya pikir itu akan sangat menarik untuk dilihat juga, jika ada.
Derek Thurn
Saya tidak tahu ada implementasi minimal. Ada satu di Typed Racket, dan satu di Scala, tetapi keduanya mengimplementasikan algoritma yang jauh lebih rumit.
Sam Tobin-Hochstadt
0

Anda dapat melihat pada sistem tipe untuk tipe persimpangan yang dapat memberi Anda sesuatu seperti a :: Int -> Int | Bool -> Bool, sehingga Anda tahu bahwa dua spesialisasi Intdan Boolcukup, atau menggunakan inferensi tipe biasa untuk menyimpulkan sebagian besar tipe umum diikuti dengan analisis aliran kontrol untuk mengumpulkan aktual ketik argumen. Bahkan ada pendekatan hybrid (CFA dinyatakan sebagai sistem tipe dan sebaliknya).

Penelitian berfungsi untuk menyimpulkan paling tidak tipe umum daripada tipe paling umum yang mungkin ada, tetapi saya tidak menyadarinya.

Adapun teknik untuk menerapkan polimorfisme, ada dua solusi: 1) spesialisasi (pikirkan template C ++) 2) asumsi representasi seragam (pikirkan koleksi gaya-C dengan void *).

Untuk 2, Anda tidak perlu mengetik dari situs panggilan selama pemeriksaan ketik, dan dapat mendukung kompilasi terpisah dengan lebih mudah.

Perhatikan bahwa kita berbicara tentang polimorfisme parametrik di sini, dan pemanggilan metode virtual OO adalah hal yang sama sekali berbeda yang disebut polimorfisme subtipe. Perhatikan bahwa templat C ++ mendukung sesuatu seperti polimorfisme parametrik dan pengetikan bebek, yang merupakan bentuk lain polimorfisme.

nponeccop
sumber
1
"Panggilan metode virtual OO adalah hal yang sama sekali berbeda yang disebut polimorfisme ad-hoc" Polimorfisme ad-hoc adalah nama lain untuk kelebihan beban. Anda tampaknya bingung dengan polimorfisme subtipe.
Radu GRIGore
Tetapi subkelas tidak selalu merupakan subtipe, bukan? Misalnya untuk subtipe yang seharusnya dimiliki LSP.
nponeccop
1
Benar, tapi di samping itu. "Subtipe polimorfisme" adalah istilah standar. Lihat en.wikipedia.org/wiki/Subtype_polymorphism untuk detailnya.
Radu GRIGore