Tes atau tipe? - Versi karat

Beberapa hari yang lalu, 0xd34df00d menerbitkan terjemahan sebuah artikel di sini yang menjelaskan apa yang dapat Anda pelajari tentang suatu fungsi dalam berbagai bahasa, jika Anda menganggapnya sebagai "kotak hitam" tanpa menggunakan informasi tentang implementasinya (tetapi, tentu saja, tanpa menghentikannya menggunakan kompiler). Tentu saja, informasi yang diterima sangat tergantung pada bahasa - empat contoh dipertimbangkan dalam artikel asli:

• Python - diketik secara dinamis, informasi minimum, hanya tes yang memberikan beberapa petunjuk;
• C - diketik dengan lemah, tidak banyak informasi;
• Haskell - sangat diketik secara statis, dengan fungsi murni, lebih banyak informasi;
• Idris adalah bahasa dengan tipe dependen, ada cukup informasi untuk membuktikan kebenaran fungsi selama kompilasi.

"Ada C, ada Haskell, tapi di mana Rust?!" - segera pertanyaan diajukan. Jawabannya ada di bawah potongan.

Ingat kondisi masalah:

Biarkan daftar dan beberapa makna diberikan. Diperlukan untuk mengembalikan indeks nilai ini dalam daftar atau menunjukkan bahwa nilai ini tidak ada dalam daftar.

Untuk yang tidak sabar - semua opsi yang dibahas di bawah ini dapat dilihat di taman bermain Rust .
Ayo pergi!

Pencarian sederhana

Kita akan mulai dengan tanda tangan yang hampir naif, yang, pada kenyataannya, berbeda dari kode C hanya dalam beberapa elemen idiomatik:

fn foo(x: &[i32], y: i32) -> Option<usize> { // 10000    } 

Apa yang kita ketahui tentang fitur ini? Yah ... sebenarnya tidak terlalu banyak. Tentu saja, memiliki Option<usize> dalam nilai yang dikembalikan jauh lebih baik daripada yang diberikan C kepada kami, tetapi kami masih tidak memiliki informasi tentang semantik fungsi. Secara khusus, tidak ada jaminan bahwa tidak akan ada efek samping, juga tidak ada cara untuk memverifikasi perilaku yang diharapkan.

Bisakah tes tertulis yang benar memperbaiki situasi? Kami melihat:

 #[test] fn test() { assert_eq!(foo(&[1, 2, 3], 2), Some(1)); assert_eq!(foo(&[1, 2, 3], 4), None); } 

Secara umum, kami tidak mendapatkan sesuatu yang baru - semua pemeriksaan yang sama dapat dengan mudah kami lakukan dengan Python (dan, melihat ke depan, tes praktis tidak akan memberikan apa-apa di masa depan).

Gunakan obat generik, Luke!

Tetapi apakah benar-benar baik bahwa kita dipaksa untuk menggunakan nomor 32-bit yang sudah ditandatangani? Kekacauan. Kami memperbaiki:

 fn foo<El>(x: &[El], y: El) -> Option<usize> where El: PartialEq, { // 10000    } 

Ya! Ini sudah menjadi sesuatu. Sekarang kita bisa mengambil irisan, yang terdiri dari elemen apa saja yang bisa kita bandingkan untuk kesetaraan. Polimorfisme eksplisit hampir selalu lebih baik daripada implisit dan hampir selalu lebih baik daripada tidak ada, bukan?

Namun, fungsi seperti itu secara tak terduga dapat lulus tes berikut untuk kita:

 fn refl<El: PartialEq + Copy>(el: El) -> Option<usize> { foo(&[el], el) // should always return Some(0), right? } #[test] fn dont_find_nan() { assert_eq!(refl(std::f64::NAN), None); } 

Ini segera menunjukkan beberapa kelemahan pada bagian kami, karena sesuai dengan spesifikasi asli, panggilan seperti itu harus mengembalikan Some(0) . Tentu saja, masalah di sini adalah karena kekhususan jenis dengan perbandingan yang didefinisikan sebagian secara umum dan mengapung pada khususnya.
Misalkan sekarang kita ingin menyingkirkan masalah seperti itu - untuk ini kita hanya memperketat persyaratan untuk tipe El:

 fn foo<El>(x: &[El], y: El) -> Option<usize> where El: Eq, { // 10000    } 

Sekarang kami menuntut tidak hanya kemungkinan perbandingan untuk kesetaraan - kami mengharuskan perbandingan ini menjadi hubungan kesetaraan . Ini agak mempersempit kisaran parameter yang mungkin, tetapi sekarang kedua jenis dan tes menunjukkan (meskipun tidak secara eksplisit menunjukkan) bahwa perilaku yang diharapkan harus benar-benar masuk dalam spesifikasi.

 fn foo<'a, El: 'a>(x: impl IntoIterator<Item = &'a El>, y: El) -> Option<usize> where El: Eq, { // 10000    } 

Seperti sebelumnya, hanya lebih ketat

Namun, misalnya, jaminan yang ditawarkan oleh kompiler pada tahap yang sudah diketahui tidak cukup bagi kami. Atau, katakanlah, kami tidak ingin (karena satu dan lain hal) masuk ke tumpukan, tetapi ingin bekerja di tumpukan, yang berarti bahwa kami memerlukan array alih-alih vektor, tetapi pada saat yang sama kami ingin kode kami digeneralisasikan ke berbagai ukuran array . Atau kami ingin fungsi dioptimalkan sebanyak mungkin untuk setiap ukuran spesifik dari daftar input.

Singkatnya, kita memerlukan array generik - dan Rust sudah memiliki paket yang menyediakannya kata demi kata .

Sekarang kami memiliki kode berikut:

 use generic_array::{GenericArray, ArrayLength}; fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<usize> where El: Eq, Size: ArrayLength<El>, { // 10000    } 

Apa yang kita ketahui dari kode ini? Bahwa fungsi mengambil array dari beberapa ukuran tetap, tercermin dalam tipenya (dan dikompilasi secara independen untuk setiap ukuran tersebut). Sejauh ini, ini tidak banyak berubah - pada akhirnya, jaminan yang persis sama, tidak hanya pada tahap monomorphization, tetapi dalam runtime, disediakan versi sebelumnya dengan potongan.

Tapi kita bisa melangkah lebih jauh.

Jenis Aritmatika Tingkat

Artikel asli menyebutkan beberapa jaminan yang kami terima dari Idris dan tidak bisa didapatkan dari orang lain. Salah satunya - dan mungkin yang paling sederhana, karena untuk itu Anda bahkan tidak perlu menulis bukti lengkap atau tes penuh, tetapi cukup tentukan jenisnya sedikit, dikatakan bahwa nilai pengembaliannya, jika ada (mis. Jika bukan Nothing ), dijamin tidak melebihi panjang daftar input.

Tampaknya syarat yang diperlukan untuk jaminan semacam itu adalah adanya tipe-tipe dependen, yah, atau setidaknya semacam kesamaan, dan akan aneh mengharapkan sesuatu seperti ini dari Rust, kan?

Bertemu - typenum . Dengannya, fungsi kita dapat digambarkan seperti ini:

 use generic_array::{ArrayLength, GenericArray}; use typenum::{IsLess, Unsigned, B1}; trait UnsignedLessThan<T> { fn as_usize(&self) -> usize; } impl<Less, More> UnsignedLessThan<More> for Less where Less: IsLess<More, Output = B1>, Less: Unsigned, { fn as_usize(&self) -> usize { <Self as Unsigned>::USIZE } } fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<Box<dyn UnsignedLessThan<Size>>> where El: Eq, Size: ArrayLength<El>, { // 10000    } 

"Apa-apaan ini sihir hitam?!" - kamu bertanya. Dan Anda pasti benar: tipenum adalah ilmu hitam itu, dan upaya untuk menggunakannya setidaknya entah bagaimana secara waras adalah dua kali lipat.

Namun demikian, tanda tangan dari fungsi ini cukup jelas.

• Fungsi menerima array elemen El ukuran panjang dan satu elemen tipe El.
• Fungsi mengembalikan nilai Opsi, yang, jika beberapa,
  
  • Ini adalah objek sifat berdasarkan tipe UnsignedLessThan<T> , yang menerima tipe Ukuran sebagai parameter;
  • pada gilirannya, sifat UnsignedLessThan<T> diimplementasikan untuk semua jenis yang menerapkan Unsigned dan IsLess<T> untuk mana IsLess<T> mengembalikan B1, mis. benar

Dengan kata lain, dengan cara ini kami menulis sebuah fungsi yang dijamin untuk mengembalikan nomor non-negatif (tidak bertanda) lebih kecil dari ukuran asli array (atau lebih tepatnya, tentu saja, mengembalikan objek sifat yang sama ini, yang kemudian harus kita panggil metode as_usize , dijamin untuk mengembalikan nomor tersebut) .

Sebenarnya ada dua trik dalam pendekatan ini:

1. Kita dapat secara nyata kehilangan kinerja. Jika tiba-tiba, karena alasan tertentu, fungsi kita seperti itu ada di bagian "panas" dari program, kebutuhan konstan untuk panggilan dinamis mungkin merupakan salah satu operasi yang paling lambat. Namun, kelemahan ini mungkin tidak sepenting yang terlihat, tetapi ada yang kedua:
2. Agar fungsi ini dapat dikompilasi dengan benar, kita harus benar-benar menulis di dalamnya bukti kebenaran pekerjaannya, atau untuk "mengelabui" sistem tipe melalui unsafe . Yang pertama terlalu rumit untuk artikel hari Jumat, tetapi yang kedua hanyalah penipuan.

Kesimpulan

Tentu saja, dalam praktiknya, dalam kasus seperti itu, baik implementasi kedua (menerima sepotong tipe sewenang-wenang) atau implementasi di bawah spoiler (menerima objek iterable) akan digunakan. Semua argumen berikutnya hampir pasti tidak memiliki kepentingan praktis dan hanya berfungsi sebagai latihan dalam bekerja dengan sistem tipe.

Namun demikian, fakta bahwa pada sistem tipe Rust dapat dapat meniru salah satu fitur dari sistem tipe Idris yang jelas lebih kuat, menurut pendapat saya, cukup indikatif.