Hai, Habr. Suatu hari saya sedang mencari cara melakukan sesuatu di Idris, dan menemukan posting yang bagus, terjemahan gratis yang sepertinya cukup sesuai. Kebebasan dan lelucon jika perlu, saya akan tunjukkan "di sini oleh coretan seperti di awal dan di akhir".
Kapan menggunakan tes, dan kapan - mengetik? Informasi apa dan jaminan apa yang kami terima sebagai imbalan atas upaya kami untuk menuliskannya?
Kita akan melihat contoh sederhana dan sedikit dibuat-buat diekspresikan dalam Python, C, Haskell, dan Idris. Kami juga akan melihat apa yang bisa dikatakan tentang implementasi tanpa pengetahuan tambahan tentang hal itu, dalam setiap kasus.
Kami tidak akan mempertimbangkan berbagai pintu belakang yang memungkinkan kami untuk secara eksplisit melanggar jaminan bahasa (misalnya, ekstensi C, unsafePerformIO di Haskell, konversi jenis tidak aman), jika tidak, tidak mungkin untuk menarik kesimpulan sama sekali, dan posting ini akan cukup singkat. ⟦Selain itu, Haskell yang sama memiliki subset Safe Haskell yang secara eksplisit dan transitif melarang penggunaannya dan sejumlah trik lain yang dapat melanggar integritas bahasa.⟧
Spesifikasi
Biarkan daftar dan beberapa makna diberikan. Diperlukan untuk mengembalikan indeks nilai ini dalam daftar atau menunjukkan bahwa nilai ini tidak ada dalam daftar.
Implementasi spesifikasi ini sepele, jadi wajar untuk bertanya, dan di sini umumnya tes atau tipe. Namun, sifat dan metode penalaran tersebut, yang akan kita bicarakan hari ini, dapat diterapkan pada kode yang jauh lebih kompleks. Biarkan implementasinya mengambil sepuluh ribu baris kode spaghetti yang tidak dapat dibaca, jika itu membantu untuk melihat kegunaannya.
Python
def x(y, z):
Kami segera mencatat bahwa kami tidak tertarik pada ⟦dan semantik yang tidak dicentang - tidak memengaruhi properti program seperti penamaan variabel dan dokumentasi teks, jadi saya sengaja tidak menulis kode yang membantu persepsi. Kami hanya tertarik pada kenyataan bahwa, setelah lulus tes dan mengetik cek, itu tidak bisa salah .
Dalam kode di atas, praktis tidak ada informasi berguna selain fakta bahwa kita memiliki fungsi yang mengambil dua argumen. Fungsi ini sama-sama dapat menemukan indeks nilai dalam daftar, atau dapat mengirim surat penghinaan kepada nenek Anda.
Analisis
Kita tidak hanya mendapatkan kode yang rapuh tanpa tes dan jenis, tetapi satu-satunya cara kita untuk memahami apa fungsi yang dilakukan adalah dokumentasi. Dan karena dokumentasi diperiksa oleh orang-orang, bukan oleh mesin, dapat dengan mudah berubah menjadi usang atau "awalnya tidak benar".
- Dokumentasi
- ✗ Kita tahu perilaku yang diharapkan
Kami tidak memiliki apa pun untuk memberi tahu kami tentang perilaku fungsi ini. Kamu membenci nenekmu. Kamu adalah monster.
- Garansi
- ✓ Keamanan Memori
Python adalah bahasa pengumpulan sampah yang menghilangkan masalah ini dari kami. ⟦Namun, sejauh yang saya tahu, tidak ada yang mencegah Anda menarik perpustakaan yang tidak aman atau C FFI di dalam fungsi ini.⟧
Python dengan tes
def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None
Sekarang kita tahu bahwa fungsi kita berfungsi, dan jika elemennya hilang, hasilnya adalah None ?
Ya ... tidak. Ini hanya satu contoh. Sayangnya, ruang lingkup fungsi kami tidak terbatas, dan tidak ada jumlah contoh yang dapat membuktikan operasi fungsi kami yang benar. Lebih banyak tes - lebih percaya diri, tetapi tidak ada jumlah tes yang akan menyelesaikan semua keraguan.
Kemungkinan bahwa fungsi ini akan mengembalikan None untuk 4 , tetapi tidak untuk 5 , kedengarannya agak delusi, dan dalam kasus khusus ini kemungkinan besar adalah omong kosong. Kita dapat puas dengan tingkat iman kita dan memikirkan sejumlah contoh tertentu. Tetapi sekali lagi, maka posting akan pendek, jadi mari kita bayangkan bahwa implementasinya tidak begitu jelas.
Karena tes tidak dapat membuktikan sesuatu dalam kasus umum, tetapi hanya menunjukkan perilaku dengan contoh spesifik, tes tidak dapat menunjukkan tidak adanya kesalahan. Misalnya, tidak ada tes yang akan menunjukkan bahwa fungsi kita tidak pernah melempar pengecualian atau tidak pernah memasuki siklus abadi, atau tidak mengandung tautan yang tidak valid. Ini hanya bisa menjadi analisis statis.
Namun, bahkan jika contoh-contohnya tidak terlalu bagus dalam peran bukti, mereka setidaknya merupakan dokumentasi yang baik. Dari dua contoh ini kita dapat memperoleh spesifikasi lengkap ⟦di bawah beberapa asumsi a priori tambahan - dua contoh tersebut juga memenuhi, misalnya, "counterspec" "menemukan elemen dalam array dan mengembalikan yang sebelumnya, jika ada", yang membutuhkan waktu sepuluh detik untuk saya ciptakan .
Analisis
Meskipun pengujian dapat menunjukkan cara menggunakan fungsi kami, dan juga memberikan sedikit kepercayaan diri bahwa fungsi ini bekerja dengan benar dengan setidaknya beberapa contoh, mereka tidak dapat membuktikan apa pun tentang kode kami dalam kasus umum. Sayangnya, ini berarti bahwa pengujian hanya membantu sebagian untuk menghindari kesalahan.
- Dokumentasi
- ✓ Kami memiliki contoh penggunaan
- ✓ Kami tahu beberapa kelas nilai yang akan diproses dengan benar
- ✗ Kami tahu semua jenis nilai yang akan diproses dengan benar
Kami tidak memiliki batasan pada jenis argumen, jadi meskipun ada contoh dari apa fungsi dapat menangani, kami tidak tahu jenis mana yang belum diuji. - ✗ Kita tahu perilaku yang diharapkan
⟦Penulis artikel asli dicentang di sini, saya akan membiarkan diri saya membuat tanda salib, memberikan komentar di atas⟧
- Spesifikasi
- ✓ Bekerja di setidaknya satu kasing
- ✗ Indeks yang dikembalikan selalu merupakan indeks yang valid
- ✗ Indeks yang dikembalikan selalu menunjukkan nilai yang sesuai
- ✗ Barang yang hilang selalu kembali
None / Nothing
- Kesalahan umum
- ✗ Tidak ada kesalahan ketik atau nama yang salah
Analisis statis dapat membantu, tetapi karena Python adalah bahasa yang dinamis dengan kemampuan untuk menimpa berbagai hal saat runtime, kami tidak pernah dapat membuktikan bahwa tidak ada kesalahan.
Secara khusus, bisa sangat sulit atau tidak mungkin untuk menentukan apakah nama metode sudah benar, karena validitas pemanggilan metode tergantung pada tipe runtime dari objek tempat pemanggilan dilakukan. - ✗ Tidak ada
null tidak terduga - ✗ Kasing kesalahan selalu ditangani
Dalam pengalaman saya, ini adalah salah satu sumber kesalahan yang paling umum: dalam contoh kami, fungsi mengembalikan None dalam kasus elemen yang hilang, tetapi kode yang menggunakan fungsi ini dapat mengasumsikan, misalnya, bahwa ia akan selalu mengembalikan angka. Selain itu, ini juga dapat menyebabkan pengecualian yang tidak tertangani.
- Garansi
- ✓ Keamanan Memori
- ✗ Fungsi tidak dapat dipanggil dengan jenis yang salah
- ✗ Tidak ada efek samping
- ✗ Tidak ada pengecualian
- ✗ Tidak ada kesalahan
- ✗ Tidak ada siklus abadi
Haskell
xyz =
Jika Anda tidak terbiasa dengan sintaks: ini adalah definisi fungsi x dengan parameter y dan z . Di Haskell, Anda dapat menghilangkan tipe, karena mereka akan disimpulkan dari implementasi ⟦kecuali, tentu saja, berbagai fitur canggih dari ekstensi modern dari sistem tipe digunakan .
Tampaknya ini tidak jauh berbeda dari versi Python, tetapi hanya berkat fakta bahwa kami menulis fungsi kami di Haskell dan itu adalah ubin, kami sudah dapat berbicara tentang beberapa properti yang menarik.
Analisis
Jelas, kita tidak bisa menarik begitu banyak kesimpulan di sini, tetapi berikut adalah beberapa hal yang perlu diperhatikan:
- Dokumentasi
- ✗ Kita tahu perilaku yang diharapkan
- Kesalahan umum
- ✓ Tidak ada kesalahan ketik atau nama yang salah
Karena Haskell adalah bahasa yang dikompilasi, semua nama harus diselesaikan pada waktu kompilasi. Program tidak akan mengkompilasi jika ada kesalahan ini. - ✓ Tidak ada
null tidak terduga
Haskell tidak memiliki null . Masalahnya terpecahkan!
- Garansi
- ✓ Keamanan Memori
- ✓ Fungsi tidak dapat dipanggil dengan jenis yang salah
- ✓ Tidak ada efek samping yang tidak terduga
⟦Penulis artikel asli tidak menunjukkan item ini, tetapi saya akan membiarkan diri saya untuk mencatat bahwa jika ada efek samping, jenis fungsi yang disimpulkan akan menunjukkan keberadaan mereka, sehingga kode panggilan akan mengetahui tentang kemampuan mereka.
Jenis Haskell menentukan
x :: Eq a => [a] -> a -> Maybe Int xyz =
Sebelumnya, kami berbicara tentang sikap agak licik terhadap keselamatan nenek: jelas dari tes bahwa fungsi tidak akan membahayakan siapa pun, tetapi apakah nenek benar - benar aman? Apakah fungsi ini secara akurat tidak mengirim surat sumpah?
Haskell dikenal sebagai bahasa fungsional murni. Ini tidak berarti bahwa kode tidak dapat memiliki efek samping, tetapi semua efek samping harus ada dalam jenisnya. Kami tahu jenis fungsi ini, kami melihat bahwa fungsinya bersih, jadi kami yakin bahwa fungsi ini tidak mengubah keadaan eksternal apa pun.
Ini adalah properti yang sangat menarik karena alasan lain: karena kita tahu bahwa tidak ada efek samping, kita dapat memahami apa fungsi ini, hanya berdasarkan tanda tangannya! Cukup cari tanda tangan Hoogle ini dan lihat hasil pertama. Tentu saja, ini bukan satu-satunya fungsi yang mungkin memiliki tipe seperti itu, tetapi tipe tersebut memberi kita kepercayaan diri yang cukup untuk keperluan dokumentasi.
Analisis
- Dokumentasi
- ✓ Kita tahu perilaku yang diharapkan
- ✗ Kami memiliki contoh penggunaan
- ✓ Kami tahu beberapa kelas nilai yang akan diproses dengan benar
- ✓ Kami tahu semua jenis nilai yang akan diproses dengan benar
- Spesifikasi
- ✗ Bekerja dalam setidaknya satu kasing.
Dengan tes atau bukti yang hilang, kami tidak tahu apakah fungsi kami berfungsi sama sekali seperti yang kami harapkan! - ✗ Indeks yang dikembalikan selalu merupakan indeks yang valid.
- ✗ Indeks yang dikembalikan selalu menunjukkan nilai yang sesuai.
- ✗ Barang yang hilang selalu kembali
None / Nothing .
- Kesalahan umum
- ✓ Tidak ada kesalahan ketik atau nama yang salah
- ✓ Tidak ada
null tidak terduga - ✓ Kasing kesalahan selalu ditangani
Jika fungsi kami mengembalikan Nothing , maka sistem jenis memastikan bahwa kasus ini ditangani dengan benar oleh kode panggilan. Tentu saja, kasus ini dapat diabaikan, tetapi ini harus dilakukan secara eksplisit.
- Garansi
- ✓ Keamanan Memori
- ✓ Fungsi tidak dapat dipanggil dengan jenis yang salah
- ✓ Tidak ada efek samping
- ✗ Tidak ada pengecualian
Saya berbagi pengecualian dan kesalahan, percaya bahwa setelah pengecualian dimungkinkan untuk pulih, dan setelah kesalahan (misalnya, fungsi yang didefinisikan sebagian) - tidak.
Sebagian besar, pengecualian dijelaskan dalam tipe (misalnya, dalam monad IO). Dalam cara yang baik, kita harus tahu bahwa suatu fungsi tidak akan membuang pengecualian, hanya berdasarkan jenisnya. Namun, Haskell mematahkan ekspektasi ini dengan membiarkan pengecualian dilemparkan dari kode murni .
"Selain itu, perlu dicatat bahwa di Haskell, kesalahan seperti salah memanggil fungsi yang didefinisikan sebagian juga disajikan sebagai pengecualian yang dapat ditangkap dan diproses, sehingga perbedaan antara kedua kategori sedikit kurang jelas." - ✗ Tidak ada kesalahan
Kita masih dapat menggunakan fungsi yang didefinisikan sebagian, misalnya, pembagian dengan nol. - ✗ Tidak ada siklus abadi
Haskell dengan tes
Ingat, saya katakan sebelumnya bahwa tes tidak dapat membuktikan tidak adanya kesalahan? Aku berbohong Ketika bintang-bintang bertemu dengan benar, dan jika tes dikombinasikan dengan jenis, maka itu menjadi mungkin! Bintang pertama adalah keterbatasan fungsi domain kita. Yang kedua - domain definisi seharusnya tidak hanya terbatas, tetapi juga tidak terlalu besar, jika tidak tes semacam itu akan sulit untuk dipraktikkan.
Sebagai contoh:
not :: Bool -> Bool not x = ...
Input dapat berupa True atau False . Sudah cukup untuk menguji dua opsi ini, dan ini dia, Holy Grail! Tidak ada pengecualian, siklus berulang, hasil salah, tidak ada kesalahan. ⟦Namun, untuk fungsi yang sedikit lebih kompleks, mungkin tidak jelas berapa banyak waktu yang dihabiskan untuk tes: jika mereka membutuhkan waktu lama untuk menyelesaikannya, apakah kita berakhir dalam siklus kekal, atau hanya berat? Masalah menghentikannya .⟧
Sebenarnya, ini juga tidak sepenuhnya benar dalam kasus Haskell: di setiap jenis Haskell ada juga nilai ⊥ (yang dapat diperoleh sebagai undefined , error atau dalam arti tertentu sebagai pengulangan tak terbatas), tetapi kaum Haskell secara tradisional menutup mata mereka dan percaya bahwa itu tidak ada.
Bacaan Ekstrakurikuler: Hanya Ada Empat Miliar Mengapung - Jadi Tes Semua Mereka!
Dalam kasus apa pun, dalam contoh asli kami, cakupannya tidak terbatas, jadi pengujian hanya dapat menunjukkan bahwa kode kami berfungsi untuk sekumpulan contoh terbatas.
Analisis
Dalam hal ini, pengujian melengkapi jenis dan memasukkan beberapa lubang di sistem jenis Haskell. Kami memiliki kepercayaan diri yang lebih besar pada kode kami dibandingkan dengan hanya menggunakan tes atau tipe.
C
/* C , int */ int x(int *y, size_t n, int z) { /* 10000 */ }
Kami menganggap C tidak tertarik pada sistem tipe lama. Dalam C, khususnya, jenis-jenis yang paling mungkin dibutuhkan bukan oleh programmer, tetapi oleh kompiler untuk membantunya menghasilkan kode lebih cepat.
Dalam contoh kita, kita tidak tahu fungsi apa yang akan kembali jika elemen tidak ditemukan. Kami harus mengandalkan tradisi atau dokumentasi (misalnya, dalam hal ini mungkin -1 ).
Kita juga bisa menggunakan argumen: dengan cara ini kita bisa mengembalikan kesalahan dan menyimpan nilai kembali ke argumen keluar ini. Ini adalah opsi yang sedikit lebih ekspresif, tetapi kita masih harus bergantung pada dokumentasi untuk memahami parameter mana yang dibaca dan mana yang ditulis. Dalam kedua kasus, sulit untuk memahami perilaku dengan melihat tipe.
/* , out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000 */ }
Analisis
Sistem tipe itu sendiri tidak memberi kami begitu banyak jaminan. Tentu saja, kami mendapatkan beberapa informasi dari tipe-tipe ini, tetapi bandingkan saja dengan case Haskell.
Idris
x : Eq x => List x -> x -> Maybe Int xyz = ...
Fungsi ini dari jenis yang sama seperti dalam kasus Haskell. Namun, dengan sistem tipe yang lebih ekspresif, kita dapat mencapai lebih banyak. Pilihan jenis dapat berbicara tentang implementasi.
%default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ...
Jenis ini dapat dibaca sebagai "beri saya daftar ukuran n dan beberapa nilai, dan saya akan mengembalikan nomor yang kurang dari n atau Nothing ." Ini memastikan bahwa fungsi mengembalikan indeks yang jelas tidak melampaui batas.
Selain itu, fungsi ini total, yaitu, timer telah memeriksa bahwa ia selalu berakhir. Ini menghilangkan siklus dan kesalahan abadi.
Analisis
- Spesifikasi
- ✗ Bekerja dalam setidaknya satu kasing.
- ✓ Indeks yang dikembalikan selalu merupakan indeks yang benar
- ✗ Indeks yang dikembalikan selalu menunjukkan nilai yang sesuai
- ✗ Barang yang hilang selalu kembali
None / Nothing
- Garansi
- ✓ Keamanan Memori
- ✓ Fungsi tidak dapat dipanggil dengan jenis yang salah
- ✓ Tidak ada efek samping
- ✗ Tidak ada pengecualian
- ✓ Tidak ada kesalahan
- ✓ Tidak ada siklus abadi
Idris dengan tes
Karena jenis bahasa Idris sama ekspresifnya dengan bahasa istilahnya ⟦(atau lebih tepatnya, bagian totalnya yang terbukti)⟧, perbedaan antara tes dan jenisnya kabur:
ex : x [1, 2, 3] 2 = Just 1 ex = Refl
Fungsi ini memiliki tipe x [1, 2, 3] 2 = Just 1 agak aneh x [1, 2, 3] 2 = Just 1 . Tipe ini berarti bahwa untuk pemeriksaan tipe yang berhasil, typer harus membuktikan bahwa x [1, 2, 3] 2 struktural sama dengan Just 1 . ⟦Dalam hal ini, buktinya sepele, karena cukup bagi tipper untuk menormalkan istilah di kedua sisi dari tanda yang sama, yang akan dilakukan dalam waktu terbatas karena totalitas semua fungsi yang digunakan, dan yang akan mengarah pada hasil unik karena Church-Rosser. Setelah itu, seseorang dapat menggunakan refleksivitas kesetaraan, yang merupakan Refl .⟧
Bahkan, kami menulis tes level type.
Idris dengan bukti
Untuk kelengkapan analisis, kita dapat menggunakan kekuatan penuh dari tipe dependen dan membuktikan implementasi kita (karena tipe dependen di Idris setara dengan sistem logis yang menyertakan logika first-order yang konstruktif).
Secara khusus, kami dapat membuktikan properti yang sebelumnya tidak dapat dijangkau oleh kami:
-- Eq DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... -- , `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ...
Ketik findIndexOk dapat dibaca sebagai “untuk semua tipe a sehingga memiliki perbandingan yang dapat ditentukan secara algoritmik ( DecEq ) untuknya, untuk vektor y elemen apa pun dari tipe a dengan panjang n apa pun dan nilai z tipe a : jika xyz mengembalikan indeks i , maka indeks ini terletak z , tetapi jika xyz mengembalikan Nothing , maka tidak ada elemen seperti itu di vektor sama sekali. "
⟦Sangat menarik bahwa penulis artikel asli memberikan jenis yang sedikit lebih lemah daripada yang diberikan di atas.⟧
Sekarang kita sudah menangkap semuanya! Apa kerugiannya? Nah, menulis semua bukti ini bisa sangat sulit.
Perbandingan
Opini
Menurut pendapat saya, penggunaan sistem tipe modern itu sendiri paling efektif dalam hal hubungan informasi yang diterima dan jaminan untuk upaya yang dikeluarkan. Jika Anda ingin menulis kode yang cukup andal, maka jenisnya dapat dibumbui dengan tes. Idealnya - dengan gaya QuickCheck.
Dengan tipe dependen, garis antara tes dan tipe menjadi kurang jelas. Jika Anda menulis perangkat lunak untuk Boeing atau untuk alat pacu jantung, mungkin berguna untuk menulis bukti.