`翻轉（$）的理解類型`

Question

綜觀($)和flip類型：

ghci> :t ($) 
($) :: (a -> b) -> a -> b 

ghci> :t flip 
flip :: (a -> b -> c) -> b -> a -> c 

能否請你解釋一下如何flip ($)有這樣的簽名？

ghci> :t flip ($) 
flip ($) :: b -> (b -> c) -> c 

Answer 1

漂亮其實很簡單：

($) :: (a -> b) -> a -> b 
     |______| | | 
      |  | | 
flip :: (a -> b -> c) -> b -> a -> c 

因此，我們基本上是統一(a -> b -> c)與(a -> b) -> a -> b。爲了清楚起見，讓我們重命名(a -> b -> c)到(r -> s -> t)：

($) :: (a -> b) -> a -> b 
     |______| | | 
      |  | | 
flip :: (r -> s -> t) -> s -> r -> t 

因此：

1. r與(a -> b)結合。
2. s與a相一致。
3. t與b統一。

因此：

flip ($) :: s -> r -> t 
     :: a -> (a -> b) -> b 

這相當於：

flip ($) :: b -> (b -> c) -> c 

這一切就是這麼簡單。

---

編輯：

1. 的flip函數有一個參數，(a -> b -> c)，以及一個返回值b -> a -> c。
2. 當您編寫flip ($)時，($)函數將成爲flip函數的第一個參數。
3. 因此，($)的類型簽名是unified，其參數的類型簽名爲flip。
4. 統一是將兩個術語合併爲一個術語的過程。
5. 在這種情況下，兩個術語是(a -> b -> c)和(a -> b) -> a -> b。
6. 爲了統一它們變成一個術語(a -> b -> c)首先重命名爲(r -> s -> t)然後r代替(a -> b)，s代替a和t代替b。統一term1和term2當http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse5

   總結的統一算法，：

例如，我們可以寫一個Prolog程序，統一條款：

% fun(R, fun(S, T))   is equivalent to (r -> s -> t). 
% fun(fun(A, B), fun(A, B)) is equivalent to (a -> b) -> a -> b. 

?- fun(R, fun(S, T)) = fun(fun(A, B), fun(A, B)). 
R = fun(A, B), 
S = A, 
T = B. 

一個統一的算法可以在這裏找到：

1. 如果term1和term2是常數，然後它們統一，當且僅當它們是相同的常數。例如Int只與常數Int相一致。它不與統一的Char統一。
2. 如果term1是變量並且term2是非變量，則term1被實例化爲term2（即term1 := term2）。例如，a和Int與a := Int一致。
3. 如果term2是變量並且term1是非變量，則term2被實例化爲term1（即term2 := term1）。例如，Int和b與b := Int統一。
4. 如果term1和term2都是變量，那麼它們都被實例化爲彼此並且它們被稱爲共享值（即term1 := term2和term2 := term1）。例如，當統一時，a和b成爲相同的變量。
5. 如果term1和term2是複雜的術語（例如term1是Either a Int和term2是Either Char b），然後他們統一當且僅當：
   1. 它們具有相同的類型構造。例如，Maybe Int和Maybe Char具有相同的類型構造函數。但是，Maybe Int和[Int]不。
   2. 他們相應的參數統一。例如在Either a Int和Either Char b中，參數與a := Char和b := Int一致。
   3. 變量實例化是兼容的。例如，統一Either a a與Either Char Int時，我們首先有a := Char，然後a := Int。這是不相容的。因此這兩個術語不統一。
6. 兩個術語統一起來，當且僅當它們從前面的5個子句中統一起來。

Answer 2

Unflipped $在其右側得到a類型的值，並且它適用於從它的左側的功能(a -> b)：func $ value相同func value。

翻轉$需要b類型的值在其左側和從其右側施加函數(b->c)它：value `flip ($)` func相同func value。

Answer 3

行了相應類型的組件：

($) :: (a -> b) -> a -> b 
flip :: (a  -> b -> c) -> b -> a -> c 

重要的規則：在任何類型的簽名，可以更換另一類型的變量每次發生不以相同的簽名出現在任何地方，和得到一個完全等同於原始的類型。 （類型不關心類型變量的名稱，只有哪些變量相同，哪些變量在同一個簽名中是不同的。）因此，我們可以在flip（a := x,b := y,c := z）中稍微重命名類型變量，並且它是相同的類型：

($) :: (a -> b) -> a -> b 
flip :: (x  -> y -> z) -> y -> x -> z 

稍有不同的規則：在任何類型的簽名，我們可以替換類型變量的所有實例的任何類型並獲得專門版本類型。讓我們專門將flip設置爲與($)兼容的類型。我們通過更換x := (a -> b)，y := a和z := b：

($) :: (a -> b) -> a -> b 
flip :: ((a -> b) -> a -> b) -> a -> (a -> b) -> b 

現在的flip這個特殊版本的第一個參數的類型($)類型相匹配，我們可以計算出的flip ($)類型：

flip ($) :: a -> (a -> b) -> b 

現在我們更換b := c，並在此之後，a := b：

flip ($) :: b -> (b -> c) -> c