Understanding Type of `flip ($)`

Question

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

Answer 1

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.

Answer 2

Unflipped $ gets a value of type a on its right side and applies it to the function (a -> b) from its left side: func $ value is the same as func value.

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

Answer 3

Line up corresponding components of the types:

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

Important rule: in any type signature, you can replace every occurrence of a type variable with another that doesn't appear anywhere in the same signature, and get a type that is completely equivalent to the original. (Types don't care about the names of the type variables, only which variables are equal and which are different within the same signature.) So we can rename type variables slightly in flip (a := x, b := y, c := z) and it's the same type:

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

Slightly different rule: in any type signature, we can replace all instances of a type variable with any type and get a specialized version of that type. Let's specialize flip to the type that makes it compatible with ($). We do that 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 of ($), we can figure out the type of flip ($):

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

Now we replace b := c, and after that, a := b:

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