Verify the type of a lambda expression

Question

I need to verify the type for the lambda expression:

My method gives me:

Im trying to define it in Haskell (on Hugs) like this:

h= \f x -> f (f x)

When i call the :type comamnd it gives me:

(a -> a) -> a -> a

Is mi function correctly defined in Haskell?, or my method gives me a wrong result?

Answer 1

Note that f gets called with both x and f x as its argument—this immediately means that the type of x and the type of f x must be the same[1]. Carrying this argument onward, we see that since x is the input to f and f x is the output of f, the input and output of f must be the same[2].

Finally, we examine the lambda term

\f x -> f (f x)

it has two inputs, f (a function) and x, and it returns whatever the return type of f is[3]. Putting all of this information together we have

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

where:

  b ~ c        by [1]
  a ~ b        by [2]
  d ~ b        by [3]

thus the type which Haskell inferred is correct

h :: (a -> a) -> a -> a
h f x = f (f x)