Saya sedang mempelajari Haskell saat ini dan mencoba memahami proyek yang menggunakan Haskell untuk mengimplementasikan algoritma kriptografi. Setelah membaca Learn You a Haskell for Great Good online, saya mulai memahami kode dalam proyek itu. Kemudian saya menemukan saya terjebak pada kode berikut dengan simbol "@":
-- | Generate an @n@-dimensional secret key over @rq@.
genKey :: forall rq rnd n . (MonadRandom rnd, Random rq, Reflects n Int)
=> rnd (PRFKey n rq)
genKey = fmap Key $ randomMtx 1 $ value @n
Di sini, randomMtx didefinisikan sebagai berikut:
-- | A random matrix having a given number of rows and columns.
randomMtx :: (MonadRandom rnd, Random a) => Int -> Int -> rnd (Matrix a)
randomMtx r c = M.fromList r c <$> replicateM (r*c) getRandom
Dan PRFKey didefinisikan di bawah ini:
-- | A PRF secret key of dimension @n@ over ring @a@.
newtype PRFKey n a = Key { key :: Matrix a }
Semua sumber informasi yang dapat saya temukan mengatakan bahwa @ adalah pola as, tetapi bagian kode ini tampaknya tidak demikian. Saya telah memeriksa tutorial online, blog, dan bahkan laporan bahasa Haskell 2010 di https://www.haskell.org/definition/haskell2010.pdf . Tidak ada jawaban untuk pertanyaan ini.
Lebih banyak cuplikan kode dapat ditemukan dalam proyek ini menggunakan @ dengan cara ini juga:
-- | Generate public parameters (\( \mathbf{A}_0 \) and \(
-- \mathbf{A}_1 \)) for @n@-dimensional secret keys over a ring @rq@
-- for gadget indicated by @gad@.
genParams :: forall gad rq rnd n .
(MonadRandom rnd, Random rq, Reflects n Int, Gadget gad rq)
=> rnd (PRFParams n gad rq)
genParams = let len = length $ gadget @gad @rq
n = value @n
in Params <$> (randomMtx n (n*len)) <*> (randomMtx n (n*len))
Saya sangat menghargai bantuan apa pun dalam hal ini.
sumber
Jawaban:
Itu
@n
adalah fitur canggih dari Haskell modern, yang biasanya tidak dicakup oleh tutorial seperti LYAH, juga tidak dapat ditemukan dalam Laporan.Ini disebut aplikasi tipe dan merupakan ekstensi bahasa GHC. Untuk memahaminya, pertimbangkan fungsi polimorfik sederhana ini
Panggilan secara intuitif
dup
berfungsi sebagai berikut:a
x
dari jenis yang dipilih sebelumnyaa
dup
lalu menjawab dengan nilai tipe(a,a)
Dalam arti tertentu,
dup
dibutuhkan dua argumen: jenisa
dan nilaix :: a
. Namun, GHC biasanya dapat menyimpulkan jenisa
(misalnya darix
, atau dari konteks tempat kami menggunakandup
), jadi kami biasanya hanya menyampaikan satu argumendup
, yaitux
. Misalnya, sudahSekarang, bagaimana jika kita ingin lulus
a
secara eksplisit? Nah, dalam hal ini kita dapat mengaktifkanTypeApplications
ekstensi, dan menulisPerhatikan
@...
argumen yang mengandung tipe (bukan nilai). Itu adalah sesuatu yang ada pada waktu kompilasi, hanya - pada saat runtime argumen tidak ada.Mengapa kita menginginkan itu? Yah, terkadang tidak ada di
x
sekitar, dan kami ingin mendorong kompiler untuk memilih yang benara
. MisalnyaAplikasi tipe sering berguna dalam kombinasi dengan beberapa ekstensi lain yang membuat inferensi tipe tidak layak untuk GHC, seperti tipe ambigu atau tipe keluarga. Saya tidak akan membahasnya, tetapi Anda hanya dapat memahami bahwa kadang-kadang Anda benar-benar perlu membantu kompiler, terutama ketika menggunakan fitur tipe-level yang kuat.
Sekarang, tentang kasus spesifik Anda. Saya tidak memiliki semua detail, saya tidak tahu perpustakaan, tetapi sangat mungkin bahwa Anda
n
mewakili semacam nilai bilangan alami pada tingkat tipe . Di sini kita menyelam dalam ekstensi yang agak canggih, seperti yang disebutkan di atas plusDataKinds
, mungkinGADTs
, dan beberapa mesin ketik kelas. Meskipun saya tidak bisa menjelaskan semuanya, mudah-mudahan saya bisa memberikan wawasan dasar. Secara intuitif,mengambil sebagai argumen
@n
, semacam waktu kompilasi alami, yang tidak diteruskan saat runtime. Sebagai gantinya,dibutuhkan
@n
( waktu kompilasi), bersama dengan bukti yangn
memenuhi kendalaC n
. Yang terakhir adalah argumen run-time, yang mungkin mengekspos nilai aktualn
. Memang, dalam kasus Anda, saya kira Anda memiliki sesuatu yang agak miripyang pada dasarnya memungkinkan kode untuk membawa alami tingkat-jenis ke tingkat-jangka, pada dasarnya mengakses "tipe" sebagai "nilai". (Ngomong-ngomong, tipe di atas dianggap sebagai yang "ambigu" - Anda benar-benar perlu
@n
membuat ambigu.)Akhirnya: mengapa kita ingin lulus
n
pada level tipe jika kita kemudian mengkonversinya ke level term? Tidak akan lebih mudah untuk menuliskan fungsi sepertibukannya lebih rumit
Jawaban jujurnya adalah: ya, itu akan lebih mudah. Namun, memiliki
n
pada tingkat tipe memungkinkan kompiler untuk melakukan pemeriksaan yang lebih statis. Misalnya, Anda mungkin ingin tipe mewakili "integer modulon
", dan memungkinkan menambahkannya. Memilikiberfungsi, tetapi tidak ada pemeriksaan itu
x
dany
dari modulus yang sama. Kita mungkin menambahkan apel dan jeruk, jika kita tidak hati-hati. Kita malah bisa menulismana yang lebih baik, tetapi masih memungkinkan untuk memanggil
foo 5 x y
bahkan ketikan
tidak5
. Tidak baik. Sebagai gantinya,mencegah hal-hal yang salah. Compiler secara statis memeriksa semuanya. Kode lebih sulit digunakan, ya, tetapi dalam arti membuatnya lebih sulit untuk digunakan adalah intinya: kami ingin membuatnya mustahil bagi pengguna untuk mencoba menambahkan sesuatu dari modulus yang salah.
Kesimpulan: ini adalah ekstensi yang sangat canggih. Jika Anda seorang pemula, Anda harus perlahan-lahan maju menuju teknik-teknik ini. Jangan berkecil hati jika Anda tidak dapat memahami mereka hanya setelah belajar singkat, itu butuh waktu. Buat langkah kecil pada satu waktu, selesaikan beberapa latihan untuk setiap fitur untuk memahami intinya. Dan Anda akan selalu memiliki StackOverflow ketika Anda terjebak :-)
sumber