Mengapa algoritma Hindley-Milner tidak akan menghasilkan tipe seperti t1 -> t2?

Saya membaca tentang algoritma pengetikan Hindley-Milner saat menulis implementasi, dan melihat bahwa, selama setiap variabel terikat, Anda akan selalu mendapatkan tipe atau tipe atom di mana argumen akan menentukan tipe final, seperti t1 -> t1atau (t1 -> t2) -> (t1 -> t2)di mana t1dan t2jenis variabel.

Saya tidak bisa memikirkan cara Anda akan mendapatkan sesuatu seperti t1 -> t2atau hanya t1, yang saya mengerti berarti algoritma rusak karena tidak akan ada cara untuk menentukan jenis ekspresi yang sebenarnya. Bagaimana Anda tahu Anda tidak akan pernah mendapatkan jenis seperti ini yang "rusak" selama setiap variabel terikat?

Saya tahu algoritma menghasilkan tipe dengan variabel, tetapi ini selalu diselesaikan setelah Anda meneruskan argumen ke fungsi, yang tidak akan terjadi pada fungsi dengan tipe t1 -> t2. Inilah mengapa saya ingin tahu bagaimana kita mengetahui dengan pasti bahwa algoritma tidak akan pernah menghasilkan tipe seperti itu.

(Tampaknya Anda bisa mendapatkan tipe "rusak" ini dalam ML , tapi saya bertanya tentang lambda calculus.)

Dalam kalkulus lambda tanpa konstanta dengan sistem tipe Hindley-Milner, Anda tidak bisa mendapatkan tipe seperti itu di mana hasil suatu fungsi adalah variabel tipe yang tidak terselesaikan. Semua variabel tipe harus memiliki "asal" di suatu tempat. Misalnya, tidak ada istilah tipe , tetapi ada istilah tipe ∀ α $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$ (fungsi identitas λ x . x ).$\forall \alpha.\; \alpha\mathbin\rightarrow\alpha$$\lambda x.x$

Secara intuitif, istilah tipe membutuhkan kemampuan untuk membangun ekspresi tipe β dari udara tipis. Sangat mudah untuk melihat bahwa tidak adanilaiyang memiliki tipe seperti itu. Lebih tepatnya, jika variabel tipe β tidak muncul dalam tipe variabel istilah apa pun di lingkungan, maka tidak ada istilah tipe β yang berada dalam bentuk normal kepala. Anda dapat membuktikan ini dengan induksi struktural pada istilah: baik variabel di kepala harus memiliki tipe β , atau salah satu argumen harus memiliki tipe utama yang melibatkan β , yaitu akan ada istilah cocok yang lebih kecil.$\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$$\beta$$\beta$$\beta$$\beta$$\beta$

Hanya karena tidak ada nilai dari jenis tertentu tidak berarti bahwa tidak ada istilah dari jenis itu: mungkin ada istilah tanpa nilai, yaitu istilah non-terminating (tepatnya, sebuah istilah tanpa bentuk normal). Alasan mengapa tidak ada istilah lambda dengan jenis seperti itu adalah bahwa semua istilah HM yang diketik dengan baik sangat normal. Ini adalah generalisasi dari hasil yang menyatakan bahwa cukup mengetik kalkulus lambda sangat normal. Ini adalah konsekuensi dari kenyataan bahwa Sistem F sangat normal: Sistem F seperti HM, tetapi memungkinkan jenis quantifiers di mana-mana dalam tipe, tidak hanya di tingkat atas. Misalnya, dalam Sistem F, memiliki tipe ( ∀ α . α ) → ( ∀ α . α ) - tetapi$\Delta = \lambda x. x \, x$$(\forall \alpha. \alpha) \rightarrow (\forall \alpha. \alpha)$ tidak diketik dengan baik.$\Delta\,\Delta$

HM dan Sistem F adalah contoh sistem tipe yang memiliki korespondensi Curry-Howard : istilah yang diketik dengan baik sesuai dengan bukti dalam logika tertentu, dan jenis yang sesuai dengan rumus. Jika sistem tipe sesuai dengan teori yang konsisten, maka teori itu tidak memungkinkan pembuktian teorema seperti ; oleh karena itu tidak ada istilah dari tipe yang sesuai ∀ α , β $\forall A, \forall B, A \Rightarrow B$ . Sistem tipe memungkinkan seseorang untuk menyimpulkan "teorema secara gratis" tentang fungsi-fungsi di atas struktur data.$\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$

Hasil ini rusak segera setelah Anda menambahkan konstanta tertentu ke kalkulus. Misalnya, jika Anda mengizinkan kombinator fixpoint umum seperti , dimungkinkan untuk membuat istilah tipe arbitrer: Y ( λ x . X ) memiliki tipe ∀ α . α . Setara dengan kombinator fixpoint umum dalam korespondensi Curry-Howard adalah aksioma yang menyatakan ∀ A , ∀ B , A ⇒ B , yang membuat logika jelas tidak sehat.$Y$$Y (\lambda x.x)$$\forall \alpha. \alpha$$\forall A, \forall B, A \Rightarrow B$

Menemukan garis tipis antara sistem tipe yang memastikan normalisasi yang kuat dan sistem tipe yang tidak merupakan masalah yang sulit dan menarik. Ini adalah masalah penting karena menentukan logika mana yang sehat, dengan kata lain program mana yang mewujudkan bukti teorema. Anda bisa melangkah lebih jauh dari Sistem F, tetapi aturannya menjadi lebih kompleks. Sebagai contoh, kalkulus konstruksi induktif yang merupakan dasar asisten bukti Coq , sangat normal namun mampu menggambarkan struktur data umum dan algoritma induktif di atasnya, dan banyak lagi.

Segera setelah Anda sampai ke bahasa pemrograman nyata, korespondensi rusak. Bahasa pemrograman nyata memiliki fitur seperti fungsi rekursif umum (yang mungkin tidak berakhir), pengecualian (ekspresi yang selalu menimbulkan pengecualian tidak pernah mengembalikan nilai dan karenanya dapat memiliki jenis apa pun di sebagian besar sistem tipe), tipe rekursif (yang memungkinkan non-terminasi) untuk menyelinap masuk), dll.