Apa alasan di balik menjadikan non-determinisme sebagai fitur Haskell?

Kita tahu bahwa di Prolog - predikat non-deterministik adalah fitur yang digunakan untuk mengurangi masalah kombinatorial .

Di Haskell kita melihat beberapa perilaku non-deterministik serupa dengan Prolog di Daftar Monad .

Dalam Haskell kita juga melihat non-determinisme dalam memilih urutan evaluasi thunk :

Tetapi tidak ada yang mengatakan pada GHC mana dari mereka yang harus dievaluasi terlebih dahulu, dan oleh karena itu GHC memiliki kebebasan penuh untuk memilih mana yang akan dievaluasi terlebih dahulu.

Ini menarik - dan agak membebaskan. Saya bertanya-tanya (terlepas dari mencampuri masalah logika seperti delapan ratu ) prinsip apa yang dilayaninya. Apakah ada ide besar atau masalah besar yang mereka coba selesaikan dengan non-determinisme?

Pertanyaan saya adalah: Apa alasan di balik menjadikan non-determinisme sebagai fitur Haskell?

Meskipun benar bahwa kedua aspek yang dikutip dalam pertanyaan muncul sebagai bentuk non-determinisme, mereka memang sangat berbeda dalam cara mereka bekerja dan dalam tujuan mereka. Karenanya setiap jawaban harus dibagi dalam dua bagian.

Urutan evaluasi

Haskell mengamanatkan tidak ada perintah eksekusi khusus dalam evaluasi thunks pada dasarnya karena dua alasan.

1. Pertama-tama, Haskell adalah bahasa murni fungsional, jadi Anda dijamin memiliki transparansi referensial (jika Anda tidak dipusingkan dengan unsafePerformIO& co.). Ini berarti bahwa evaluasi ekspresi apa pun, misalnya f x akan menghasilkan hasil yang sama tidak peduli berapa kali ia dievaluasi dan tidak peduli di mana bagian dari program itu dievaluasi (dengan asumsi fdan xmengikat nilai-nilai yang sama dalam lingkup yang dianggap, dari tentu saja). Karenanya mandat urutan eksekusi tertentu tidak akan memiliki tujuan , karena mengubahnya tidak akan menghasilkan efek yang dapat diamati dalam hasil program. Dalam hal ini, ini sebenarnya bukan bentuk nondeterminisme, setidaknya tidak ada bentuk yang dapat diamati satu, karena kemungkinan eksekusi yang berbeda dari program semuanya secara semantik setara.

Mengubah urutan eksekusi dapat, bagaimanapun, memiliki efek pada kinerja program, dan meninggalkan kompiler kebebasan memanipulasi order di kehendaknya adalah fundamental untuk mencapai kinerja luar biasa bahwa kompiler seperti GHC dapat memperoleh kompilasi sedemikian tinggi. bahasa tingkat Sebagai contoh, pikirkan tentang transformasi aliran-fusi klasik:

map f . map g = map (f.g)

Kesetaraan ini hanya berarti bahwa menerapkan dua fungsi ke daftar dengan mapmemiliki hasil yang sama daripada menerapkan sekali komposisi kedua fungsi tersebut. Ini hanya benar karena transparansi referensial, dan merupakan semacam transformasi yang selalu dapat dilakukan oleh kompilerberlaku, apa pun yang terjadi. Jika mengubah urutan eksekusi dari tiga fungsi memiliki efek pada hasil ekspresi, ini tidak akan mungkin. Di sisi lain, kompilasi dalam bentuk kedua dan bukan yang pertama dapat memiliki dampak kinerja yang sangat besar, karena menghindarkan pembuatan satu daftar sementara dan hanya melintasi daftar sekali saja. Fakta bahwa GHC dapat secara otomatis menerapkan transformasi semacam itu adalah konsekuensi langsung dari transparansi referensial dan urutan eksekusi yang tidak tetap dan itu adalah salah satu aspek kunci dari kinerja hebat yang dapat dicapai Haskell.

2. Haskell adalah bahasa yang malas . Ini berarti bahwa ungkapan tertentu tidak diperlukan untuk dievaluasi kecuali hasilnya benar-benar diperlukan, dan ini juga tidak akan pernah terjadi. Kemalasan adalah fitur yang terkadang diperdebatkan dan beberapa bahasa fungsional lainnya menghindarinya atau membatasinya untuk ikut serta, tetapi dalam konteks Haskell itu adalah fitur utama dalam cara bahasa tersebut digunakan dan dirancang. Kemalasan adalah alat lain yang ampuh di tangan pengoptimal kompiler, dan yang paling penting memungkinkan kode dikomposisi dengan mudah.

Untuk melihat apa yang saya maksud dengan kemudahan komposisi, pertimbangkan contoh ketika Anda memiliki fungsi producer :: Int -> [Int]yang melakukan beberapa tugas kompleks untuk menghitung daftar beberapa jenis data dari argumen input, dan consumer :: [Int] -> Intyang merupakan fungsi kompleks yang menghitung hasil dari daftar memasukan data. Anda telah menulisnya secara terpisah, mengujinya, mengoptimalkannya dengan sangat hati-hati, dan menggunakannya secara terpisah dalam berbagai proyek. Sekarang di proyek berikutnya kebetulan Anda harus memanggil consumerhasilproducer. Dalam bahasa yang tidak lazim, ini mungkin tidak optimal, karena ini mungkin merupakan tugas gabungan yang paling efisien dilaksanakan tanpa membangun struktur daftar sementara. Untuk mendapatkan implementasi yang dioptimalkan, Anda harus mengimplementasikan kembali tugas gabungan dari awal, menguji ulang, dan mengoptimalkannya kembali.

Dalam haskell ini tidak diperlukan, dan memanggil komposisi dari kedua fungsi consumer . produceritu baik-baik saja. Alasannya adalah bahwa program tersebut tidak diharuskan untuk benar-benar menghasilkan seluruh hasil producersebelum memberikannya kepada consumer. Bahkan, segera setelah consumerakan membutuhkan elemen pertama dari daftar inputnya, maka kode yang sesuai dari producerakan berjalan sejauh yang diperlukan untuk memproduksinya, dan tidak lebih. Ketika elemen kedua dibutuhkan, itu akan dihitung. Jika beberapa elemen tidak akan dibutuhkan consumer, itu tidak akan dihitung sama sekali, secara efektif menyimpan perhitungan yang tidak berguna. Eksekusi consumerdanproducerakan secara efektif disisipkan, tidak hanya menghindari penggunaan memori dari struktur daftar perantara, tetapi juga mungkin menghindari perhitungan yang tidak berguna, dan eksekusi mungkin akan mirip dengan versi gabungan tulisan tangan yang harus Anda tulis sendiri. Inilah yang saya maksud dengan komposisi . Anda memiliki dua keping kode yang teruji dan berkinerja baik dan Anda dapat menyusunnya untuk mendapatkan sepotong kode yang teruji dan berkinerja baik.

Monad yang tidak deterministik

Penggunaan perilaku nondeterministik yang disediakan oleh monad Daftar dan yang serupa malah sangat berbeda. Di sini intinya bukan menyediakan kompiler dengan cara mengoptimalkan program Anda, tetapi dengan jelas dan ringkas menyatakan perhitungan yang secara inheren nondeterministic.

Contoh yang saya maksudkan disediakan oleh antarmuka Data.Boolean.SatSolverperpustakaan. Ini menyediakan pemecah SAT DPLL yang sangat sederhana diimplementasikan di Haskell. Seperti yang Anda ketahui, menyelesaikan masalah SAT melibatkan menemukan penugasan variabel boolean yang memenuhi formula boolean. Namun, mungkin ada lebih dari satu penugasan semacam itu, dan orang mungkin perlu menemukan salah satu dari mereka, atau beralih ke semuanya, tergantung pada aplikasi. Oleh karena itu, banyak perpustakaan akan memiliki dua fungsi berbeda seperti getSolutiondan getAllSolutions. Pustaka ini sebagai gantinya hanya memiliki satu fungsi solve,, dengan tipe berikut:

solve :: MonadPlus m => SatSolver -> m SatSolver

Di sini, hasilnya adalah SatSolvernilai yang dibungkus di dalam monad dari tipe yang tidak ditentukan, yang bagaimanapun dibatasi untuk mengimplementasikan MonadPluskelas tipe. Tipe kelas ini adalah yang mewakili jenis nondeterminisme yang disediakan oleh daftar monad, dan pada kenyataannya daftar adalah contoh. Semua fungsi yang beroperasi pada SatSolvernilai mengembalikan hasil mereka terbungkus dalam MonadPlusinstance. Jadi misalkan Anda memiliki rumus p || !qdan Anda ingin menyelesaikannya dengan membatasi hasil yang disetel qbenar, maka penggunaannya adalah sebagai berikut (variabel diberi nomor alih-alih diidentifikasi dengan nama):

expr = Var 1 :||: Not (Var 2)

task :: MonadPlus m => m SatSolver
task = do
  pure newSatSolver
  assertTrue expr
  assertTrue (Var 2)

Perhatikan bagaimana instance monad dan notasi menutupi semua detail tingkat rendah tentang bagaimana fungsi mengelola SatSolverstruktur data, dan memungkinkan kami menyatakan dengan jelas maksud kami.

Sekarang, jika Anda ingin mendapatkan semua hasil, Anda cukup menggunakan solvedalam konteks di mana hasilnya harus daftar. Berikut ini akan mencetak semua hasil di layar (dengan asumsi Showinstance untuk SatSolver, yang tidak ada, tetapi maafkan saya saat ini).

main = sequence . map print . solve task

Namun, daftar bukan satu-satunya contoh MonadPlus. Maybeadalah contoh lain. Jadi jika Anda hanya perlu satu solusi, tidak peduli yang mana, Anda bisa menggunakannya solveseolah-olah itu mengembalikan Maybe SatSolvernilai:

main = case solve task of 
  Nothing -> putStrLn "No solution"
  Just result -> print result

Sekarang anggaplah Anda memiliki dua tugas yang dibangun, taskdan task2, dan Anda ingin mendapatkan solusi untuk keduanya. Sekali lagi semuanya menyatu untuk membuat komposisi balok yang sudah ada:

combinedTask = task <|> task2

di mana <|>adalah operasi biner yang disediakan oleh Alternativetypeclass, yang merupakan kelas super dari MonadPlus. Sekali lagi ini mari kita jelaskan maksud kita, menggunakan kembali kode tanpa perubahan. Nondeterminisme secara jelas dinyatakan dalam kode, tidak dikubur di bawah rincian tentang bagaimana nondeterminisme sebenarnya diimplementasikan. Saya sarankan Anda untuk melihat kombinator yang dibangun di atas Alternativekelas tipe untuk mendapatkan contoh lebih lanjut.

Daftar nondeterministik seperti daftar bukan hanya cara untuk mengekspresikan latihan yang bagus tetapi menawarkan cara untuk merancang kode yang elegan dan dapat digunakan kembali yang dengan jelas menyatakan niat dalam pelaksanaan tugas yang inheren nondeterministik.