I would like to understand how to get manual to the correct type of this Haskell expression.
(\x y z -> (x y) z)
In general I understand roughly how to manually determine the correct type, but with lambda expressions I am totally confused.
I would like to understand how to get manual to the correct type of this Haskell expression.
(\x y z -> (x y) z)
In general I understand roughly how to manually determine the correct type, but with lambda expressions I am totally confused.
There's a fast way to get the type and a slow way. The slow way is below and does not remove any unnecessary parentheses.
Let us remember the properties of Haskell functions, namely for
f :: a -> b -> c
Both f x y and (f x) y are the same, as a -> b -> c is a -> (b -> c).
Thus \x y z -> (x y) z is the same as \x y z -> x y z. Therefore, if y's and z's type where a and b resp., then x's type is a -> b -> c:
\x y z -> x y z :: (a -> b -> c) -> a -> b -> c
If we named that function, then we would write:
f :: (a -> b -> c) -> a -> b -> c
f x y z = x y z
or even simpler:
f :: (a -> b -> c) -> a -> b -> c
f = id
as it is the identify function restrained to a function type. You can add parentheses around a -> b -> c in the type to see that, as a -> b -> c is a -> (b -> c):
f :: (a -> b -> c) -> (a -> b -> c)
f = id
Let's start first by giving the lambda a name. This will enable us to use type signatures and continue from there:
f = \x y z -> (x y) z
Next, we use the regular function syntax instead of the lambda syntax:
f :: A -> B -> C -> D
f x y z = (x y) z
Now, we need to figure out A, B, C and D. Due to x being applied to y, we notice that A must be some function type, e.g. B -> ...?. Next we notice that x y must also be a function. Therefore, A needs to be B -> G, and G needs to be a function again. Since G is able to use z and therefore a value of type C, we know that G is G = C -> D:
f :: (B -> (C -> D)) -> B -> C -> D
We now have x's type, it's B -> (C -> D). Since neither y nor z are restrained, we can now change all type placeholders into type varialbles and end up with:
f :: (b -> (c -> d)) -> b -> c -> d
f x y z = (x y) z
For a last step, let's rename those variables:
f :: (a -> (b -> c)) -> a -> b -> c
f x y z = (x y) z
And that's \x y z -> (x y) z's type: (a -> (b -> c)) -> a -> b -> c.