Apa perbedaan utama antara polimorfisme baris dan subtipe

Saya sering mendengar bahwa polimorfisme baris adalah pendekatan yang lebih baik daripada subtyping, tetapi saya kesulitan menemukan apa pun yang membandingkannya secara terperinci. Saya terutama tertarik pada perspektif pengguna sistem.

Saya memang menemukan posting blog ini , tetapi meninggalkan saya dengan lebih banyak pertanyaan daripada sebelumnya. Misalnya, ia membuat klaim bahwa sistem dengan subtyping akan menetapkan satu jenis, sedangkan sistem dengan pengetikan baris akan menetapkan yang lain; apakah itu berarti bahwa jika suatu sistem yang konon memiliki subtyping menetapkan tipe "pengetikan baris", bahwa sistem tersebut mengklaim secara salah?

Satu perbedaan utama yang saya lihat adalah bahwa pengetikan baris memungkinkan untuk menyelaraskan jenis argumen (yaitu, menulis fungsi dua argumen yang hanya menyangkut abidang argumennya, tetapi mengharuskan argumennya memiliki bidang yang sama) .

Subtyping mengatakan dengan memberikan ekspresi dari satu tipe, kita juga dapat memberikannya tipe yang lain. Kami mengatakan yang pertama adalah subtipe dari yang terakhir dan hubungan subtyping ini menginduksi banyak hubungan lainnya. Dalam simbol,

Kuncinya di sini (dan alasan saya meninjaunya) adalah bahwa ekspresi yang sama diberikan dua jenis yang berbeda. Dalam bahasa parametrically polimorfik dengan implisit jenis Instansiasi kita memiliki hubungan subtyping berikut: untuk semua jenis . Jika tipe Instansiasi eksplisit seperti di Sistem F, hubungan subtyping ini tidak berlaku.$(\forall \alpha.\tau) <: \tau[T/\alpha]$$T$

Sebagai tambahan, kita dapat mengatakan sebuah bahasa dengan tipe baris (biasanya) memiliki hubungan subtyping dari bentuk memunculkan mana . Namun, cara ini sebenarnya ditangani adalah dengan mengubah gagasan kesetaraan jenis (yaitu penyatuan) sehingga , yaitu mereka menyatukan. Dalam kasus ini, hubungan subtipe adalah sepele satu.$\{\ell_1:A,\ell_2:B\} <: \{\ell_2:B,\ell_1:A\}$$\{\ell_1:A,\ell_2:B\} \cong \{\ell_2:B,\ell_1:A\}$$S \cong T \iff S <: T \land T <: S$$\{\ell_1:A,\ell_2:B\} = \{\ell_2:B,\ell_1:A\}$$T <: T$

Biasanya ketika kita berbicara tentang bahasa dengan subtyping yang kita maksud adalah bahasa dengan hubungan subtyping non-sepele pada tipe tanah , yaitu tipe tanpa variabel bebas (yang, tentu saja, dapat dan akan menghasilkan hubungan subtipe untuk jenis non-tanah). Jadi sebuah sistem dengan polimorfisme baris seperti milik Roy bukanlah bahasa dengan subtyping dalam pengertian ini, meskipun ia memiliki hubungan subtipe non-sepele yang berasal dari bahasa polimorfik parametrik instantiated implisit. Subtipe struktural, di sisi lain, secara eksplisit menyatakan hubungan subtipe non-sepele untuk tipe tanah.

Menurut jenis baris , maksud saya memiliki penyatuan non-sepele seperti yang dijelaskan di atas atau yang setara. Tanpa ini, jenis baris sedikit lebih dari tuple bersarang. Catatan, tipe baris tidak tergantung pada polimorfisme parametrik; Saya tidak bermaksud menyiratkan variabel baris. Dari argumen tentang$(\cong)$di atas, subtyping struktural menyiratkan jenis baris tetapi tidak sebaliknya. Polimorfisme parametrik bersifat ortogonal (dalam arti Anda dapat memiliki atau tidak memilikinya, pasti ada interaksi) dengan tipe baris atau subtipe struktural. Sebuah sistem dengan struktural subtyping + parametrik polimorfisme merangkum tipe baris + parametrik polimorfisme (dengan asumsi beberapa jenis "serikat rekaman") dalam arti bahwa setiap istilah dalam yang terakhir dapat diketik dengan jenis yang sama di yang sebelumnya. Yang pertama hanya bisa mengetik dengan tipe tambahan juga. Menggunakan contoh Brian, dalam suatu sistem dengan struktural subtyping dan parametrik polimorfisme answerakan memiliki tipe yang sama seperti pada versi pengetikan baris, tetapi juga akan memiliki tipe versi subtyping juga .

Jadi Anda mungkin ingin membandingkan tipe baris + polimorfisme parametrik dengan subtyping struktural tanpa polimorfisme parametrik. Manfaat utama dari yang pertama (dan kadang-kadang kelemahan) adalah memungkinkan Anda untuk menyebarkan informasi secara global . Ketika akan dipakai untuk , segala sesuatu yang pernah bersatu dengan itu akan dipakai juga. Ini dapat meresap hingga ke akar aplikasi Anda. Membawa variabel baris melalui bagian besar kode tidak jarang. Pendekatan Subtyping adalah melupakan$\rho${ c : Number }informasi: beralih dari subtipe ke supertipe kehilangan informasi (jenis). Ini seringkali bisa seperti yang Anda inginkan: ada tipe umum yang Anda pedulikan dan yang lainnya adalah detail yang tidak relevan. Bias saya adalah mempertahankan sebanyak mungkin jenis informasi dan hanya membuangnya secara eksplisit. Kelemahan dari pendekatan subtyping sering dibuktikan dengan program-program yang bertipe benar tetapi hanya karena tipe-tipe didorong ke tipe "top" (n tanpa informasi), misalnya catatan kosong. Pengulangan, polimorfisme parametrik (secara umum) mempertahankan informasi jenis, subtyping sengaja kehilangannya.