Verify the type of a lambda expression

Question

I need to verify the type for the lambda expression: $\lambda f.\lambda x.f (f x)$

My method gives me: $(a\rightarrow c)\rightarrow b\rightarrow c$

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?

I'm afraid that questions about software programming languages (such as Haskell) are off-topic here. Sorry. You might try StackOverflow. But first do some research (e.g., reading about the Haskell type system). And, don't re-post on StackOverflow. You can click the flag button underneath your question to ask the moderators to migrate the question to StackOverflow, if you like. — D.W., Mar 19, 2014 at 6:45
@D.W. This is not a question about Haskell. Haskell is only used as a tool to check the answer, which is lambda-calculus. — babou, Mar 19, 2014 at 17:53
If this question is "What is the type of the following expression in the lambda calculus?", that is not a very useful question either. Our mission is to build a high-quality archive of questions and answers that will be useful not only to the original author but to others as well. The chances that the question "what's the type of the following very specific expression in the lambda calculus?" is useful to anyone else seems minimal to me. "In general, How do I tell the type of a expression in the lambda calculus" might be a better question, but the answer to that might be: read a textbook. — D.W., Mar 19, 2014 at 21:15

babou · Accepted Answer · 2014-03-19 17:51:33Z

1

Haskell is right.

I do not know whether your Haskell syntax is correct, though it looks plausible to me, but the Haskell typing is the right one.

Since $f$ is applied to the result of $f(x)$, $f$ must be of type $a\rightarrow a$, $a$ being the type of $x$.

answered Mar 19, 2014 at 17:51

babou

19.4k40 silver badges76 bronze badges

Add a comment |

1 Answer 1