# Haskell type of lambda expressions

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?

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

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.

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.
• @Kingvinst \y x -> x is valid because it's unambiguously clear what x means. It has the same type as \y -> \x -> x: p1 -> p2 -> p2. You can easily check those yourself with GHCi's :type command. May 5, 2020 at 15:21