How to find the type of (\x y z -> x . y z)

Question

I'm trying to find the type of (\x y z -> x . y z) but haven't had any success in finding the same type as ghci

(\x y z -> x . y z) :: (b -> c) -> (t -> a -> b) -> t -> a -> c

After removing the infix functions and getting (\x y z -> (.) x (y z)), I'm not sure how to proceed.

In general, you would try to find the type of any sub-expression. The type of (.) is known, and from that you can deduce the types of x and (y z). Maybe try starting with that. — Paul Georg Podlech, Jul 31 '18 at 08:52

score 5 · Answer 1 · edited Jul 31 '18 at 17:58

Work backwards, and assign type variables until they are specified:

-- We assign types one by one:
(.) x (y z) :: a -- So,
(y z) :: b
(.) x :: b -> a
x :: c
(.) :: c -> b -> a

But we know that (.) :: (y -> z) -> (x -> y) -> (x -> z), so, we can equate some types, written with ~:

c ~ y -> z
b ~ x -> y
a ~ x -> z

We now know that:

x :: y -> z
(.) x (y z) :: x -> z
y z :: x -> y

So

z :: d
y :: d -> x -> y

Finally, we just complete the type of the function

--                     (type of x) (Type of y) (type of z) (return type)
(\x y z -> x . y z) :: (y -> z) -> (d -> x -> y) -> d -> (x -> z)

Finally, we can ask GHCi for confirmation:

Prelude> :t (\x y z -> x . y z)
(\x y z -> x . y z) :: (b -> c) -> (t -> a -> b) -> t -> a -> c

You should note, that you can omit the brackets in the return type to match the signature that ghc calculates. — Paul Georg Podlech, Jul 31 '18 at 08:55

Aadit M Shah · Answer 2 · 2018-07-31T09:11:32.720

We can expand the expression \x y z -> x . y z as follows:

  \x y z   -> x . y z
≡ \x y z w -> x (y z w) -- because (f . g) ≡ (\x -> f (g x))
≡ \f g x y -> f (g x y) -- renaming the variables

Now, we can look at the types:

x :: a1
y :: a2

-- Because g is applied to x and y:

g :: (a1 -> a2 -> b)

-- Because f is applied to (g x y):

f :: (b -> c)

-- Therefore:

(\f g x y -> f (g x y)) :: (b -> c) -> (a1 -> a2 -> b) -> a1 -> a2 -> c
                        -- └──┬───┘    └──────┬──────┘    │     │
                        --    f               g           x     y

As you can see, this function just composes f and g:

          ┌───────┐       ┌───────┐
x :: a1 ──┤       │       │       │
          │   g   ├── b ──┤   f   ├── c
y :: a2 ──┤       │       │       │
          └───────┘       └───────┘

For more information, take a look at the following question and answer: What does (f .) . g mean in Haskell?

How to find the type of (\x y z -> x . y z)

2 Answers2