Understanding type `flip ($)`

Question

Look at type ($) and flip :

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

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

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

Answer 1

Pretty simple:

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

Therefore, we essentially combine (a -> b -> c) with (a -> b) -> a -> b . For clarity, rename (a -> b -> c) to (r -> s -> t) :

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

Hence:

• r combines with (a -> b) .
• s combines with a .
• t combines with b .

In this way:

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

This is equivalent to:

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

That is all there is to him.

---

Edit:

• The flip function has one argument, (a -> b -> c) and one return value b -> a -> c .
• When you write flip ($) , the function ($) becomes the first argument to the flip function.
• Therefore, a signature of type ($) unified with a signature of type argument flip .
• Unification is the process of combining two terms into one term.
• In this case, two members: (a -> b -> c) and (a -> b) -> a -> b .
• To combine them into one term (a -> b -> c) , it is first renamed to (r -> s -> t) , and instead of r is replaced (a -> b) , s is replaced by a , and t is replaced by 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. 

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

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

• If term1 and term2 are constants, then they are combined if and only if they are one and the same constant. For example, Int only combined with the constant Int . It does not combine with the constant Char .
• If term1 is a variable and term2 is non-variable, then term1 is created on term2 (i.e. term1 := term2 ). Example: unify a and Int with a := Int .
• If term2 is a variable and term1 is non-variable, then term2 is created on term1 (i.e. term2 := term1 ). Example: unify Int and b with b := Int .
• If term1 and term2 are both variables, then they are both created with each other and say that they have common values ​​(i.e. term1 := term2 and term2 := term1 ). For example, a and b , when unified, become the same variable.
• If term1 and term2 are complex terms (for example, term1 is Either a Int and term2 is Either Char b ), then they are combined if and only if:
  • They have the same type of constructor. For example, Maybe Int and Maybe Char have the same constructor type. However, Maybe Int and [Int] do not.
  • Their respective arguments are combined. For example, in Either a Int and Either Char b arguments are combined with a := Char and b := Int .
  • Instance variables are compatible. For example, when combining Either aa with Either Char Int we first have a := Char , and then a := Int . This is incompatible. Therefore, the two members are not combined.
• Two members are combined if and only if it follows from the previous 5 sections that they combine.

Answer 2

Align the appropriate type components:

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

An important rule: in any type signature, you can replace each occurrence of a type variable with another that does not appear anywhere in the same signature and get a type that is completely equivalent to the original. (Types do not care about the names of type variables, only those variables are equal and differ within the same signature.) Thus, we can rename the type variables a little in flip ( a := x , b := y , c := z ) and the same type:

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

A slightly different rule: in a signature of any type, we can replace all instances of a variable of a type with any type and get a specialized version of this type. Let me specialize flip to the type that makes it compatible with ($) . We do this by replacing x := (a -> b) , y := a and z := b :

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

Now that the type of the first argument of this specialized version of flip matches the type ($) , we can determine the type flip ($) :

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

Now replace b := c , and then a := b :

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

Answer 3

Unflipped $ takes a value of type a on the right side and applies it to a function (a -> b) on the left side: func $ value matches the func value .

Flipped $ takes a value of type b on the left side and applies the function (b->c) on the right side to it: value `flip ($)` func same as func value .