“Bukti adalah sebuah program; formula yang dibuktikannya adalah tipe untuk program ”

Ini mungkin jenis pertanyaan filosofis, tetapi saya percaya bahwa ada jawaban yang objektif untuk itu.

Jika Anda membaca artikel wikipedia tentang Haskell, Anda dapat menemukan yang berikut:

Bahasa ini berakar pada pengamatan Haskell Curry dan keturunan intelektualnya, bahwa "bukti adalah program; rumus yang dibuktikannya adalah tipe untuk program"

Sekarang, yang saya tanyakan adalah: bukankah ini benar-benar berlaku untuk hampir semua bahasa pemrograman? Fitur apa (atau serangkaian fitur) dari Haskell yang membuatnya sesuai dengan pernyataan ini? Dengan kata lain, apa sajakah cara yang terlihat di mana pernyataan ini memengaruhi desain bahasa?

Konsep esensial berlaku secara universal dalam beberapa cara, ya, tetapi jarang dengan cara yang bermanfaat.

Pertama-tama, dari perspektif teori tipe ini diasumsikan, bahasa "dinamis" paling baik dianggap memiliki tipe tunggal , yang berisi (antara lain) metadata tentang sifat nilai yang dilihat oleh programmer, termasuk apa yang akan disebut oleh bahasa dinamis ini sebuah "tipe" sendiri (yang bukan merupakan hal yang sama, secara konseptual). Setiap bukti semacam itu cenderung tidak menarik, sehingga konsep ini sebagian besar relevan dengan bahasa dengan sistem tipe statis.

Selain itu, banyak bahasa yang diduga memiliki "sistem tipe statis" harus dianggap dinamis dalam praktiknya, dalam konteks ini, karena mereka mengizinkan inspeksi dan konversi jenis saat dijalankan. Secara khusus, ini berarti bahasa apa pun dengan dukungan bawaan untuk "refleksi" atau semacamnya. C #, misalnya.

Haskell tidak biasa dalam berapa banyak informasi yang diharapkannya diberikan oleh suatu tipe - khususnya, fungsi tidak dapat bergantung pada nilai apa pun selain dari yang ditentukan sebagai argumennya. Di dalam bahasa dengan variabel global yang bisa berubah, di sisi lain, fungsi apa pun dapat (berpotensi) memeriksa nilai-nilai itu dan mengubah perilaku yang sesuai. Jadi fungsi Haskell dengan tipe A -> Bdapat dianggap sebagai program miniatur yang membuktikan secara tidak Alangsung B; fungsi yang setara dalam banyak bahasa lain hanya akan memberi tahu kita hal itu Adan apa pun keadaan global yang digabungkan menyiratkan B.

Perhatikan bahwa sementara Haskell memang memiliki dukungan untuk hal-hal seperti tipe refleksi dan dinamis, penggunaan fitur tersebut harus ditunjukkan dalam tipe tanda tangan dari suatu fungsi; demikian juga untuk penggunaan negara global. Tidak ada yang tersedia secara default.

Ada beberapa cara untuk memecahkan hal-hal di Haskell juga, misalnya dengan memungkinkan pengecualian runtime, atau menggunakan operasi primitif non-standar yang disediakan oleh kompiler, tetapi yang datang dengan harapan kuat bahwa mereka hanya akan digunakan dengan pemahaman penuh dengan cara yang akan menang ' t merusak arti kode eksternal. Secara teori, hal yang sama dapat dikatakan untuk bahasa lain, tetapi dalam praktiknya dengan sebagian besar bahasa lain, keduanya lebih sulit untuk mencapai hal-hal tanpa "curang", dan kurang disukai untuk "menipu". Dan tentu saja dalam bahasa "dinamis" yang sebenarnya, semuanya tetap tidak relevan.

Konsep ini dapat diambil lebih jauh daripada di Haskell, juga.

Anda benar bahwa korespondensi Curry-Howard adalah hal yang sangat umum. Ada baiknya membiasakan diri dengan sedikit tentang sejarahnya: http://en.wikipedia.org/wiki/Curry-Howard_correspondence

Anda akan mencatat bahwa sebagaimana dirumuskan pada awalnya, korespondensi ini diterapkan terutama pada logika intuitionistic di satu sisi, dan kalkulus lambda yang diketik secara sederhana (STLC) di sisi lain.

Klasik Haskell - baik '98 atau bahkan versi sebelumnya, sangat dekat dengan STLC, dan sebagian besar ada terjemahan langsung yang sangat sederhana antara setiap ekspresi yang diberikan dalam Haskell dan istilah yang sesuai dalam STLC (diperpanjang dengan rekursi dan beberapa tipe primitif). Jadi ini membuat Curry-Howard sangat eksplisit. Hari ini, berkat ekstensi, terjemahan semacam itu adalah bisnis yang agak rumit.

Jadi, dalam arti tertentu, pertanyaannya adalah mengapa Haskell "menghendaki" masuk ke dalam STLC secara langsung. Dua hal yang terlintas dalam pikiran:

• Jenis. Tidak seperti Skema, yang juga merupakan semacam kalkulus lambda bergula (antara lain), Haskell sangat diketik. Ini berarti bahwa tidak ada istilah dalam Haskell klasik yang menurut definisi tidak dapat diketik dengan baik istilah dalam STLC.
• Kemurnian. Sekali lagi, tidak seperti Skema, tetapi seperti STLC, Haskell adalah bahasa yang murni dan transparan. Ini sangat penting. Bahasa dengan efek samping dapat disematkan ke dalam bahasa yang bebas efek samping. Namun, melakukannya adalah transformasi seluruh program, bukan hanya keinginan lokal. Jadi untuk memiliki korespondensi langsung , Anda perlu memulai dengan bahasa yang murni fungsional.

Ada juga cara penting di mana Haskell, seperti kebanyakan bahasa, gagal sehubungan dengan aplikasi langsung korespondensi Curry-Howard. Haskell, sebagai bahasa turing-complete, mengandung kemungkinan rekursi tak terbatas, dan karenanya non-terminasi. STLC tidak memiliki operator fixpoint, tidak turing-selesai, dan sangat normal - yang mengatakan bahwa tidak ada pengurangan istilah dalam STLC akan gagal untuk mengakhiri. Kemungkinan rekursi berarti bahwa seseorang dapat "menipu" Curry-Howard. Misalnya let x = x in xmemiliki tipeforall a. a- yaitu, karena tidak pernah kembali, saya bisa berpura-pura memberi saya apa saja! Karena kita selalu dapat melakukan ini di Haskell, itu berarti bahwa kita tidak dapat "percaya" sepenuhnya pada bukti apa pun yang terkait dengan program Haskell kecuali kita memiliki bukti terpisah bahwa program itu sendiri berakhir.

Silsilah pemrograman fungsional sebelum Haskell (terutama keluarga ML) adalah hasil dari penelitian CS yang berfokus pada membangun bahasa yang Anda dapat dengan mudah membuktikan hal-hal tentang (antara lain), penelitian yang sangat sadar dan berasal dari CH untuk memulai. Sebaliknya, Haskell telah bertindak sebagai bahasa host dan inspirasi bagi sejumlah asisten pembuktian yang sedang dikembangkan, seperti Agda dan Epigram, yang berakar pada perkembangan dalam teori tipe yang sangat terkait dengan garis keturunan CH.

Untuk perkiraan tingkat pertama, sebagian besar bahasa lain (lemah dan / atau tidak diketik) tidak mendukung penggambaran tingkat-bahasa yang ketat antara

• proposisi (yaitu tipe)
• sebuah bukti (yaitu program mendemonstrasikan bagaimana kita dapat membangun proposisi dari satu set primitif dan / atau lainnya yang lebih tinggi konstruksi)

dan hubungan yang ketat antara keduanya. Jika ada, jaminan terbaik yang diberikan oleh bahasa lain adalah

• dengan batasan terbatas pada input, bersama dengan apa pun yang terjadi di lingkungan pada saat itu, kita dapat menghasilkan nilai dengan batasan terbatas. (tipe statis tradisional, cf C / Java)
• setiap konstruk memiliki tipe yang sama (tipe dinamis, cf ruby ​​/ python)

Perhatikan bahwa berdasarkan jenis , kami merujuk pada proposisi , dan karenanya sesuatu yang menggambarkan informasi jauh lebih banyak daripada sekadar int atau bool . Dalam Haskell, ada budaya meresapi fungsi hanya dipengaruhi oleh argumen itu - tidak ada pengecualian *.

Untuk menjadi sedikit lebih ketat, ide umumnya adalah bahwa dengan menerapkan pendekatan intuitionistic yang kaku untuk (hampir) semua konstruksi program (yaitu kita hanya dapat membuktikan apa yang dapat kita buat), dan dengan membatasi sekumpulan konstruksi primitif dalam suatu seperti yang kita miliki

• proposisi yang ketat untuk semua primitif bahasa
• serangkaian mekanisme terbatas di mana primitif dapat digabungkan

Konstruksi Haskell cenderung memberikan alasan yang baik tentang perilaku mereka. Jika kita dapat membangun bukti (baca: fungsi) membuktikan bahwa Amenyiratkan B, ini memiliki sangat sifat yang berguna:

• itu selalu memegang (selama kita memiliki A, kita dapat membangun B)
• implikasi ini hanya bergantung pada A, dan tidak ada yang lain.

sehingga memungkinkan kita untuk berpikir tentang invarian lokal / global secara efektif. Untuk kembali ke pertanyaan awal; Fitur bahasa Haskell yang paling memudahkan pemikiran ini adalah:

• Kemurnian / Segmentasi efek ke dalam konstruksi eksplisit (efek keduanya diperhitungkan dan diketik!)
• Ketik Inference / Memeriksa dalam kompiler Haskell
• Kemampuan untuk menanamkan kontrol dan / atau aliran data invarian ke dalam proposisi / tipe yang sedang disiapkan oleh sebuah program untuk membuktikan: (dengan Polimorfisme, Tipe Keluarga, GADT, dll.)
• Integritas referensial

Tidak ada satupun yang semuanya unik untuk Haskell (banyak dari ide-ide ini sangat tua). Namun, ketika dikombinasikan bersama-sama dengan serangkaian abstraksi yang kaya di perpustakaan standar (biasanya ditemukan di kelas tipe), berbagai sugaring tingkat sintaksis dan komitmen yang ketat untuk kemurnian dalam desain program, kita berakhir dengan bahasa yang entah bagaimana berhasil menjadi keduanya cukup praktis untuk aplikasi dunia nyata , tetapi pada saat yang sama membuktikan lebih mudah untuk alasan tentang bahasa yang paling tradisional itu.

Pertanyaan ini pantas mendapat jawaban yang cukup dalam, dan saya tidak mungkin melakukannya dengan adil dalam konteks ini. Saya sarankan membaca lebih lanjut di wikipedia / dalam literatur:

• The Curry-Howard Isomorphism
• Kubus Lambda
• Teori Tipe Konstruktivisme / Intuitionistik
• Tinjauan Bob Harper tentang Trinitarianisme Komputasi

* NB: Saya mengabaikan / mengabaikan beberapa aspek rumit dari ketidakmurnian Haskell (pengecualian, non-terminasi, dll.) Yang hanya akan memperumit argumen.

Fitur apa? Sistem tipe (menjadi statis, murni, polimorfik). Titik awal yang baik adalah "Theorems for Free" karya Wadler. Efek yang terlihat pada desain bahasa? Tipe IO, kelas tipe.

The Kleene Hirarki menunjukkan kepada kita bahwa bukti-bukti yang tidak program.

Hubungan rekursif pertama adalah:

R1( Program , Iteration )  Program halts at Iteration.
R2( Theorem , Proof ) Proof proves a Theorem.

Hubungan enumerable rekursif pertama adalah:

(exists x) R1( Program , x )  Program Halts.
(exists x) R2( Theorem , x)   Theorem is provable.

Sehingga suatu program adalah teorema dan iterasi yang ada dimana program terhenti seperti bukti yang ada yang membuktikan teorema tersebut.

Program = Theorem
Iteration = Proof

Ketika suatu program diproduksi dengan benar dari suatu spesifikasi, kita harus dapat membuktikan bahwa itu memenuhi spesifikasi, dan jika kita dapat membuktikan suatu program memenuhi suatu spesifikasi maka itu adalah sintesis program yang benar. Jadi kami melakukan sintesis program jika kami membuktikan program memenuhi spesifikasi. Teorema bahwa program memenuhi spesifikasi adalah program di mana teorema merujuk ke program yang disintesis.

Kesimpulan palsu Martin Lof tidak pernah menghasilkan program komputer apa pun dan sungguh menakjubkan bahwa orang-orang percaya itu adalah metodologi sintesis program. Tidak ada contoh lengkap yang pernah diberikan tentang program yang disintesis. Spesifikasi seperti "input tipe dan output program tipe itu" bukan fungsi. Ada beberapa program seperti itu dan memilih satu secara acak bukanlah fungsi rekursif atau bahkan fungsi. Ini hanyalah upaya konyol untuk menunjukkan sintesis program dengan program konyol yang tidak mewakili program komputer nyata yang menghitung fungsi rekursif.