在學習米田引理時，我遇到了 Haskell 中潛在自然同構的以下編碼：
forward :: Functor f => (forall r . (a -> r) -> f r) -> f a
forward f = f id
backward :: Functor f => f a -> (forall r. (a -> r) -> f r)
backward x f = fmap f x
我試圖簡化 to 的實作，backward但flip fmap失敗了，因為后者有 type f a -> (a -> r) -> f r。
從這里開始，我一直在查明這兩種實作之間的差異究竟是什么。更重要的是，將任一函式應用于具體函子會產生相同的結果型別：
ghci> :t bw (Just "")
bw (Just "") :: (String -> r) -> Maybe r
ghci> :t (flip fmap) (Just "")
(flip fmap) (Just "") :: (String -> r) -> Maybe r
問題：
- 兩者之間究竟有什么區別？
- 有什么我可以用一個不能用另一個做的嗎？
- 為什么需要全稱量化
backward？
uj5u.com熱心網友回復：
在 Haskell 中，我們為傳遞的值撰寫 lambda：
id :: forall a . a->a
id = \x -> x
但是當我們編譯到對 System F 封閉的較低級別的 Core 語言時，我們也會看到型別 lambdas。代碼變得更像
id = \ @a (x :: @a) -> x
這意味著：呼叫者應該選擇并傳遞一個型別@a，然后是該型別的一個值，x :: @a最后接收該值x。
現在，您的問題來自兩種（同構）型別
forall a . T -> U a
-- vs
T -> forall a . U a
在這里，T不依賴于a. 這兩種型別確實是同構的，在較低級別上，只需將術語 lambda 與 type-lambda 進行“翻轉”即可：
\ @a (x :: T) -> ... -- has the former type
-- vs
\ (x :: T) @a -> ... -- has the latter
由于在 Haskell 中我們通常不會撰寫或看到 type-lambda，因此很難區分它們。此外，當編譯器執行型別推斷時，它會（據我所知）推斷第一個，其中 type-lambdas 都在開頭。
兩者之間究竟有什么區別？
不多。畢竟，它們具有同構型別。一個forall a在最頂層，而另一個在另一個位置。
一旦你像你一樣將 then 應用于引數，GHC 將自動選擇正確的位置來添加推斷的@a引數，因此你不會輕易注意到差異。這兩個呼叫具有以下形式：
f @r x
-- vs
f x @r
最重要的是，GHC 可以重新泛化型別，因此我們得到
(\@r -> f @r x) :: forall r . ....
(\@r -> f x @r) :: forall r . ....
有什么我可以用一個不能用另一個做的嗎？
并不真地。
為什么向后完全需要通用量化？
通常，在定義 和 之間的同構時A，B我們想要
forw :: A -> B
back :: B -> A
如果任何一種型別都有一個 forall（比如A = forall r . V r），那么我們會在那個位置得到一個 forall。請注意，back在這種情況下的型別也是同構的
forall r . B -> V r
如果我們省略量詞（并讓 Haskell 在頂層隱式地重新添加它），這就是我們將得到的結果。
（相比之下，型別中的量詞forw :: (forall r . V r) -> B不能移動到頂層。）
轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/488478.html