Apakah polimorfisme parametrik peringkat tinggi berguna?

Saya cukup yakin semua orang akrab dengan metode generik formulir:

T DoSomething<T>(T item)

Fungsi ini juga disebut parametrically polymorphic (PP), khususnya peringkat-1 PP.

Katakanlah metode ini dapat direpresentasikan menggunakan objek fungsi dari bentuk:

<T> : T -> T

Artinya, <T>berarti dibutuhkan satu parameter tipe, dan T -> Tberarti ia mengambil satu parameter tipe Tdan mengembalikan nilai dari tipe yang sama.

Maka yang berikut ini adalah fungsi peringkat-2 PP:

(<T> : T -> T) -> int 

Fungsi tidak mengambil parameter tipe itu sendiri, tetapi mengambil fungsi yang mengambil parameter tipe. Anda dapat melanjutkan ini secara iteratif, membuat sarang semakin dalam, semakin dalam, mendapatkan PP dengan peringkat yang lebih tinggi dan lebih tinggi.

Fitur ini sangat jarang di antara bahasa pemrograman. Bahkan Haskell tidak mengizinkannya secara default.

Apakah itu berguna? Bisakah itu menggambarkan perilaku yang sulit untuk dijelaskan sebaliknya?

Juga, apa artinya sesuatu menjadi tidak bijaksana ? (pada konteks ini)

Secara umum, Anda menggunakan polimorfisme tingkat tinggi ketika Anda ingin callee dapat memilih nilai parameter tipe, daripada pemanggil . Sebagai contoh:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

Setiap fungsi gyang saya lewati untuk ini fharus dapat memberi saya Intnilai dari suatu tipe, di mana satu - satunya yang gtahu tentang tipe itu adalah ia memiliki instance Show. Jadi ini halal:

f (length . show)
f (const 42)

Tapi ini bukan:

f length
f succ

Salah satu aplikasi yang sangat berguna adalah dalam menggunakan pelingkupan jenis untuk menegakkan pelingkupan nilai . Misalkan kita memiliki objek tipe Action<T>, mewakili tindakan yang dapat kita jalankan untuk menghasilkan hasil tipe T, seperti masa depan atau panggilan balik.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Sekarang, anggaplah kita juga memiliki objek Actionyang dapat mengalokasikan Resource<T>objek:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

Kami ingin menegakkan bahwa sumber daya itu hanya digunakan di dalam Actiontempat mereka diciptakan, dan tidak dibagi di antara tindakan yang berbeda atau tindakan yang berbeda dari tindakan yang sama, sehingga tindakan itu deterministik dan berulang.

Kita dapat menggunakan tipe dengan peringkat lebih tinggi untuk mencapai hal ini dengan menambahkan parameter Ske Resourcedan Actiontipe, yang benar-benar abstrak — itu mewakili “cakupan” dari Action. Sekarang tanda tangan kami adalah:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

Sekarang ketika kita memberikan runActionsebuah Action<S, T>, kita yakin bahwa karena “lingkup” parameter Ssepenuhnya polimorfik, itu tidak bisa lepas dari tubuh runAction-jadi nilai apapun dari jenis yang menggunakan Sseperti Resource<S, int>juga tidak dapat melarikan diri!

(Dalam Haskell, ini dikenal sebagai STmonad, di mana runActiondisebut runST, Resourcedisebut STRef, dan newResourcedisebut newSTRef.)

Polimorfisme peringkat tinggi sangat berguna. Dalam Sistem F (bahasa inti dari bahasa FP yang diketik yang Anda kenal), ini penting untuk mengakui "pengkodean Gereja yang diketik" yang sebenarnya adalah cara Sistem F melakukan pemrograman. Tanpa ini, sistem F sama sekali tidak berguna.

Dalam Sistem F, kami mendefinisikan angka sebagai

Nat = forall c. (c -> c) -> c -> c

Penambahan memiliki tipe

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

yang merupakan tipe peringkat yang lebih tinggi ( forall c.muncul di dalam panah itu).

Ini muncul di tempat lain juga. Misalnya, jika Anda ingin menunjukkan bahwa perhitungan adalah gaya kelanjutan lewat yang tepat (google "codensity haskell") maka Anda akan menganggap ini sebagai

type CPSed A = forall c. (A -> c) -> c

Bahkan berbicara tentang tipe yang tidak berpenghuni dalam Sistem F membutuhkan polimorfisme peringkat yang lebih tinggi

type Void = forall a. a 

Panjang dan pendek dari ini, menulis fungsi dalam sistem tipe murni (Sistem F, CoC) membutuhkan polimorfisme peringkat yang lebih tinggi jika kita ingin berurusan dengan data yang menarik.

Dalam Sistem F khususnya, pengkodean ini harus "impredikatif". Ini berarti bahwa jumlah semua jenisforall a. dikuantifikasi secara absolut . Ini secara kritis termasuk tipe yang kami definisikan. Dalam forall a. ahal aitu sebenarnya bisa berdiri forall a. alagi! Dalam bahasa-bahasa seperti ML, ini bukan masalahnya, mereka dikatakan "predikatif" karena suatu variabel tipe hanya mengukur lebih dari sekumpulan tipe tanpa quantifiers (disebut monotipe). Definisi kita tentang plusimpredicativity diperlukan juga karena kita instantiated cdi l : Natuntuk menjadi Nat!

Akhirnya, saya ingin menyebutkan satu alasan terakhir di mana Anda ingin impredicativitas dan polimorfisme peringkat tinggi bahkan dalam bahasa dengan tipe rekursif sewenang-wenang (tidak seperti Sistem F). Di Haskell, ada monad untuk efek yang disebut "state thread monad". Idenya adalah bahwa thread negara monad memungkinkan Anda bermutasi tetapi mengharuskan untuk melarikan diri bahwa hasil Anda tidak bergantung pada apa pun yang bisa berubah. Ini berarti bahwa perhitungan ST dapat diamati murni. Untuk menegakkan persyaratan ini kami menggunakan polimorfisme peringkat yang lebih tinggi

runST :: forall a. (forall s. ST s a) -> a

Di sini dengan memastikan bahwa aitu terikat di luar ruang lingkup di mana kami memperkenalkan s, kami tahu bahwa asingkatan dari tipe yang dibentuk dengan baik yang tidak bergantung s. Kami menggunakan suntuk melakukan parameritisasi semua hal yang dapat berubah dalam utas status khusus tersebut sehingga kami tahu bahwa hal atersebut tidak tergantung pada hal-hal yang dapat berubah dan dengan demikian tidak ada yang lolos dari cakupan STperhitungan itu! Sebuah contoh yang bagus dari penggunaan tipe untuk menyingkirkan program yang tidak sempurna.

Omong-omong, jika Anda tertarik untuk belajar tentang teori jenis, saya sarankan berinvestasi dalam satu atau dua buku yang bagus. Sulit untuk mempelajari hal ini sedikit demi sedikit. Saya menyarankan salah satu buku Pierce atau Harper tentang teori PL secara umum (dan beberapa elemen teori tipe). Buku "Topik lanjutan dalam jenis dan bahasa pemrograman" juga mencakup sejumlah besar teori jenis. Akhirnya "Pemrograman dalam teori tipe Martin Lof" adalah eksposisi yang sangat baik ke dalam teori tipe intensional Martin Lof diuraikan.