爲什麼函數（+）匹配類型（a - > b - > b）？

Question

摺疊功能：

從 http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

採取

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

什麼用a -> a -> a型型(a -> b -> b)匹配(+)功能？

由於摺疊定義接受函數類型(a -> b -> b)這意味着前2個參數(a -> b)必須是不同的類型？

Answer 1

不，它的意思是，a和b可以是不同的，但它不是強制性的它是不同的。在你的情況下，它是一樣的。

一個非常簡單的例子來傳達這一點：

data SomeType a b = Test a b deriving (Show) 

現在ghci：

Answer 2

你在相反的方向所思所想。您不必檢查是否+相同或相匹配a -> b -> b，你想要的+類型是專業化a -> b -> b並檢查這一點，你必須統一類型。

統一意味着你想看是否+和類型的類型a -> b -> b可以通過重命名的類型變量應相等。

所以+有類型Num x => x -> x -> x。現在讓我們忽略類約束，讓我們看看我們是否可以匹配功能類型。 類型變成x -> x -> x和a -> b -> b。實際上，如果我們看看它們的實際情況，最好不要使用關聯性：x -> (x -> x)和a -> (b -> b)。

->是型構造函數。即它是將一定數量的類型映射到不同類型的函數。在這種情況下，->構造函數將t_1和t_2這兩種類型映射到功能類型(->) t_1 t_2（通常由t_1 -> t_2表示）。

所以類型x -> (x -> x)實際上是(->) x ((->) x x)是應用於x並應用於x和x類型構造->類型構造->。 另一種是(->) a ((->) b b)。

統一時，您考慮兩種類型的最外層類型構造函數（在這種情況下爲->）。如果這不匹配，你不能統一。否則，你不得不統一構造函數的參數。

所以我們必須統一x與a。它們都是類型變量，所以我們可以將其重命名爲其中之一。假設我們將a重命名爲x。所以現在我們將重命名應用於類型，獲得：(->) x ((->) x x)和(->) x ((->) b b)，您會看到現在匹配x和x。

讓我們考慮第二個參數。它不是一個類型變量，所以我們必須匹配類型構造函數，這兩個都是->。所以我們對這些參數進行遞歸處理。

我們想要匹配x和b。它們都是類型變量，所以我們可以重命名其中的一個。假設我們將x重命名爲b。我們將這種替換應用於類型，獲得：(->) b ((->) b b)和(->) b ((->) b b)。現在一切都匹配。因此這兩種類型統一。

關於類約束，當我們重命名x與b我們應用替代的約束也因此成爲Num x和Num b最後兩種類型都Num b => b -> b -> b。

我希望這可以讓你更好地理解類型是如何工作的以及如何檢查類型。

---

附註：這是haskell在執行類型推斷時所做的。它首先分配一個未知函數一個新的類型變量t。然後它使用統一來獲得定義它的表達式的類型，並檢查與t相關聯的類型，這是函數的類型。