Just trying to see the types of some lambda expressions like this one:
:t \x -> (\y -> x y)
\x -> (\y -> x y) :: (t1 -> t2) -> t1 -> t2
shouldn't the type here be t1->(t2->t1->t2) ?
Similarly
:t \x -> (\y -> (\k -> y (x k)))
\x -> (\y -> (\k -> y (x k)))
:: (t1 -> t2) -> (t2 -> t3) -> t1 -> t3
Shouldn't the type be t1->(t2->(t3->t2))?
:t \x -> (\y -> x y) \x -> (\y -> x y) :: (t1 -> t2) -> t1 -> t2shouldn't the type here be t1->(t2->t1->t2) ?
No, t1->(t2->t1->t2) is the same as t1->t2->t1->t2 which is the type of a three-arguments function (of type t1, t2, and t1) returning t2. However, there are only two lambdas, for the two arguments x and y.
The right type is instead
typeOfX -> (typeofY -> typeOfResult)
\x -> (\y -> x y)
(By the way, none of the parentheses above are needed.)
What is typeOfResult? Is is the type of x y, so it is the return type for x which must be a function.
In order for the code to type check, we must then have that typeOfX is a function type, say a -> b. In such case we can see that typeOfResult = b. Further, in x y we pass y to x, and this can type check only if typeOfY = a.
So,
typeOfX -> typeofY -> typeOfResult
=
(a -> b) -> a -> b
The compiler used names t1 and t2, but this is the same type.
Parentheses here matter, since we must remember that x is a function a -> b.
Without parentheses we would get a three-argument function, as explained above.
You can try to apply the same reasoning to the second example. Start from
typeOfX -> typeofY -> typeOfK -> TypeOfResult, and slowly discover what these types actually are.
The type of x in \x -> \y -> x y is t1 -> t2, and it's the first argument.
As the outermost lambda, it gets applied first, followed by y
You could've written it as \x y -> x y which is just function application in the natural order.
