Polymorphic types in Haskell

Question

I came across this function

iter p f x = if (p x) then x else (iter p f (f x))

and I thought I'd give a go at defining the polymorphic types myself to understand the concept.

My thought was the following:

The function takes 3 parameters, so we have t1 -> t2 -> t3 -> T

1. p is being used inside the if condition so it must return a bool, therefore t1 = a -> Bool

2. f is also the same type as p because it is passed as an argument in the else block, therefore t2 = a -> Bool

3. x is being used inside the if condition so it must return a bool, therefore t1 = a -> Bool

But when i checked the type in the ghci, the type they gave me was

iter :: (t -> Bool) -> (t -> t) -> t -> t

Can someone please explain the reasoning behind this.

Thanks

Answer 1

The function takes 3 parameters, so we have t1 -> t2 -> t3 -> T

This is correct as a starting point.

p is being used inside the if condition so it must return a bool, therefore t1 = a -> Bool

Correct.

f is also the same type as p because it is passed as an argument in the else block, therefore t2 = a -> Bool

Incorrect. f is never used in the same way as p. In the else block f is being applied to x and the result passed as the last argument to iter. From that we know f x must be the same type as x so f :: a -> a.

x is being used inside the if condition so it must return a bool, therefore t1 = a -> Bool

Incorrect. In the if condition x is being used only as an argument to p. You established above p :: a -> Bool. Therefore x :: a.

But when i checked the type in the ghci, the type they gave me was

iter :: (t -> Bool) -> (t -> t) -> t -> t

Correct. You could also write this replacing t with a to be consistent in the notation - we used a above:

iter :: (a -> Bool) -> (a -> a) -> a -> a

Answer 2

Let's evaluate it again:

iter p f x = if (p x) then x else (iter p f (f x))

iter takes three parameters (well technically speaking every function takes one parameter, but let's skip the details). So it has indeed a type t1 -> t2 -> t3 -> t.

Now in the if-then-else statement, we see (p x) this means that p x has to evaluate to a boolean. So that means that:

t1 ~ t3 -> Bool

Next we see x in the then statement. This may strike as non-important, but it is: it means that the output type t is the same as that of t3, so:

t3 ~ t

Now that means we already derived that iter has the type:

iter :: (t3 -> Bool) -> t2 -> t3 -> t3

Now we see in the else statement the call:

iter p f (f x)

So that means that f is a function f :: t4 -> t5. Since it takes x as input, its input type should be t3, and since the result of (f x) is passed to an iter function (that is not per se the same "grounded" iter function). So we have to inspect the call:

iter :: (u3 -> Bool) -> u2 -> u3 -> u3  -- call

Now since we call it with iter p f (f x) we definitely know that u3 ~ t3: because p has type t3 -> Bool. So it grounds further to:

iter :: (t3 -> Bool) -> u2 -> t3 -> t3  -- call

Sine (f x) is used as third argument, we know that the type of the result of f x should be t3 as well. So f has type f :: t3 -> t3. So we conclude that iter has the type:

iter :: (t3 -> Bool) -> (t3 -> t3) -> t3 -> t3