Im trying to define the polymorphic type of the following function:
flip f x y = f y x
My thought was the following:
1st parameter of flip
, f
takes two arguments so (t1 -> t2 -> t3)
2nd parameter of flip
, x
is of type t1
because of the parameter t1
inside f
function.
3rd parameter of flip
, y
which is of type t3
because of the parameter t3
inside f
function.
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
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