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

Question

This Lambda function returns 1:

  (\x y -> 1) 1 p

where p = (\x y -> 1)

Okay, that makes sense to me -- the Lambda function returns 1, independent of its arguments.

Now, this Lambda function generates an error (infinite type error):

  (\x y -> x y x) p 1

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

  p 1 p

Replace the first p by its definition:

  (\x y -> 1) 1 p

Hey! That’s identical to the above, which returned 1.

Question: why does (\x y -> 1) 1 p succeed whereas (\x y -> x y x) p 1 fail?

/Roger

Answer 1

Take this expression (Where both p's have to have the same type, because a lambda variable cannot have two types simultaneously if you don't explicitly specify a polymorphic type):

p 1 p

What is the type of p in this context? Let's say that 1 is an Int for simplicity. Let's start with a simple attempt:

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

So, what's the question mark? Well, it has to be the type of p because that's the argument that you're giving. So:

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

Again, same problem, same solution:

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

Now you understand why we have a problem with infinite types: While we don't need to know the type of the second argument of p; because the Haskell type system is strict (aka not lazy), it needs to find out the type anyways, and gets stuck with this infinite type.

This code succeeds:

(\x y -> 1) 1 p

... because the function to the left can have a different type from p, because they are different functions, so we don't get the same problem when trying to unify the types:

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

Answer 2

In addition to what dflemstr said, the type of the lamba will never depend on the values it is applied to. The type checker will first find the type of the lambda and then check if it is applied correctly.

Hence, your arguing that after beta substitution the expressions are the same is irrelevant: the lambda must be well typed nonetheless in isolation.