Polimorfisme tingkat tinggi di atas tipe yang tidak dikotak

Saya memiliki bahasa di mana tipe tidak dikotakkan secara default, dengan inferensi tipe berdasarkan Hindley-Milner. Saya ingin menambahkan polimorfisme tingkat tinggi, terutama untuk bekerja dengan tipe eksistensial.

Saya rasa saya mengerti bagaimana memeriksa jenis ini, tapi saya tidak yakin apa yang harus dilakukan ketika kompilasi. Saat ini, saya mengkompilasi definisi polimorfik dengan menghasilkan spesialisasi, seperti template C ++, sehingga mereka dapat bekerja dengan nilai-nilai unboxed. Misalnya, diberi definisi f<T>, jika program hanya memanggil f<Int32>dan f<Char>, maka hanya spesialisasi yang muncul dalam program yang dikompilasi. (Saya mengasumsikan kompilasi seluruh program untuk saat ini.)

Tetapi ketika melewati fungsi polimorfik sebagai argumen, saya tidak melihat bagaimana saya dapat menghasilkan spesialisasi yang tepat secara statis, karena fungsi tersebut dapat dipilih saat runtime. Apakah saya tidak punya pilihan selain menggunakan representasi kotak? Atau apakah ada cara untuk mengatasi masalah ini?

Pikiran pertama saya adalah entah bagaimana encode Rank n polimorfisme sebagai peringkat 1, tapi saya tidak percaya itu mungkin pada umumnya karena formula dalam logika konstruktif tidak selalu memiliki bentuk normal prenex.

Saya sudah memikirkan sedikit tentang ini. Masalah utama adalah bahwa secara umum, kita tidak tahu seberapa besar nilai tipe polimorfik. Jika Anda tidak memiliki informasi ini, Anda harus mendapatkannya entah bagaimana. Monomorphisation mendapatkan informasi ini untuk Anda dengan mengkhususkan diri pada polimorfisme. Boxing mendapatkan informasi ini untuk Anda dengan meletakkan semuanya ke dalam representasi ukuran yang diketahui.

Alternatif ketiga adalah melacak informasi ini. Pada dasarnya, yang dapat Anda lakukan adalah memperkenalkan jenis yang berbeda untuk setiap ukuran data, dan kemudian fungsi polimorfik dapat didefinisikan atas semua jenis ukuran tertentu. Saya akan membuat sketsa sistem seperti di bawah ini.

$$\newcommand{\bnfalt}{\;\;|\;\;} \newcommand{\rule}[2]{{\mathord{\array{#1}} \over {\mathord{#2}}}} \newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}$$ $$\begin{array}{llcl} \mbox{Kinds} & \kappa & ::= n \\ \mbox{Type constructors} & A & ::= & \forall a:\kappa.\; A \bnfalt \alpha \bnfalt A \times B \bnfalt A + B \bnfalt A \to B \\ & & | & \mathsf{ref}\;A \bnfalt \mathsf{Pad}(k) \bnfalt \mu \alpha:\kappa.\; A\\ \end{array}$$

Di sini, ide tingkat tinggi adalah bahwa jenis tipe memberi tahu Anda berapa banyak kata yang diperlukan untuk meletakkan objek dalam memori. Untuk ukuran apa pun, mudah menjadi polimorfik untuk semua jenis ukuran tertentu. Karena setiap jenis - bahkan yang polimorfik - masih memiliki ukuran yang diketahui, kompilasi tidak lebih sulit daripada untuk C.

Aturan kinding mengubah bahasa Inggris ini menjadi matematika, dan akan terlihat seperti ini: Γ ⊢ A : n Γ ⊢ B :

$$\rule{ \alpha:n \in \Gamma} { \judge{\Gamma}{\alpha}{n} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{m} } { \judge{\Gamma}{\forall \alpha:n.\; A}{m} }$$ Γ ⊢ A : m Γ ⊢ B : $$\rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{m} } { \judge{\Gamma}{A \times B}{n + m} } \qquad \rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A + B}{n + 1} }$$ $$\rule{ \judge{\Gamma}{A}{m} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A \to B}{1} } \qquad \rule{ \judge{\Gamma}{A}{n} } { \judge{\Gamma}{\mathsf{ref}\;A}{1} }$$ $$\rule{ } { \judge{\Gamma}{\mathsf{Pad}(k)}{k} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{n} } { \judge{\Gamma}{\mu \alpha:n.\; A}{n} }$$

Jadi forall quantifier mengharuskan Anda memberikan jenis yang Anda jangkau. Demikian juga, pasangan adalah jenis pasangan tanpa kotak, yang hanya menjabarkan sebelah dalam memori (seperti tipe C struct). Disjoint unions mengambil dua nilai dengan ukuran yang sama, dan kemudian menambahkan kata untuk tag diskriminator. Fungsi adalah penutupan, diwakili seperti biasa oleh pointer ke catatan lingkungan dan kode.$A \times B$$A$$B$

Referensi menarik - pointer selalu satu kata, tetapi mereka dapat menunjuk ke nilai dari berbagai ukuran. Hal ini memungkinkan pemrogram menerapkan polimorfisme ke objek sewenang-wenang dengan tinju, tetapi tidak mengharuskan mereka untuk melakukannya. Akhirnya, setelah ukuran eksplisit dimainkan, sering kali berguna untuk memperkenalkan jenis padding, yang menggunakan ruang tetapi tidak melakukan apa-apa. (Jadi jika Anda ingin mengambil persatuan int dan sepasang int, Anda perlu menambahkan pad int pertama, sehingga tata letak objek seragam.)

Tipe rekursif memiliki aturan formasi standar, tetapi perhatikan bahwa kejadian rekursif harus memiliki ukuran yang sama, yang berarti Anda biasanya harus menempelkannya dalam sebuah pointer untuk membuat kinding bekerja. Misalnya, tipe data daftar dapat direpresentasikan sebagai

$$\mu \alpha:1.\; \mathsf{ref}\;(\mathsf{Pad}(2) + \mathsf{int} \times \alpha)$$

Jadi ini menunjuk ke nilai daftar kosong, atau sepasang int dan pointer ke daftar tertaut lainnya.

Jenis memeriksa sistem seperti ini juga tidak terlalu sulit; algoritma dalam makalah ICFP saya dengan Joshua Dunfield, Pengetikan Dua Arah Lengkap dan Mudah untuk Polimorfisme Peringkat Tinggi berlaku untuk kasus ini dengan hampir tidak ada perubahan.

Ini tampaknya lebih dekat dengan masalah kompilasi daripada masalah "ilmu komputer teoretis", jadi Anda mungkin lebih baik bertanya di tempat lain.

Dalam kasus umum, memang, saya pikir tidak ada solusi lain selain menggunakan representasi kotak. Tetapi saya juga berharap bahwa dalam praktiknya ada banyak pilihan alternatif yang berbeda, tergantung pada spesifik situasi Anda.

Misalnya representasi tingkat rendah dari argumen tanpa kotak biasanya dapat dikategorikan ke dalam beberapa alternatif, misalnya integer-atau-mirip, floating-point, atau pointer. Jadi untuk suatu fungsi f<T>, mungkin Anda benar-benar hanya perlu menghasilkan 3 implementasi tanpa kotak yang berbeda dan Anda dapat mewakili yang polimorfik sebagai tuple dari 3 fungsi tersebut, jadi instantiasi T ke Int32 hanya memilih elemen pertama tuple, ...