了解`flip（$）`的类型 [英] Understanding Type of `flip ($)`

问题描述

查看（$）和 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 
  




解决方案

很简单：

 （$）::（a  - > b） - > a  - > b 
 | ______ | | | 
 | | | 
 flip ::（a  - > b  - > c） - > b  - > a  - > c 
  

因此，我们基本上统一了（a - > b - > c）与（a - > b） - > a - > B'/ code>。为了清楚起见，我们将（a - > b - > c）重命名为（r - > s - > t） / code>：



 （$）::（a  - > b） - > a  - > b 
 | ______ | | | 
 | | | 
 flip ::（r  - > s  - > t） - > s  - > r  - > t 
  

因此：



1. r 与（a - > b）相统一。


2. s 用 a 。
统一

3. 
   
   $ b 因此：
   
   

    翻转（$）:: s  - > r  - > t 
    :: a  - > （a  - > b） - > b 
     

   这相当于：
   
   

     flip（$）:: b  - > （b→c）→> c 
     

   这就是它的全部。

   
   
   
   
   

   编辑：
   $ b

   
   
   1. flip 函数有一个参数，（a - > b - > c），一个返回值 b - > a - > c 。
   
   
   2. 当您写 flip（$）时，（$ ）函数成为 flip 函数的第一个参数。
   因此，类型签名（$）与统一 flip 的参数的类型签名。
   
   3. 统一是将两个词合并为一个词的过程。 $ b
   4. 在这种情况下，两个项是（a - > b - > c）和（a - > b） - > a - > b 。
   
   
   5. 将它们合并为一个词（a - > b - > c）首先被重命名为（r - > s - > t），然后用 r 代替（a - > b）， s 代替 a 和 t 取代 b 。
   
   

   例如，我们可以编写一个Prolog程序来统一术语：



    ％fun（R，fun（S ，T））等价于（r→s→t）。 
   ％fun（fun（A，B），fun（A，B））等价于（a-> b） - > a  - >湾（乐趣（S，T））=乐趣（乐趣（A，B），乐趣（A，B））。 
    R =有趣（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 。
   如果 term2 是一个变量， term1 是一个非变量那么 term2 被实例化为 term1 （即 term2：= term1 ）。例如， Int 和 b 与 b：= Int 。
   
   3. 如果 term1 和 term2 都是变量，那么它们都被实例化他们被称为分享价值（即 term1：= term2 和 term2：= term1 ）。例如，当统一时， a 和 b 变成相同的变量。
      
   4. 如果 term1 和 term2 是复杂的词语（例如 term1 是一个Int 和 term2 是任一字符b ），那么他们统一，当且仅当：
      
      
      
      
      1. 它们具有相同的类型构造函数。例如， Maybe Int 和 Maybe Char 具有相同的类型构造函数。但是， Maybe Int 和 [Int] 不。
      
      
      2. 论点统一。例如，在中，一个Int 和任一个Char b ，参数与 a：=一致Char 和 b：= Int 。
      
      
      3. 变量实例是兼容的。例如，统一或者aa 与任何一个Char Int ，我们首先都有 a：= Char ，然后 a：= Int 。这是不相容的。因此，这两个术语不统一。
      / li>
      

      
      

      Looking at the type of ($) and flip:

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

      Can you please explain to me how flip ($) has such a signature?

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

      解决方案

      Pretty simple really:

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

      Hence we are essentially unifying (a -> b -> c) with (a -> b) -> a -> b. For the sake of clarity let's rename (a -> b -> c) to (r -> s -> t):

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

      Hence:

      1. r unifies with (a -> b).
      2. s unifies with a.
      3. t unifies with b.

      Therefore:

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

      This is equivalent to:

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

      That's all that there is to it.

      ---

      Edit:

      1. The flip function has one argument, (a -> b -> c), and one return value b -> a -> c.
      2. When you write flip ($), the ($) function becomes the first argument of the flip function.
      3. Hence the type signature of ($) is unified with the type signature of the argument of flip.
      4. Unification is the process of combining two terms into one term.
      5. In this case the two terms are (a -> b -> c) and (a -> b) -> a -> b.
      6. To unify them into one term (a -> b -> c) is first renamed to (r -> s -> t) and then r is substituted for (a -> b), s is substituted for a and t is substituted for b.

      For example, we could write a Prolog program to unify terms:

      % 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.
      

      A unification algorithm can be found here: http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse5

      To summarize the unification algorithm, when unifying term1 and term2:

      1. If term1 and term2 are constants then they unify if and only if they are the the same constant. For example Int only unifies with the constant Int. It doesn't unify with the constant Char.
      2. If term1 is a variable and term2 is a non-variable then term1 is instantiated to term2 (i.e. term1 := term2). Example, a and Int unify with a := Int.
      3. If term2 is a variable and term1 is a non-variable then term2 is instantiated to term1 (i.e. term2 := term1). Example, Int and b unify with b := Int.
      4. If term1 and term2 are both variables then they are both instantiated to one another and they are said to share values (i.e. term1 := term2 and term2 := term1). For example, a and b, when unified, become the same variable.
      5. If term1 and term2 are complex terms (e.g. term1 is Either a Int and term2 is Either Char b), then they unify if and only if:
         1. They have the same type constructor. For example, Maybe Int and Maybe Char have the same type constructor. However, Maybe Int and [Int] do not.
         2. Their corresponding arguments unify. For example in Either a Int and Either Char b, the arguments unify with a := Char and b := Int.
         3. The variable instantiations are compatible. For example, when unifying Either a a with Either Char Int, we first have a := Char and then a := Int. This is incompatible. Hence the two terms do not unify.

      6. Two terms unify if and only if it follows from the previous 5 clauses that they unify.

      这篇关于了解`flip（$）`的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！