`翻转（$）的理解类型`

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