Polymorphic type of functions as parameter in haskell?

Question

Im trying to define the polymorphic type of the following function:

flip f x y = f y x

My thought was the following:

1. 1st parameter of flip, f takes two arguments so (t1 -> t2 -> t3)

2. 2nd parameter of flip, x is of type t1 because of the parameter t1 inside f function.

3. 3rd parameter of flip, y which is of type t3 because of the parameter t3 inside f function.

4. I don't know the polymorphic type of the overall return.

But when I checked the type in the ghci, I get:

flip :: (t2 -> t1 -> t) -> t1 -> t2 -> t

Can someone please help go through this example was to whats happening here?

Thanks

Answer 1

Your second assumption is wrong:

2nd parameter of flip, x is of type t1 because of the parameter t1 inside f function.

Let us first analyze the function:

flip f x y = f y x

We see that flip has three arguments in the head. So we first make the type:

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

We will of course now aim to fill in the types. With:

f :: a
x :: b
y :: c
flip f x y :: d

We see on the right hand side:

(f y) x

So that means that f is a function that takes as input y. So that means that a is the same type as c -> e (or shorter a ~ c -> e).

So now:

flip :: (c -> e) -> (b -> (c -> d))
f :: (c -> e)
x :: b
y :: c

Furthermore we see that:

(f x) y

So the result of (f x) is another function, with as input y. So that means that e ~ b -> f. Thus:

flip :: (c -> (b -> f)) -> (b -> (c -> d))
f :: c -> (b -> f)
x :: b
y :: c

Finally we see that (f y) x is the result of flip f x y. So that means that the type of the result of (f y) x is the same type as d. So that means that f ~ d. Which thus means that:

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

Or if we drop some redundant brackets:

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

Answer 2

This is just a matter of solving a system of equations. First, assign unknown types:

f : a1
x : a2
y : a3

Next, f is applied to y. So, f must be a function type with argument of the same type as y, that is

f : a1 = a3 -> a4
f y : a4

Similarily, f y is applied to x, so

f y : a4 = a2 -> a5
f y x : a5

Substituting this back, we get

f : a3 -> a2 -> a5
x : a2
y : a3

We can rename these types

t2 = a3
t1 = a2
t  = a5

and get

f : t2 -> t1 -> t
x : t1
y : t2

The function body is f y x, which has type t = a5.