Haskell Lambda functions - two seemingly equivalent functions, one works and the other is wrong

Question

This lambda function returns 1:

(\xy -> 1) 1 p 

where p = (\ xy → 1)

Well, that makes sense to me - the lambda function returns 1, regardless of its arguments.

Now this lambda function generates an error (error of infinite type):

  (\xy -> xyx) p 1 

That doesn't make sense to me. If this function is applied to the arguments here, then this is the result of substituting p for x and 1 for y:

  p 1 p 

Replace the first p by its definition:

  (\xy -> 1) 1 p 

Hey! Same as above that returned 1.

Question: why does (\ xy → 1) 1 p succeed, while (\ xy → xyx) p 1 fails?

/ Roger

Answer 1

In addition to what dflemstr said, the lamba type will never depend on the values ​​to which it applies. First, it checks the type of the lambda type, and then checks the correctness of its application.

Therefore, your argument that the expressions are the same after beta substitution does not matter: the lambda should be well printed, however, in isolation.

Answer 2

Take this expression (where both p must have the same type, because the lambda variable cannot have two types at the same time, unless you explicitly specify the polymorphic type):

 p 1 p 

What is type p in this context? Say 1 is an Int for simplicity. Start with a simple try:

 (p :: Int -> ? -> Int) 1 p 

So what is the question mark? Well, it must be type p , because the argument you give. So:

 (p :: Int -> (Int -> ? -> Int) -> Int) 1 p 

Again, the same problem, the same solution:

 (p :: Int -> (Int -> (Int -> ? -> Int) -> Int) -> Int) 1 p 

Now you understand why we have a problem with infinite types: although we do not need to know the type of the second argument p ; because a system like Haskell is strict (aka not lazy), it still needs to know the type and focus on this infinite type.

This code succeeds:

 (\xy -> 1) 1 p 

... because the function on the left can have a different type from p , because they are different functions, so we are not trying to combine these types:

 ((\ xy -> 1) :: a -> b -> Int) 1 (p :: c -> d -> Int)