haskell - 了解 `flip ($)` 的类型

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。

例如，我们可以编写一个 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.

统一算法可以在这里找到:http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse5

总结统一算法，统一term1和term2时:

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 个子句。