Subtipe implisit vs eksplisit

Halaman ini menegaskan hal itu

banyak bahasa tidak menggunakan subtyping implisit (ekuivalensi struktural), lebih memilih subtyping eksplisit / dinyatakan (deklarasi ekuivalensi)

Saya sebagian besar menggunakan bahasa pemrograman yang menggunakan subtyping eksplisit . Apa keuntungan dari subtyping implisit, seperti yang dijelaskan dalam catatan di atas.

pl.programming-languages type-theory Frankie Ribery
sumber

Dari FAQ, pada lingkup pertukaran ini: "Pekerjaan di bidang ini sering dibedakan dengan penekanannya pada teknik matematika dan kekakuan." Saya downvoting karena saya tidak melihat ruang untuk ketelitian dalam jawaban atas pertanyaan ini.

David Eppstein

Sayangnya, ada jauh lebih banyak ruang untuk ketelitian dalam menjawab pertanyaan ini daripada yang mungkin Anda harapkan pada awalnya. Banyak orang yang sangat terkenal membakar banyak tahun 90-an bergulat dengan pertanyaan-pertanyaan yang tampaknya sepele tentang subtipe. Sayangnya, ini adalah wilayah dengan rasio upaya-terhadap-hadiah yang sangat buruk.

Neel Krishnaswami

ya, ada banyak ruang untuk matematika dan ketelitian dalam menjawab pertanyaan ini, atau setidaknya untuk menjelaskan secara matematis apa subtyping tersirat itu . Saya tidak yakin tentang rasio upaya-untuk-hadiah.

Noam Zeilberger

Saya mungkin seharusnya mengatakan itu "sangat sulit", karena setelah refleksi saya sadar saya sangat tertarik dengan jawabannya.

Neel Krishnaswami

Oke, saya yakin. Saya akan menghapus downvote saya, tetapi sistem tidak membiarkan saya.

David Eppstein

Jawaban:

Jawaban singkatnya adalah "untuk memverifikasi properti tambahan dari kode yang ada". Jawaban yang lebih panjang mengikuti.

Saya tidak yakin "implisit" vs "eksplisit" adalah terminologi yang baik. Perbedaan ini kadang-kadang disebut subtyping "struktural" vs "nominal". Kemudian ada juga perbedaan kedua dalam kemungkinan interpretasi subtyping struktural (dijelaskan secara singkat). Perhatikan bahwa ketiga interpretasi subtyping benar-benar ortogonal, sehingga tidak masuk akal untuk membandingkannya satu sama lain, daripada memahami penggunaan masing-masing.

Perbedaan operasional utama dalam menafsirkan hubungan subtyping struktural A <: B adalah apakah itu disaksikan oleh paksaan nyata dengan konten komputasi (runtime / compiletime), atau apakah itu dapat disaksikan oleh paksaan identitas. Jika yang pertama, properti teoretis penting yang harus dimiliki adalah "koherensi", yaitu, jika ada beberapa cara untuk menunjukkan bahwa A adalah subtipe substruktural dari B, masing-masing paksaan yang menyertainya harus memiliki konten komputasi yang sama.

Tautan yang Anda berikan tampaknya memiliki interpretasi kedua tentang subtyping struktural dalam pikiran, di mana A <: B dapat disaksikan oleh pemaksaan identitas. Ini kadang-kadang disebut "subset interpretasi" dari subtyping, mengambil pandangan naif bahwa suatu tipe mewakili satu set nilai, dan jadi A <: B kalau-kalau setiap nilai tipe A juga merupakan nilai tipe B. Itu juga kadang-kadang disebut "mengetik perbaikan", dan makalah yang baik untuk membaca untuk motivasi asli adalah jenis Refemanement Freeman & Pfenning untuk ML . Untuk inkarnasi yang lebih baru di F #, Anda dapat membaca Bengston et al, tipe perbaikan untuk implementasi yang aman. Ide dasarnya adalah untuk mengambil bahasa pemrograman yang ada yang mungkin (atau mungkin tidak) sudah memiliki tipe tetapi di mana tipe tidak menjamin semua yang banyak (misalnya, hanya keamanan memori), dan mempertimbangkan lapisan kedua jenis memilih subset dari program dengan properti tambahan, lebih tepat.

(Sekarang, saya berpendapat bahwa teori matematika di balik interpretasi subtyping ini masih belum dipahami sebagaimana mestinya, dan mungkin itu karena penggunaannya tidak dihargai secara luas sebagaimana mestinya. Satu masalah adalah bahwa "set interpretasi tipe nilai terlalu naif, sehingga terkadang diabaikan dan tidak disempurnakan. Untuk argumen lain bahwa interpretasi subtyping ini layak mendapat perhatian matematis, bacalah pengantar Subspaces Paul Taylor dalam Abstrak Dualitas Batu .)

Noam Zeilberger
sumber

A \times B \times C <: A \times B

$A \times B \times C <: A \times B$

C

$C$

A

$A$

B

$B$

Ini adalah tugas pengoptimal untuk mengetahui tata letak memori yang optimal, sehingga paksaan yang merupakan identitas harus benar-benar hasil dari optimasi.

Andrej Bauer

jadi hanya untuk memperjelas komentar Andrej sehubungan dengan jawaban saya, dalam interpretasi mengetik penyempurnaan, hubungan subtipe selalu disaksikan oleh pemaksaan identitas menurut definisi , karena tipe penyempurnaan tidak membawa konten komputasi tambahan. Dengan kata lain, jika A dan B adalah dua penyempurnaan ("himpunan bagian" / "properti") dari jenis nilai X, A <: B menyatakan bahwa untuk setiap nilai x dalam X, jika x: A maka juga x: B. Pernyataan seperti itu dapat diverifikasi atau dipalsukan, tetapi tidak memiliki efek pada saat runtime, karena bukti bahwa x: A dan x: B tidak ada saat runtime.

Noam Zeilberger

N

$\mathbb{N}$

{x : N | x < 2^{32}}

$\{x:N\;\;|\;\;x < 2^{32}\}$

N

$N$

{x : N | x < 2^{32}}

$\{x:N | x < 2^{32}\}$

N

$N$

{x : N | x < 2^{32}}

$\{x:N | x < 2^{32}\}$

Noam Zeilberger

Jawaban ini adalah semacam suplemen minimal untuk jawaban luar biasa Noam. Salah satu titik data yang menarik adalah nasib konsep C ++, yang kandas pada upaya untuk menyatukan gagasan nominal dan struktural jenis.

Ada artikel yang bagus di sini, dengan tautan ke banyak diskusi yang relevan: http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/

Namun, penulisan di atas tidak membahas masalah nominal vs struktural secara mendalam. Ada langganan lain di sini, yaitu: http://nerdland.net/2009/07/alas-concepts-we-hardly-knew-ye/

Makalah utama yang sama-sama menunjuk pada Bjarne Stroustrup adalah “Penyederhanaan Penggunaan Konsep”: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2906.pdf , yang masuk ke dalam praktik masalah yang dihadapi secara mendalam.

Secara keseluruhan, diskusi lebih pragmatis daripada keras. Namun, ini memberikan wawasan yang baik tentang jenis pengorbanan yang terlibat dalam masalah ini, terutama dalam konteks bahasa besar yang ada.

sclv
sumber