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)

Answer 2

The type (a -> b) -> (c -> d) is equivalent to(a -> b) -> c -> d in haskells type system. You also need to consider, if x had type a, and f x has type b, then f has type a -> b. So let y = f x. So what is the type of f y === f (f x)?

Answer 3

Your Haskell command is fine.

Your type inference is incorrect though. The type of the x argument should unify with the type of the input to f, since you call f x, then the input type of f should unify with the output type of f since you call f on the result (f x).