Just looking for an explanation of the type of this function, please
In functional programming this refers to the study of the type of returned values.
f x y z = x y (y z)
Prelude is the haskell interpreter which solves it as:
f :: ((b -> a) -> a -> c) -> (b -> a) -> b -> c
But I'm not able getting that result with any known method ¬¬
Best regards.
Ugh, those “manually typecheck this expression” exercises are so silly. I don't know why lecturers keep putting them in assignments.
In practice, what's actually much more relevant is to go the other way around: given a type, find an implementation. So let me answer the question from that angle: you already know
f :: ((b -> a) -> a -> c) -> (b -> a) -> b -> c
-- └──────────────────┘ └──────┘ └─┘
...so you have three arguments to accept, reasonable enough to call them x, y and z
f x y z = _
You're in the end looking for a c, and the only c you have available is in the final result of x
x :: (b -> a) -> a -> c
-- └──────┘ └─┘
...which requires two arguments
f x y z = x _ _
...of types b -> a and a. Let's check what we have available
y :: b -> a
z :: b
Great, we can directly use y as the first argument
f x y z = x y _
For the second argument we need an a. Well, z is a b, that doesn't work, but y yields an a when given a b, so we can pass y z and thus end up with
f x y z = x y (y z)
or as we prefer to write it in Haskell, f x y = x y . y.
Now for the other way around: let's start with the η-reduced form
f x y = x y . y
This is a pipeline, so let's start giving the passing-through argument a name p
x y . y :: p -> _
That argument is passed first to y, so we have
y :: p -> _
from which it follows, since y is also the first argument to x
x :: (p -> _) -> _
Furthermore, x then accepts (in the pipeline) whatever comes out of y
y :: p -> r
x :: (p -> r) -> r -> _
Let's call the final result q
y :: p -> r
x :: (p -> r) -> r -> q
And write up the whole function as given:
(\x y -> x y . y) :: ((p -> r) -> r -> q) -> (p -> r) -> p -> q
-- └─────────x────────┘ └──y───┘
Which is, after renaming the type variables, the same as what you started with.