What is the type of flip id
?
\[ flip :: (a \rightarrow b \rightarrow c) \rightarrow (b \rightarrow a \rightarrow c) \\ id :: x \rightarrow x \]
Because id
is the parameter of flip
, we can solve
\[
(a \rightarrow (b \rightarrow c)) \sim (x \rightarrow x)
\]
to get
\[
\\\begin{cases}
a \sim x
\\(b \rightarrow c) \sim x
\end{cases}
\]
and thus $a \sim (b \rightarrow c)$. Because the type of flip id
is just its result type, i.e. $b \rightarrow a \rightarrow c$, we conclude that its type is
\[
b \rightarrow (b \rightarrow c) \rightarrow c
\]