Tes vs Jenis - Versi karat

Beberapa hari yang lalu 0xd34df00d telah menerbitkan terjemahan artikel tersebut , menjelaskan kemungkinan informasi tentang beberapa fungsi jika kita menggunakannya sebagai "kotak hitam", tidak mencoba membaca implementasinya. Tentu saja, informasi ini sangat berbeda dari bahasa ke bahasa; dalam artikel asli, empat kasus dipertimbangkan:

• Python - pengetikan dinamis, hampir tidak ada informasi dari tanda tangan, beberapa petunjuk diperoleh oleh tes;
• C - pengetikan statis lemah, sedikit informasi lebih lanjut;
• Haskell - pengetikan statis yang kuat, dengan fungsi murni secara default, lebih banyak informasi;
• Mengetik Idris - dependen, kompiler dapat membuktikan kebenaran fungsi.

"Ini C dan ada Haskell, dan bagaimana dengan Rust?" - ini adalah pertanyaan pertama dalam diskusi berikut. Jawabannya ada di sini.

Pertama-tama mari kita mengingat tugas:

Diberikan daftar nilai dan nilai, kembalikan indeks nilai dalam daftar atau tandakan bahwa itu tidak ada dalam daftar.

Jika seseorang tidak ingin tidak ingin membaca ini semua, contoh kode disediakan di taman bermain Rust .
Kalau tidak, mari kita mulai!

Pencarian sederhana

Pendekatan pertama adalah tanda tangan yang hampir naif, berbeda dari kode C hanya dalam beberapa elemen idiomatik:

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

Apa yang kita ketahui tentang fungsi ini? Yah, sebenarnya - tidak terlalu banyak. Tentu saja, Option<usize> sebagai nilai balik adalah peningkatan besar atas apa pun yang disediakan oleh C, tetapi tidak ada informasi tentang fungsi semantik. Secara khusus, kami tidak memiliki jaminan efek samping tidak ada dan tidak ada cara untuk memeriksa perilaku yang diinginkan.

Bisakah tes meningkatkan ini? Lihat di sini:

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

Tidak lebih, tampaknya - semua pemeriksaan ini bisa sama dengan Python (dan, untuk mengantisipasi, tes akan sedikit membantu untuk seluruh artikel).

Gunakan obat generik, Luke!

Tetapi apakah ada gunanya kita harus menggunakan hanya angka bertanda 32-bit? Memperbaikinya:

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

Ya, itu sesuatu! Sekarang kita dapat mengambil irisan apa pun, yang terdiri dari elemen-elemen dari jenis apa pun yang sebanding. Polimorfisme eksplisit hampir selalu lebih baik daripada yang implisit (halo, Python) dan hampir selalu lebih baik daripada tidak ada polimorfisme sama sekali (halo, C), kan?

Meskipun, fungsi ini mungkin secara tidak terduga lulus tes ini:

 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 mengisyaratkan pada satu titik yang hilang, karena spesifikasi menginginkan fungsi refl , pada kenyataannya, untuk selalu mengembalikan Some(0) . Tentu saja, ini semua disebabkan oleh perilaku spesifik dari tipe-tipe yang sepadan sebagian pada umumnya dan mengapung pada khususnya.
Mungkin kita ingin menyingkirkan masalah ini? Jadi, kami hanya akan memperketat ikatan pada tipe El:

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

Sekarang, kami tidak hanya membutuhkan jenis yang sebanding, - kami membutuhkan perbandingan ini untuk menjadi setara . Ini, tentu saja, membatasi jenis yang mungkin untuk digunakan dengan fungsi ini, tetapi sekarang tanda tangan dan tes mengisyaratkan bahwa perilaku tersebut harus sesuai dengan spesifikasi.

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

Seperti sebelumnya, tetapi sedikit lebih ketat

Tapi sekarang, mungkin kita perlu jaminan lagi. Atau kami ingin bekerja pada stack (dan karenanya tidak dapat menggunakan Vec ), tetapi perlu menggeneralisasi kode kami untuk setiap ukuran array yang memungkinkan. Atau kami ingin mengkompilasi fungsi yang dioptimalkan untuk setiap ukuran array beton.

Bagaimanapun, kita membutuhkan array generik - dan ada peti di Rust, memberikan itu .

Sekarang, ini kode kami:

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

Apa yang kita ketahui darinya? Kita tahu bahwa fungsi akan mengambil array dari beberapa ukuran tertentu, tercermin dalam tipenya (dan akan dikompilasi secara independen untuk setiap ukuran tersebut). Untuk saat ini, ini hampir tidak ada - jaminan yang sama diberikan pada saat runtime oleh implementasi sebelumnya.

Tapi kita bisa melangkah lebih jauh.

Aritmatika tingkat-jenis

Artikel awal menyebutkan beberapa jaminan yang diberikan oleh Idris yang tidak mungkin didapat dari bahasa lain. Salah satunya - dan mungkin yang paling sederhana, karena tidak melibatkan bukti atau tes, hanya sedikit perubahan jenis, - menyatakan bahwa nilai kembali, jika bukan Nothing - Nothing , akan selalu kurang dari panjang daftar.

Sepertinya jenis ketergantungan - atau sesuatu seperti itu - perlu untuk jaminan seperti itu, dan kita tidak bisa mendapatkan yang sama dari Rust, kan?

Memenuhi typenum . Dengan menggunakannya, kita dapat menulis fungsi kita dengan cara berikut:

 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>, { // Implementation elided } 

"Apa ini sihir hitam?!" - kamu bisa bertanya. Dan Anda benar: typenum adalah sihir hitam, dan segala upaya untuk menggunakannya bahkan lebih ajaib.

Tapi tanda tangan fungsi ini cukup konkret.

• Dibutuhkan array dari El dengan Ukuran panjang dan satu lagi El.
• Ini mengembalikan Opsi, yang, jika itu Beberapa,
  
  • memegang objek sifat , berdasarkan pada ciri UnsignedLessThan<Size> ;
  • dan UnsignedLessThan<T> diimplementasikan di mana pun Unsigned dan IsLess<T> diimplementasikan dan IsLess<T> mengembalikan B1, mis. true.

Dengan kata lain, fungsi ini dijamin untuk mengembalikan integer unsigned kurang dari ukuran array (secara tegas, ia mengembalikan objek sifat, tetapi kita dapat memanggil metode as_usize dan mendapatkan integer).

Sekarang saya dapat berbicara tentang dua peringatan utama:

1. Kita bisa kehilangan kinerja. Jika entah bagaimana fungsi ini akan berada di jalur "panas" program, pengiriman dinamis konstan mungkin memperlambat seluruh proses. Sebenarnya, ini mungkin bukan masalah besar, tapi ada yang lain:
2. Untuk mengkompilasi fungsi ini, kita harus menulis bukti kebenarannya di dalamnya, atau menipu sistem tipe dengan beberapa yang unsafe . Yang pertama cukup kompleks, dan yang terakhir hanya menipu.

Kesimpulan

Tentu saja, dalam praktiknya kita biasanya akan menggunakan pendekatan kedua (dengan irisan generik) atau pendekatan di spoiler (dengan iterator). Semua diskusi selanjutnya mungkin tidak menarik secara praktis dan di sini hanya sebagai latihan dengan tipe.

Bagaimanapun, fakta bahwa sistem tipe Rust dapat meniru fitur dari sistem tipe Idris yang lebih kuat, bagi saya, cukup mengesankan dengan sendirinya.