Halo semuanya!
Terlepas dari ketidakjelasan dan beberapa abstraksi dari topik yang dibahas hari ini - kami berharap dapat mendiversifikasi akhir pekan Anda. Di akhir posting, kami menempatkan tiga tautan dari penulis, memungkinkan Anda untuk berkenalan dengan pengetikan yang tergantung pada Idris, F * dan JavaScript
Terkadang sepertinya bahasa pemrograman tidak banyak berubah sejak tahun 60an. Ketika mereka memberi tahu saya tentang hal ini, saya sering mengingat berapa banyak alat dan fitur keren yang kami miliki, dan bagaimana mereka menyederhanakan kehidupan kami. Begitu saja: ini adalah debugger terintegrasi, dan tes unit, dan analisis statis, dan IDE keren, serta array yang diketik dan banyak lagi. Perkembangan bahasa adalah proses yang panjang dan progresif, dan tidak ada "peluru perak" yang dengannya perkembangan bahasa akan berubah sekali dan untuk semua.
Hari ini saya ingin memberi tahu Anda tentang salah satu tahap terakhir dalam proses yang sedang berlangsung ini. Teknologi yang sedang kita bicarakan ini sedang dieksplorasi secara aktif, tetapi semuanya menunjukkan bahwa teknologi itu akan segera berakar dalam bahasa-bahasa umum. Dan kisah kami dimulai dengan salah satu konsep paling mendasar dalam ilmu komputer: dengan
tipe .
Dunia tipe
Mengetik adalah salah satu dari hal-hal yang begitu tidak terpisahkan dari pemikiran kita sehingga kita bahkan tidak memikirkan konsep tipe seperti itu? Mengapa 1
int , tetapi jika Anda hanya meletakkan nilai ini dalam tanda kutip - dan itu berubah menjadi
string ? Apa itu "tipe" pada intinya? Seperti yang sering terjadi dalam pemrograman, jawabannya tergantung pada kata-kata dari pertanyaan.
Jenisnya beragam. Dalam beberapa sistem tipe, ada batas yang sangat jelas antara tipe dan nilai. Jadi, 3, 2, dan 1 adalah nilai
integer , tetapi
integer bukan nilai. Konstruk ini "tertanam" dalam bahasa dan pada dasarnya berbeda dari artinya. Tetapi, pada kenyataannya, perbedaan seperti itu tidak perlu dan hanya dapat membatasi kita.
Jika Anda membebaskan jenis dan mengubahnya menjadi kategori nilai lain, maka sejumlah kemungkinan luar biasa terbuka. Nilai dapat disimpan, dikonversi, dan diteruskan ke fungsi. Dengan demikian, akan memungkinkan untuk membuat fungsi yang menggunakan tipe sebagai parameter, membuat fungsi yang digeneralisasi: yang dapat bekerja dengan banyak tipe tanpa kelebihan beban. Anda dapat memiliki array nilai dari tipe yang diberikan, daripada berurusan dengan aritmatika aneh dari pointer dan tipe casting, seperti yang harus Anda lakukan dalam C. Anda juga dapat mengumpulkan tipe baru saat program berjalan dan memberikan fitur seperti deserialisasi JSON otomatis. Tetapi, bahkan jika Anda memperlakukan tipe sebagai nilai, Anda masih tidak bisa melakukan semua tipe itu dengan nilai. Jadi, beroperasi dengan instance pengguna, Anda dapat, misalnya, membandingkan nama mereka, memeriksa usia atau pengenal mereka, dll.
if user.name == "Marin" && user.age < 65 { print("You can't retire yet!") }
Namun, ketika Anda mencoba melakukan hal yang sama dengan tipe
User , Anda hanya bisa membandingkan nama tipe dan mungkin nama properti. Karena ini adalah tipe, bukan sebuah instance, Anda tidak dapat memeriksa nilai propertinya.
if typeof(user) == User { print("Well, it's a user. That's all I know") }
Betapa kerennya jika kita memiliki fungsi yang hanya mampu menerima daftar pengguna yang tidak kosong? Atau fungsi yang hanya akan menerima alamat email jika direkam dalam format yang benar? Untuk tujuan ini, Anda akan memerlukan jenis "array tidak kosong" atau "alamat email". Dalam kasus ini, ini adalah tipe yang bergantung pada nilai, mis. tentang
tipe dependen . Dalam bahasa umum, ini tidak mungkin.
Agar tipe dapat digunakan, kompiler harus memeriksanya. Jika Anda mengklaim bahwa variabel berisi integer, akan lebih baik jika tidak ada
string di dalamnya, jika tidak maka kompiler akan bersumpah. Pada prinsipnya, ini bagus, karena tidak memungkinkan kita untuk merayu. Memeriksa tipe cukup sederhana: jika suatu fungsi mengembalikan
integer , dan kami mencoba mengembalikan
"Marin" di dalamnya, maka ini adalah kesalahan.
Namun, dengan tipe dependen, segalanya menjadi lebih rumit. Masalahnya adalah kapan tepatnya kompiler memeriksa tipenya. Bagaimana dia bisa memastikan bahwa ada tepat tiga nilai dalam array, jika program belum berjalan? Bagaimana cara memastikan bahwa bilangan bulat lebih besar dari 3, jika belum ditetapkan? Ada
keajaiban untuk ini ... atau, dengan kata lain,
matematika . Jika dapat dibuktikan secara matematis bahwa himpunan angka selalu lebih besar dari 3, maka kompiler dapat memverifikasi ini.
Matematika di studio!
Induksi matematika digunakan untuk merumuskan bukti. Induksi memungkinkan kita untuk mengkonfirmasi kebenaran suatu pernyataan tanpa syarat. Misalnya, kami ingin membuktikan bahwa rumus matematika berikut berlaku untuk bilangan positif:
1 + 2 + 3 + ... + x = x * (x + 1) / 2
Ada kemungkinan x yang tak terhingga jumlahnya, jadi kami butuh waktu sangat lama untuk memeriksa semua angka secara manual. Untungnya, ini tidak perlu. Kami hanya perlu membuktikan dua hal:
- Pernyataan ini diamati untuk hari pertama. (Biasanya 0 atau 1)
- Jika pernyataan ini benar untuk angka
n , maka itu akan berlaku untuk angka berikutnya n + 1
Karena pernyataan tersebut diamati untuk angka pertama dan semua angka berikut, kita tahu bahwa itu benar untuk semua angka yang mungkin.
Untuk membuktikan ini tidak sulit:
1 = 1 * (1 + 1) / 2 1 = 1
Sekarang kita juga harus membuktikan bahwa pernyataan itu berlaku untuk semua angka lainnya. Untuk melakukan ini, anggap itu berfungsi untuk beberapa angka n, dan kemudian pastikan itu bekerja untuk n +1.
Anggap ungkapan berikut ini benar:
1 + 2 + 3 + ... + n = n * (n + 1) / 2
Lihat
n + 1 :
(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2
Dengan demikian, kita dapat mengganti
"(1 + 2 + 3 + ... + n)" persamaan di atas:
(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)
dan menyederhanakan untuk
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)
Karena kedua bagian ekspresi itu sama, kami memastikan bahwa pernyataan ini benar. Ini adalah salah satu cara di mana Anda dapat memverifikasi kebenaran pernyataan tanpa secara manual menghitung setiap kasus, dan itu berdasarkan prinsip ini bahwa jenis ketergantungan bekerja. Anda menulis pernyataan matematis untuk memastikan bahwa jenis tesis ini benar.
Keindahan dari pendekatan ini terletak pada kenyataan bahwa bukti matematika dapat dikeluarkan dalam bentuk program komputer - dan inilah yang kami butuhkan!
Kembali ke pemrograman
Jadi, kami menemukan bahwa beberapa hal dapat dibuktikan terlebih dahulu, lalu beralih ke nilai tertentu. Untuk melakukan ini dalam bahasa pemrograman, Anda perlu cara untuk mengekspresikan pernyataan ini dalam kode yang akan ditulis ke dalam sistem tipe itu sendiri, yaitu, tipe sistem perlu ditingkatkan.
Pertimbangkan sebuah contoh. Di sini kita memiliki fungsi append yang mengambil dua array dan menggabungkannya. Sebagai aturan, tanda tangan dari fungsi tersebut akan terlihat seperti ini:
append: (arr1: Array, arr2: Array) -> Array
Namun, hanya dengan melihat tanda tangan, kami tidak dapat memastikan implementasi yang benar. Fakta bahwa fungsi mengembalikan array tidak berarti melakukan sesuatu. Salah satu cara untuk memeriksa hasilnya adalah memastikan bahwa panjang array yang dihasilkan sama dengan jumlah panjang array parameter.
newArray = append([1], [2, 3]) assert(length(newArray) == 3)
Tetapi mengapa memeriksa ini pada waktu berjalan jika Anda dapat membuat batasan yang akan diperiksa pada waktu kompilasi:
append: (arr1: Array, arr2: Array) -> newArray: Array where length(newArray) == length(arr1) + length(arr2)
Kami menyatakan bahwa
append adalah fungsi yang mengambil dua argumen
Array dan mengembalikan argumen
Array baru, yang kami sebut
newArray . Hanya kali ini kami menambahkan peringatan bahwa panjang array baru harus sama dengan jumlah dari panjang semua argumen ke fungsi. Pernyataan yang kami miliki di atas pada saat runtime dikonversi untuk mengetik pada waktu kompilasi.
Kode di atas mengacu pada dunia tipe, bukan nilai, yaitu tanda
== menunjukkan perbandingan
length tipe yang dikembalikan, dan bukan nilainya. Agar mekanisme seperti itu berfungsi, panjang jenis yang dikembalikan harus memberi kami beberapa informasi tentang jumlah aktual.
Untuk memastikan pengoperasian mekanisme semacam itu, Anda perlu memastikan bahwa setiap nomor adalah tipe yang terpisah. Satu jenis hanya dapat berisi satu nilai: 1. Hal yang sama berlaku untuk Dua, Tiga, dan semua angka lainnya. Secara alami, pekerjaan seperti itu sangat melelahkan, tetapi untuk pekerjaan seperti itulah kami memiliki pemrograman. Anda dapat menulis kompiler yang akan melakukan ini untuk kami.
Setelah melakukan ini, Anda bisa membuat tipe terpisah untuk array yang mengandung 1, 2, 3 dan sejumlah elemen yang berbeda.
ArrayOfOne ,
ArrayOfTwo , dll.
Dengan demikian, Anda dapat mendefinisikan fungsi panjang, yang akan mengambil salah satu dari jenis array di atas dan memiliki tipe pengembalian bergantung dari
One untuk
ArrayOfOne ,
Two untuk
ArrayOfTwo , dll. untuk setiap nomor.
Sekarang kita memiliki tipe yang terpisah untuk panjang array tertentu, kita dapat memverifikasi (pada waktu kompilasi) bahwa kedua array memiliki panjang yang sama. Untuk melakukan ini, bandingkan tipenya. Dan karena tipe adalah nilai yang sama dengan yang lain, Anda dapat menetapkan operasi kepadanya. Anda dapat menentukan penambahan dua jenis spesifik dengan menetapkan bahwa jumlah
ArrayOfOne dan
ArrayOfTwo sama dengan
ArrayOfThree .
Itu semua informasi yang dibutuhkan oleh kompiler untuk memastikan bahwa kode yang Anda tulis sudah benar.
Misalkan kita ingin membuat variabel tipe
ArrayOfThree :
result: ArrayOfThree = append([1], [2, 3])
Kompiler dapat menentukan bahwa [1] hanya memiliki satu nilai, sehingga Anda dapat menetapkan tipe
ArrayOfOne . Itu juga dapat menetapkan
ArrayOfTwo ke [2, 3].
Kompiler tahu bahwa jenis hasil harus sama dengan jumlah dari jenis argumen pertama dan kedua. Dia juga tahu bahwa ArrayOfOne + ArrayOfTwo sama dengan ArrayOfTiga, yaitu, dia tahu bahwa seluruh ekspresi di sisi kanan identitas adalah tipe ArrayOfThree. Itu cocok dengan ekspresi di sebelah kiri, dan kompiler senang.
Jika kami menulis yang berikut:
result: ArrayOfTwo = append([1], [2, 3])
maka kompiler akan benar-benar tidak puas, karena ia akan tahu bahwa jenisnya tidak benar.
Pengetikan dependen sangat keren
Dalam hal ini, sejumlah besar bug tidak mungkin diijinkan. Dengan pengetikan bergantung, kesalahan per unit, akses ke indeks array tidak ada, pengecualian pointer nol, loop tak terbatas, dan kode rusak dapat dihindari.
Menggunakan tipe dependen, Anda dapat mengekspresikan hampir semua hal. Fungsi faktorial hanya akan menerima angka alami, fungsi
login tidak akan menerima baris kosong, fungsi
removeLast hanya akan menerima array yang tidak kosong. Selain itu, semua ini diperiksa sebelum Anda memulai program.
Masalah dengan pemeriksaan runtime adalah bahwa mereka gagal jika program sudah berjalan. Ini normal jika program dijalankan hanya oleh Anda, tetapi tidak oleh pengguna. Tipe dependen memungkinkan Anda untuk melakukan pemeriksaan ke tingkat tipe, sehingga kegagalan jenis ini selama eksekusi program menjadi tidak mungkin.
Saya pikir pengetikan dependen adalah masa depan bahasa pemrograman umum, dan saya tidak sabar untuk menunggu!
→
Idris→
F *→
Menambahkan Jenis Ketergantungan ke JavaScript