Haskell type of lambda expressions

Question

I'm new to Haskell and have some general questions.

Question 1: The Haskell expression (\x -> \x -> x) is the same as the λ-term λx.λx.x The type of this expression is p1 -> p2 -> p2. What does this mean?

Question 2: λyx.x is shorthand for λy.λx.x. In Haskell (\y x -> x) is shorthand for (\y -> \x -> x). Do (\x x -> x) and (\x -> \x -> x) have the same type in Haskell and why?

Answer 1

Contrary to Church's lambda calculus, Haskell is typed.

Answer 1

When types are denoted with lower-case letters (such as p1 and p2) that indicates a type variable. When types are denoted with capital letters (e.g. Bool or Int) they're concrete types.

The type p1 -> p2 -> p2 indicates a function in curried form. You can think of it as a function that takes a p1 value as input and returns a new function of the type p2 -> p2, or you can think of it as a function that takes p1 and p2 as inputs, and returns p2 as output. The right-most type indicates the return type.

The types p1 and p2 are here unconstrained, which means that they can be literally any type - Bool, Int, or your own custom type(s). They can also be equal. For example, both p1 and p2 could be Bool.

The interpretation of p1 -> p2 -> p2 as a function that takes p1 as input and returns a function with the type p2 -> p2 makes most sense. What really happens is that in the expression \x -> \x -> x the second x shadows the first x. If you think of the expression as \x -> (\x -> x), you can see that the returned function is \x -> x, and that it doesn't matter what the 'leftmost' x was. Thus, the type of the leftmost x is irrelevant because the value is never used. It'd be more idiomatic to write the expression as \_ -> \x -> x. The underscore is Haskell's wildcard placeholder, indicating that there's a variable there, but we don't care about it.

In the expression \x -> x, however, the input value is being returned unmodified, so that the type must be p2 -> p2 - i.e. the output type must be the same as the input type.

The expression \x -> x is the identity function, and it's already built into Haskell as the function id. Likewise, a function that ignores its input and instead always returns the same result is called const. Thus, the expression \x -> \x -> x is equivalent to const id.

Answer 2

The expression \x x -> x is invalid in Haskell. It would indicate a (curried) function that takes two arguments, but returns a value. Which one of them? Keep in mind that they could be different.

In Haskell, variables are bound to input arguments, but the binding must be unambiguous. That's the way that the language works, but it's quite a standard design.

For an example of a language that behaves differently you might look to Erlang, where a function that receives two arguments with the same variable name indicates a pattern-match where the match only succeeds if the arguments are equal to each other. Erlang is the only language I'm aware of that does it that way, but I only know a handful of languages...