我正在玩 Rank-N-type 并嘗試輸入x x. 但是我發現這兩個函式可以以相同的方式輸入是違反直覺的。
f :: (forall a b. a -> b) -> c
f x = x x
g :: (forall a b. a -> b) -> c
g x = x x x x x
我還注意到像f x = x x ... x x(many xs)這樣的東西仍然具有相同的型別。誰能解釋為什么會這樣？
uj5u.com熱心網友回復：
關鍵是這x :: a -> b是一個可以提供任何型別值的函式，無論給出什么引數。這意味著x可以應用于自身，結果可以x再次應用于，依此類推。
至少，這就是它承諾的型別檢查器可以做的事情。型別檢查器不關心是否存在任何這樣的值，只關心型別是否對齊。既不f也不g實際上不能被呼叫，因為不存在這樣的型別值a -> b（忽略底部和unsafeCoerce）。
uj5u.com熱心網友回復：
一個更簡單的例子
每當我們使用具有多型型別的變數（如您的x）時，都可以觀察到這種現象。恒等函式id可能是最著名的例子。
id :: forall a . a -> a
在這里，所有這些運算式型別檢查，并具有型別Int -> Int：
id :: Int -> Int
id id :: Int -> Int
id id id :: Int -> Int
id id id id :: Int -> Int
...
這怎么可能？好吧，關鍵是每次我們寫的時候，我們id實際上是指“a應該從背景關系中推斷出的某個未知型別的恒等函式”。至關重要的是，每次使用id都有自己的a.
讓我們id @T來表示 type 上的特定標識函式T。
寫作
id :: Int -> Int
實際上是指
id @Int :: Int -> Int
這很簡單。相反，寫
id id :: Int -> Int
實際上是指
id @(Int -> Int) (id @Int) :: Int -> Int
其中第一個id現在指的是函式空間Int -> Int！而且當然，
id id id :: Int -> Int
方法
(id @((Int -> Int) -> (Int -> Int))) (id @(Int -> Int)) (id @Int) :: Int -> Int
等等。我們沒有意識到型別會變得如此混亂，因為 Haskell 會為我們推斷這些型別。
具體案例
在您的具體情況下，
g :: (forall a b. a -> b) -> c
g x = x x x x x
我們可以通過多種方式進行型別檢查。一種可能的方法是定義A ~ Int, B ~ Bool，T ~ (A -> B)然后推斷：
g x = x @T @(T -> T -> T -> c) (x @A @B) (x @A @B) (x @A @B) (x @A @B)
我建議花一些時間來了解所有型別的檢查。（此外，我們對A和的選擇B是完全任意的，我們可以在那里使用任何其他型別。我們甚至可以為 each使用不同的As 和Bs x，只要第一個x被適當地實體化！）
很明顯，即使x x x ...是更長的序列，這種推斷也是可能的。
uj5u.com熱心網友回復：
這不應該比以下事實更令人驚訝
m :: (? a . a) -> (? a . a) -> (Int, Bool)
m p q = (p, q)
具有相同的型別
n :: (? a . a) -> (? a . a) -> (Int, Bool)
n p q = (q, p)
就像在您的示例中一樣，這是有效的，因為通用量化引數可以以多種不同的方式使用，編譯器在每種情況下都會選擇適當的型別并強制執行x該型別。
這實際上是一個相當人為的情況，因為型別像? a . a或? a b . a->b無人居住（模⊥），因此您實際上永遠無法使用帶有此類引數的 RankN 函式；實際上，那時您甚至都不會寫它！
實用的 RankN 函式通常會在其引數中強加一些額外的結構或型別類約束，例如
foo :: (? a . [a] -> [a]) -> ...
或者
qua :: (? n . Num n -> Int -> n -> n) -> ...
轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/355868.html
標籤：哈斯克尔