Pengetikan dinamis yang aman secara statis ala Python

Hai, Habr.

Suatu hari, di salah satu proyek hobi saya, tugas muncul menulis repositori metrik.

Tugas itu sendiri diselesaikan dengan sangat sederhana, tetapi masalah saya dengan Haskell (terutama dalam proyek untuk hiburan saya sendiri) adalah bahwa tidak mungkin untuk hanya mengambil dan menyelesaikan masalah. Adalah perlu untuk memutuskan, memperluas, abstrak, abstrak dan kemudian memperluas lebih lanjut. Oleh karena itu, saya ingin membuat penyimpanan metrik diperluas agar tidak menentukan sebelumnya apa yang akan ada di sana. Ini sendiri merupakan topik untuk artikel terpisah, dan hari ini kami akan mempertimbangkan satu bahan kecil: menulis pembungkus yang aman untuk jenis yang sebelumnya tidak dikenal. Sesuatu seperti mengetik dinamis, tetapi dengan jaminan statis bahwa kami tidak akan melakukan omong kosong.

Artikel ini, saya pikir, tidak akan membuka sesuatu yang baru untuk Haskellists berpengalaman, tapi sekarang kita setidaknya akan meletakkan bahan ini di luar kotak dan tidak akan terganggu olehnya di artikel berikutnya. Baik, atau Anda bisa tidak terlalu sederhana dan mengatakan bahwa saya sudah menemukan pola desain keseluruhan.

Jadi, pertama kita rumuskan masalahnya. Kita harus dapat mengaitkan beberapa objek dengan nilai dari tipe yang sebelumnya tidak diketahui. Atau, dengan kata lain, perlu bahwa nilai dari tipe yang sebelumnya tidak diketahui bertindak sebagai kunci dalam beberapa jenis peta.

Secara alami, kami tidak gila dan kami tidak akan membutuhkan dukungan nilai dari jenis apa pun. Kami mengharuskan jenis (bahkan jika tidak diketahui) mendukung perbandingan dalam arti pemesanan. Dalam istilah Haskell, ini berarti bahwa kami mendukung tipe a yang mengimplementasikan kelas Ord a .

Perhatikan bahwa kita dapat meminta dukungan untuk melakukan hash dan memeriksa kesetaraan, tetapi karena sejumlah alasan akan lebih mudah dan jelas untuk membatasi diri kita sebagai pembanding.

Ketika datang untuk menyimpan nilai yang dikenal untuk mengimplementasikan beberapa jenis kelas, tipe eksistensial biasanya digunakan di Haskell:

 data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd 

Jadi, jika kita diberi objek bertipe SomeOrd dan kita membuat pola yang cocok untuk itu:

 foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ... 

kemudian pada titik (1) kita tidak tahu tipe val yang mana, tetapi kita tahu (dan, yang terpenting, timer juga tahu) bahwa val mengimplementasikan timeclass Ord .

Namun, jika fungsi tipe kelas menyiratkan dua (atau lebih) argumen, maka penggunaan catatan semacam itu tidak banyak berguna:

 tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ? 

Untuk menggunakan metode Ord , perlu bahwa val dan val2 jenis yang sama, tetapi ini tidak harus dilakukan sama sekali! Ternyata SomeOrd kita SomeOrd berguna. Apa yang harus dilakukan

Terlepas dari kenyataan bahwa Haskell adalah bahasa yang dikompilasi dengan penghapusan tipe agresif (setelah kompilasi, mereka tidak ada di sana secara umum), kompilator masih dapat menghasilkan perwakilan tipe runtime jika ditanya tentang hal itu. Perwakilan peran tipe a adalah nilai tipe TypeRep a , dan permintaan generasi dijawab oleh typeclass Typeable .

Selain itu, jika kita memiliki dua contoh berbeda dari rep1 :: TypeRep a, rep2 :: TypeRep b , maka kita dapat membandingkannya dan memeriksa apakah mereka mewakili jenis yang sama atau tidak. Apalagi jika mereka benar-benar mewakili tipe yang sama, maka jelas bertepatan dengan b . Dan, yang paling penting, fungsi memeriksa representasi tipe untuk kesetaraan menghasilkan hasil yang dapat meyakinkan juru ketik ini:

 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) 

Omong kosong apa yang tertulis di sini?

Pertama, eqTypeRep adalah sebuah fungsi.

Kedua, polimorfik, tetapi tidak hanya berdasarkan jenis, tetapi juga oleh varietas jenis ini. Ini ditunjukkan oleh bagian forall k1 k2 (a :: k1) (b :: k2) - ini berarti bahwa a dan b tidak hanya tipe biasa seperti Int atau [String] , tetapi juga, misalnya, konstruktor terkenal (lihat DataKinds dan upaya lain untuk membuat Haskell tersertifikasi). Tapi kami tidak membutuhkan semua ini.

Ketiga, ia menerima dua representasi runtime dari tipe yang berpotensi berbeda, TypeRep a dan TypeRep b .

Keempat, mengembalikan nilai tipe Maybe (a :~~: b) . Hal paling menarik terjadi di sini.

Jika jenisnya tidak cocok, maka fungsinya mengembalikan Nothing biasa, dan semuanya baik-baik saja. Jika jenisnya cocok, maka fungsi mengembalikan Just val , di mana val bertipe a :~~: b . Mari kita lihat apa itu:

 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a 

Sekarang mari kita bicara. Misalkan kita mendapatkan nilai val dari tipe a :~~: b . Bagaimana itu bisa dibangun? Satu-satunya cara adalah dengan konstruktor HRefl , dan konstruktor ini mensyaratkan bahwa di kedua sisi ikon :~~: itu harus sama. Karena itu, bertepatan dengan b . Apalagi, jika kita zapternnom-match on val , maka taypcheker akan mengetahuinya juga. Oleh karena itu, ya, fungsi eqTypeRep mengembalikan bukti bahwa dua tipe yang berpotensi berbeda adalah sama jika sebenarnya sama.

Namun, dalam paragraf di atas, saya berbohong. Tidak ada yang menghentikan kita dari menulis di Haskell

 wrong :: Int :~~: String wrong = wrong --    

atau

 wrong :: Int :~~: String wrong = undefined 

atau hancurkan sistem dengan banyak cara yang kurang jelas. Ini adalah salah satu manifestasi yang terkenal di kalangan sempit yang mengatakan bahwa Haskell tidak konsisten sebagai logika. Dalam bahasa dengan sistem tipe yang lebih kuat, definisi seperti itu tidak dicap.

Itulah sebabnya dalam bagian dokumentasi yang dikutip di atas, nilai terminating disebutkan. Kedua varian implementasi wrong atas tidak menghasilkan nilai yang sangat terminasi ini, yang memberi kita sedikit alasan dan kepercayaan: jika program kita di Haskell dihentikan (dan tidak mengalami undefined ), maka hasilnya sesuai dengan jenis yang ditulis. Namun, di sini ada beberapa detail yang terkait dengan kemalasan, tetapi kami tidak akan membuka topik ini.

Dan omong-omong, manifestasi kedua dari kelemahan Haskell dalam kode di atas adalah jenis fungsi eqTypeRep . Dalam bahasa yang lebih kuat, itu akan mengembalikan nilai dari tipe yang lebih kuat, yang tidak hanya akan membuktikan kesetaraan jenis jika mereka benar-benar sama, tetapi juga akan membuktikan ketidaksetaraan mereka jika mereka sebenarnya tidak setara. Namun, ketidakkonsistenan dari logika Haskell membuat fungsi-fungsi seperti itu menjadi sedikit tidak berguna: itu semua penting ketika Anda menggunakan bahasa sebagai pembuktian teorema, dan bukan sebagai bahasa pemrograman, dan tidak menggunakan Haskell sebagai pembanding.

Oh well, cukup dari teori log dan ketik, mari kita kembali ke metrik kami. Sekarang hanya menggambar burung hantu Diskusi di atas mengisyaratkan bahwa itu cukup untuk menyimpan dalam tipe eksistensial kita juga ini adalah representasi paling runtime dari tipe tersebut, dan semuanya akan baik-baik saja.

Ini membawa kita ke implementasi tipe pembungkus berikut:

 data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val 

Sekarang kita menulis fungsi yang mengambil yang berikut:

1. dua nilai tipe Dyn ;
2. fungsi yang menghasilkan sesuatu untuk dua nilai dari jenis apa pun ,
   hanya berdasarkan konstanta yang disebutkan saat membuat Dyn ( forall bertanggung jawab untuk ini),
   dan yang disebut jika kedua Dyn menyimpan nilai dari tipe yang sama;
3. dan fungsi fallback, yang disebut bukan yang sebelumnya, jika jenisnya masih berbeda:

 withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

SomeTypeRep adalah pembungkus eksistensial atas TypeRep a untuk a .

Sekarang kita dapat menerapkan, misalnya, pengecekan dan perbandingan kesetaraan:

 instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare 

Di sini kami mengambil keuntungan dari fakta bahwa SomeTypeRep dapat dibandingkan satu sama lain, sehingga fungsi mundur untuk pemesanan juga compare .

Selesai

Hanya sekarang ini dosa untuk tidak menggeneralisasi: kami mencatat bahwa di dalam Dyn , toDyn , withDyns kami tidak menggunakan Ord secara khusus, dan ini bisa berupa rangkaian konstanta lain, sehingga kami dapat mengaktifkan ekstensi ConstraintKinds dan menggeneralisasi dengan parameterisasi Dyn serangkaian pembatasan tertentu yang kami dibutuhkan dalam tugas khusus kami:

 data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

Kemudian Dyn Ord akan menjadi tipe Dyn Monoid , dan, katakanlah, Dyn Monoid akan memungkinkan Anda untuk menyimpan monoid yang sewenang-wenang dan melakukan sesuatu yang monoidal dengannya.

Mari kita menulis contoh yang kita butuhkan untuk Dyn baru kita:

 instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare 

... hanya ini yang tidak berfungsi. Typecher tidak tahu bahwa Dyn Ord juga mengimplementasikan Eq ,
karena itu Anda harus menyalin seluruh hierarki:

 instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare 

Nah, sekarang sudah pasti.

... mungkin, dalam Haskell modern, Anda dapat membuatnya sehingga timer itu sendiri menampilkan contoh formulir

 instance C_i (Dyn (C_1, ... C_n)) where ... 

karena ada sesuatu yang prologikal keluar, tetapi saya belum melakukannya, saya harus duduk memetiknya. Tetap disini.

Dan juga, jika Anda dengan hati-hati menyipitkan mata, Anda dapat melihat bahwa Dyn kami terlihat mencurigakan seperti pasangan jenis yang bergantung (ty : Type ** val : ty) dari bahasa samar. Tetapi hanya dalam bahasa yang saya kenal tidak mungkin untuk mencocokkan jenisnya, karena parametrikitas (yang dalam hal ini, IMHO, ditafsirkan terlalu luas), tetapi di sini tampaknya mungkin.

Tapi yang paling penting - sekarang Anda dapat dengan aman memiliki sesuatu seperti Map (Dyn Ord) SomeValue dan menggunakan nilai apa pun sebagai kunci, selama mereka sendiri mendukung perbandingan. Misalnya, pengidentifikasi dengan deskripsi metrik dapat digunakan sebagai kunci, tetapi ini adalah topik untuk artikel selanjutnya.