Inferring type refinement

Di tempat kerja saya ditugaskan untuk menyimpulkan beberapa jenis informasi tentang bahasa yang dinamis. Saya menulis ulang urutan pernyataan menjadi letekspresi bersarang , seperti:

return x; Z            =>  x
var x; Z               =>  let x = undefined in Z
x = y; Z               =>  let x = y in Z
if x then T else F; Z  =>  if x then { T; Z } else { F; Z }

Karena saya mulai dari informasi tipe umum dan mencoba menyimpulkan tipe yang lebih spesifik, pilihan alami adalah tipe perbaikan. Sebagai contoh, operator kondisional mengembalikan penyatuan jenis cabang benar dan salahnya. Dalam kasus sederhana, ini bekerja dengan sangat baik.

Namun, saya mengalami hambatan, ketika mencoba menyimpulkan jenis berikut ini:

function g(f) {
  var x;
  x = f(3);
  return f(x);
}

Yang ditulis ulang untuk:

\f.
  let x = undefined in
    let x = f 3 in
      f x

$\mathtt{f} : \mathtt{Int} \to \mathtt{Int}$$\mathtt{g} : (\mathtt{Int} \to \mathtt{Int}) \to \mathtt{Int}$

$$\mathtt{g} : \forall \tau_1 \tau_2. \:(\mathtt{Int} \to \tau_1 \land \tau_1 \to \tau_2) \to \tau_2$$

Saya sudah menggunakan dependensi fungsional untuk menyelesaikan tipe +operator yang kelebihan beban , jadi saya pikir itu adalah pilihan alami untuk menggunakannya untuk menyelesaikan tipe fdalam g. Artinya, tipe-tipe fdalam semua aplikasinya bersama-sama secara unik menentukan tipe g. Namun, ternyata, fundeps tidak meminjamkan diri mereka dengan sangat baik untuk jumlah variabel jenis sumber.

Pokoknya, saling mempengaruhi polimorfisme dan pengetikan mengetik bermasalah. Jadi, apakah ada pendekatan yang lebih baik yang saya lewatkan? Saat ini saya sedang mencerna "Jenis Perbaikan untuk ML" dan akan lebih menghargai literatur atau petunjuk lainnya.

Anda telah tersandung pada kenyataan bahwa kesimpulan invarian statis untuk bahasa tingkat tinggi cukup sulit dalam praktiknya, di samping tidak dapat ditentukan secara teori. Saya tidak yakin apa jawaban pasti untuk pertanyaan Anda, tetapi perhatikan beberapa hal:

• Tipe polimorfisme dan perbaikan berperilaku buruk bersama, seperti yang telah Anda catat, khususnya gagasan tentang tipe paling umum hilang. Konsekuensi dari hal ini adalah bahwa analisis yang didasarkan pada tipe penyempurnaan dengan adanya polimorfisme mungkin perlu memilih antara analisis seluruh program (yang bertentangan dengan analisis komposisi) dan penggunaan heuristik untuk memutuskan jenis yang ingin Anda tetapkan untuk program Anda.

• Ada hubungan yang kuat antara menyimpulkan jenis penyempurnaan dan:

  1. Komputasi interpretasi abstrak dari program Anda

  2. Komputasi invarian loop dalam bahasa imperatif.

Dengan mengingat hal ini, berikut adalah beberapa referensi yang tidak teratur tentang kesimpulan jenis penyempurnaan. Perhatikan bahwa ada banyak jenis rasa yang berbeda: Saya cenderung lebih tertarik pada penyempurnaan tipe data induktif, jadi daftar ini mungkin condong ke arah itu.

1. Mulailah dengan klasik: Interpretasi Abstrak Relasional dari Program Fungsional Tingkat Tinggi oleh Cousot & Cousot. Ini menjelaskan bagaimana memperluas interpretasi abstrak ke program tingkat tinggi menggunakan semantik relasional.

2. Jenis Cair oleh Rhondon, Kawaguchi dan Jhala. Ini adalah pekerjaan yang sangat berkembang, yang menggabungkan HM dan jenis penyempurnaan predikat untuk menyimpulkan anotasi keamanan (cek terikat array misalnya) untuk program gaya ML. Inferensi berlangsung dalam 2 langkah; yang pertama adalah inferensi HM dari anotasi jenis, yang memandu pilihan penyempurnaan untuk dilakukan.

3. $F^*$$F^\#$

4. Ada kertas bagus karya Chin dan Khoo tentang inferensi jenis penyempurnaan tertentu: jenis dengan anotasi ukuran.

5. The ATS bahasa pemrograman adalah sistem yang memungkinkan berbagai perbaikan dan menyediakan fasilitas untuk menulis program dengan mereka. Namun penjelasannya mungkin rumit dan sewenang-wenang (dan karenanya tidak dapat dipastikan) dan karenanya memerlukan interaksi pengguna. Saya percaya bahwa ada bentuk inferensi untuk jenis ini, saya tidak yakin artikel mana yang direkomendasikan.

6. Terakhir, namun tidak kalah pentingnya , Algoritma Produk Cartesian , oleh Ole Agesen. Meskipun tidak menyebutkan jenis penyempurnaan secara eksplisit, ini tampaknya merupakan pekerjaan terdekat untuk menyelesaikan masalah yang tampaknya Anda miliki. Jangan tertipu oleh penyebutan parametrik polimorfisme secara abstrak: mereka mencari kesimpulan tipe-tipe konkret , yang hanya merupakan tupel dari tipe-tipe atom yang mungkin. Penekanan diberikan pada efisiensi. Saya sarankan membaca artikel ini terlebih dahulu untuk melihat apakah itu memecahkan masalah Anda.

$\lambda$