Manual inferring type of (\x y z -> (x y) z)

Viewed 66

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.

1 Answers

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.

The fast way (for this function)

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

The "slow" way

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.

Related