Apa tujuan Rank2Types?

Saya tidak terlalu mahir dalam Haskell, jadi ini mungkin pertanyaan yang sangat mudah.

Batasan bahasa apa yang dipecahkan oleh Rank2Types ? Bukankah fungsi di Haskell sudah mendukung argumen polimorfik?

Bukankah fungsi di Haskell sudah mendukung argumen polimorfik?

Ya, tetapi hanya dari peringkat 1. Ini berarti bahwa meskipun Anda dapat menulis fungsi yang menggunakan tipe argumen berbeda tanpa ekstensi ini, Anda tidak dapat menulis fungsi yang menggunakan argumennya sebagai tipe berbeda dalam pemanggilan yang sama.

Misalnya fungsi berikut tidak dapat diketik tanpa ekstensi ini karena gdigunakan dengan tipe argumen yang berbeda dalam definisi f:

f g = g 1 + g "lala"

Perhatikan bahwa sangat mungkin untuk meneruskan fungsi polimorfik sebagai argumen ke fungsi lain. Jadi sesuatu seperti map id ["a","b","c"]itu legal. Tetapi fungsinya hanya dapat menggunakannya sebagai monomorfik. Dalam contoh mappenggunaan idseolah-olah memiliki tipe String -> String. Dan tentu saja Anda juga bisa meneruskan fungsi monomorfik sederhana dari tipe yang diberikan, bukan id. Tanpa rank2types, tidak ada cara bagi suatu fungsi untuk mensyaratkan argumennya harus berupa fungsi polimorfik dan dengan demikian tidak ada cara untuk menggunakannya sebagai fungsi polimorfik.

Sulit untuk memahami polimorfisme peringkat tinggi kecuali Anda mempelajari Sistem F secara langsung, karena Haskell dirancang untuk menyembunyikan detailnya dari Anda demi kesederhanaan.

Tapi pada dasarnya, ide kasarnya adalah tipe polimorfik tidak memiliki ekstensi a -> b bentuk seperti yang mereka lakukan di Haskell; pada kenyataannya, mereka terlihat seperti ini, selalu dengan bilangan eksplisit:

id :: ∀a.a → a
id = Λt.λx:t.x

Jika Anda tidak tahu simbol "∀", itu dibaca sebagai "untuk semua"; ∀x.dog(x)berarti "untuk semua x, x adalah seekor anjing." "Λ" adalah lambda kapital, digunakan untuk mengabstraksi parameter tipe; apa yang baris kedua katakan adalah bahwa id adalah fungsi yang mengambil tipe t, dan kemudian mengembalikan fungsi yang diparameterisasi oleh tipe itu.

Anda lihat, di Sistem F, Anda tidak bisa begitu saja menerapkan fungsi seperti itu id ke nilai secara langsung; pertama, Anda perlu menerapkan fungsi Λ ke suatu tipe untuk mendapatkan fungsi λ yang Anda terapkan ke nilai. Jadi contohnya:

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

Standard Haskell (yaitu, Haskell 98 dan 2010) menyederhanakan hal ini untuk Anda dengan tidak memiliki salah satu pembilang tipe, lambda kapital, dan aplikasi tipe ini, tetapi di balik layar GHC menempatkannya saat menganalisis program untuk kompilasi. (Saya yakin, ini semua adalah hal waktu kompilasi, tanpa overhead waktu proses.)

Tetapi penanganan otomatis Haskell terhadap hal ini berarti bahwa ia mengasumsikan bahwa "∀" tidak pernah muncul di cabang kiri jenis fungsi ("→"). Rank2TypesdanRankNTypes matikan batasan tersebut dan memungkinkan Anda untuk mengganti aturan default Haskell untuk tempat penyisipan forall.

Mengapa Anda ingin melakukan ini? Karena Sistem F yang lengkap dan tidak terbatas sangat kuat, dan dapat melakukan banyak hal keren. Misalnya, penyembunyian tipe dan modularitas dapat diimplementasikan menggunakan tipe peringkat yang lebih tinggi. Ambil contoh fungsi lama biasa dari tipe peringkat-1 berikut (untuk mengatur pemandangan):

f :: ∀r.∀a.((a → r) → a → r) → r

Untuk menggunakan f, pemanggil terlebih dahulu harus memilih tipe apa yang akan digunakan rdan a, lalu memberikan argumen dari tipe yang dihasilkan. Jadi Anda bisa memilih r = Intdan a = String:

f Int String :: ((String → Int) → String → Int) → Int

Tapi sekarang bandingkan itu dengan tipe peringkat lebih tinggi berikut:

f' :: ∀r.(∀a.(a → r) → a → r) → r

Bagaimana cara kerja fungsi jenis ini? Nah, untuk menggunakannya, pertama-tama Anda tentukan jenis yang akan digunakan r. Katakanlah kita memilih Int:

f' Int :: (∀a.(a → Int) → a → Int) → Int

Tapi sekarang ∀aada di dalam fungsi panah, jadi Anda tidak bisa memilih tipe apa yang akan digunakan a; Anda harus menerapkan f' Intfungsi Λ dari tipe yang sesuai. Ini berarti bahwa implementasi f'dapat memilih tipe apa yang akan digunakan a, bukan pemanggilf' . Sebaliknya, tanpa tipe peringkat yang lebih tinggi, pemanggil selalu memilih tipe.

Untuk apa ini berguna? Sebenarnya, untuk banyak hal, tapi satu idenya adalah Anda dapat menggunakan ini untuk memodelkan hal-hal seperti pemrograman berorientasi objek, di mana "objek" menggabungkan beberapa data tersembunyi bersama dengan beberapa metode yang bekerja pada data tersembunyi. Jadi misalnya, sebuah objek dengan dua metode — satu yang mengembalikan Intdan yang lainnya mengembalikan String, bisa diimplementasikan dengan tipe ini:

myObject :: ∀r.(∀a.(a → Int, a -> String) → a → r) → r

Bagaimana cara kerjanya? Objek diimplementasikan sebagai fungsi yang memiliki beberapa data internal tipe tersembunyi a. Untuk benar-benar menggunakan objek, kliennya mengirimkan fungsi "callback" yang akan dipanggil oleh objek dengan dua metode. Sebagai contoh:

myObject String (Λa. λ(length, name):(a → Int, a → String). λobjData:a. name objData)

Di sini kita, pada dasarnya, memanggil metode kedua objek, metode yang tipenya a → Stringuntuk yang tidak diketahui a. Yah, tidak diketahui myObjectklien; tetapi klien ini tahu, dari tanda tangan, bahwa mereka akan dapat menerapkan salah satu dari dua fungsi ke sana, dan mendapatkan salah satu Intatau a String.

Untuk contoh Haskell yang sebenarnya, di bawah ini adalah kode yang saya tulis ketika saya belajar sendiri RankNTypes. Ini mengimplementasikan tipe yang disebut ShowBoxyang menggabungkan nilai dari beberapa tipe tersembunyi bersama dengan Showinstance kelasnya. Perhatikan bahwa dalam contoh di bawah, saya membuat daftar ShowBoxelemen pertamanya yang dibuat dari angka, dan yang kedua dari string. Karena tipe disembunyikan dengan menggunakan tipe peringkat yang lebih tinggi, ini tidak melanggar pemeriksaan tipe.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

PS: bagi siapa saja yang membaca ini yang bertanya-tanya kenapa ExistentialTypesmenggunakan GHC forall, saya yakin alasannya adalah karena menggunakan teknik semacam ini di belakang layar.

Jawaban Luis Casillas memberikan banyak info bagus tentang apa arti tipe peringkat 2, tetapi saya hanya akan memperluas satu hal yang tidak dia bahas. Mewajibkan argumen menjadi polimorfik tidak hanya mengizinkannya digunakan dengan banyak tipe; ia juga membatasi apa yang dapat dilakukan fungsi tersebut dengan argumennya dan bagaimana ia dapat menghasilkan hasilnya. Artinya, ini memberi lebih sedikit kepada penelepon fleksibilitas yang . Mengapa Anda ingin melakukan itu? Saya akan mulai dengan contoh sederhana:

Misalkan kita memiliki tipe data

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

dan kami ingin menulis fungsi

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

yang mengambil fungsi yang seharusnya memilih salah satu elemen dari daftar yang diberikan dan mengembalikan IOaksi meluncurkan rudal ke target itu. Kami bisa memberikan ftipe sederhana:

f :: ([Country] -> Country) -> IO ()

Masalahnya adalah kita bisa lari tanpa sengaja

f (\_ -> BestAlly)

dan kemudian kita akan mendapat masalah besar! Pemberian ftipe polimorfik rank 1

f :: ([a] -> a) -> IO ()

tidak membantu sama sekali, karena kami memilih jenis asaat kami menelepon f, dan kami hanya mengkhususkan Countrydan menggunakan perangkat jahat kami \_ -> BestAllylagi. Solusinya adalah dengan menggunakan tipe rank 2:

f :: (forall a . [a] -> a) -> IO ()

Sekarang fungsi yang kita berikan harus polimorfik, jadi \_ -> BestAllytidak akan mengetik cek! Faktanya, tidak ada fungsi yang mengembalikan elemen yang tidak ada dalam daftar yang diberikan akan melakukan kesalahan ketik (meskipun beberapa fungsi yang masuk ke loop tak terbatas atau menghasilkan kesalahan dan karena itu tidak pernah kembali akan melakukannya).

Hal di atas tentu saja dibuat-buat, tetapi variasi pada teknik ini adalah kunci untuk membuat STmonad aman.

Tipe peringkat lebih tinggi tidak eksotis seperti jawaban lain yang dibuat. Percaya atau tidak, banyak bahasa berorientasi objek (termasuk Java dan C #!) Menampilkannya. (Tentu saja, tidak ada seorang pun di komunitas itu yang mengenal mereka dengan nama yang terdengar menakutkan "tipe peringkat lebih tinggi".)

Contoh yang akan saya berikan adalah implementasi buku teks dari pola Pengunjung, yang saya gunakan sepanjang waktu dalam pekerjaan saya sehari-hari. Jawaban ini tidak dimaksudkan sebagai pengenalan pola pengunjung; pengetahuan yang mudah tersedia di tempat lain .

Dalam aplikasi SDM imajiner yang konyol ini, kami ingin beroperasi pada karyawan yang mungkin merupakan staf tetap penuh waktu atau kontraktor sementara. Variasi yang saya sukai dari pola Pengunjung (dan memang yang relevan dengan RankNTypes) menentukan parameter jenis pengunjung yang kembali.

interface IEmployeeVisitor<T>
{
    T Visit(PermanentEmployee e);
    T Visit(Contractor c);
}

class XmlVisitor : IEmployeeVisitor<string> { /* ... */ }
class PaymentCalculator : IEmployeeVisitor<int> { /* ... */ }

Intinya adalah bahwa sejumlah pengunjung dengan jenis pengembalian yang berbeda dapat beroperasi pada data yang sama. Ini berarti tidak IEmployeeboleh mengungkapkan pendapat tentang apa yang Tseharusnya.

interface IEmployee
{
    T Accept<T>(IEmployeeVisitor<T> v);
}
class PermanentEmployee : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
class Contractor : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}

Saya ingin menarik perhatian Anda pada tipe. Perhatikan bahwa IEmployeeVisitorsecara universal mengkuantifikasi jenis kembaliannya, sedangkan IEmployeemengkuantifikasikannya di dalam Acceptmetode - artinya, pada peringkat yang lebih tinggi. Menerjemahkan dengan kikuk dari C # ke Haskell:

data IEmployeeVisitor r = IEmployeeVisitor {
    visitPermanent :: PermanentEmployee -> r,
    visitContractor :: Contractor -> r
}

newtype IEmployee = IEmployee {
    accept :: forall r. IEmployeeVisitor r -> r
}

Jadi begitulah. Tipe berperingkat lebih tinggi muncul di C # ketika Anda menulis tipe yang berisi metode umum.

Slide dari kursus Haskell Bryan O'Sullivan di Stanford membantu saya memahami Rank2Types.

Bagi mereka yang akrab dengan bahasa berorientasi objek, fungsi peringkat lebih tinggi hanyalah fungsi generik yang mengharapkan fungsi generik lain sebagai argumennya.

Misalnya di TypeScript Anda bisa menulis:

type WithId<T> = T & { id: number }
type Identifier = <T>(obj: T) => WithId<T>
type Identify = <TObj>(obj: TObj, f: Identifier) => WithId<TObj>

Lihat bagaimana tipe fungsi generik Identifymenuntut fungsi generik dari tipe tersebut Identifier? Ini membuat Identifyfungsi peringkat lebih tinggi.