GHC擴展-XRankNTypes是什麼？如何理解forall .？

01-27

某些關於RankNTypes的例子中提到了類似nested forall這種東西，不是很理解，或許我應該把它當作?符號來理解？
為什麼
theAnswer :: (forall a. a -&> a) -&> Int theAnswer id = id 42
是正確而可用的，而這個

theAnswer :: forall a. (a -&> a) -&> Int theAnswer id = id 42
就會提示錯誤
Couldnt match expected type 『Int』 with actual type 『a』『a』 is a rigid type variable bound by the type signature for: theAnswer :: forall a. (a -&> a) -&> Int
另外我還觀察到了一個現象，當我寫更多層類似「nested forall」的函數的時候，應用函數的效率會明顯地降低，在ghci上對比一個普通一層（應該叫Rank 1？）的函數可以感覺到明顯的卡頓。-XRankNTypes的效率對比普通的（Rank 1？）類型低很多嗎？

rankntypes 可以將多態函數作為參數

這裡多態的意思是，其參數類型變數沒有出現在外部函數中，你無法根據其他參數和返回值的類型來確定這個作為參數的函數的類型

比如

t :: Int -&> (forall b . b -&> Int) -&> Int

t x f = if x == 1 then f a else f 1

rank1 就是函數自己是多態的，但沒有多態函數做參數

rank2 就是有多態函數做參數，但是這個多態函數本身不可以接受多態函數做參數

rank3 就是可以有一個接受多態函數做參數的多態函數來做參數，但是最裡面那層多態函數不可以接受多態函數做參數

……以此類推……

你第二個的問題出在forall必須作用在作為參數的多態函數上，以顯式說明此函數為多態函數，不然效果如同未開rankntypes

使用 UTT 的符號的話，並且標出所有的類型參數和實例化調用的話，forall a. b 可以改寫成這個形式

{a :: } -&> b

其中的是所有類型的類型，一個大類（或者說全集）；b 則是一個可能包含 a 的項，一般是其他類型。在 Haskell 中，調用一個帶有 forall 的函數的時候，{a :: } 對應的那個參數會由編譯器推理出來填上（而且你還沒辦法手工指定……）

於是你的第一個例子裡面 theAnswer 的類型是：

theAnswer :: ({a :: } -&> a -&> a) -&> Int theAnswer id = id {Int} 42

而第二個例子裡面

theAnswer :: {a :: } -&> (a -&> a) -&> Int theAnswer {aTy} id = id 42

這裡，id 的類型由參數 aTy 決定，但是 aTy 是未知的（它不一定是 Int），所以報錯「Int 無法合演到固化類型變數 a」。

對於第二個問題，既然 forall 本質上就是一種函數類型，那麼自然也需要調用它，只不過對於一般的 Rank-1 type，因為傳入的參數都是常量（已知的類型定義），編譯器把對應的函數抽象和調用給幹掉了而已。

補充一下其他答案，舉個例子:

foo :: forall b c. (forall a. a -&> a) -&> (b, c) -&> (b, c)

foo f (b, c) = (f b, f c)

然後我們調用這個函數:

foo id (1 :: Int, c :: Char)

一切都沒問題。但是如果我們將a放到外面，就過不了typecheck，因為Int和Char的鍋。