Can someone explain how to unify types(Haskell)?

Question

Can someone explain type unification in Haskell? For example: snd . snd :: (a1, (a2, c)) -> c

Example

How do we get to, (a1, (a2, c)) -> c, from snd . snd?

Thanks in advance for the help.

Answer 1

Start with

snd :: (x1, y1) -> y1
snd :: (x2, y2) -> y2

(.) :: (b -> c) -> (a -> b) -> a -> c

Applying (.) to snd, with the following pairings

b ~ (x1, y1)
c ~ y1

yields

-- (.) :: (   b    -> c ) -> (a ->     b   ) -> a -> c
-- snd :: (x1, y1) -> y1
(.) snd ::                   (a -> (x1, y1)) -> a -> y1

Now applying this to snd again with the following pairings

a        ~ (x2, y2)
(x1, y1) ~ y2

yields

-- (.) snd :: (   a    -> (x1, y1)) -> a -> y1
-- snd ::     (x2, y2) ->     y2
(.) snd snd ::                      (x2, y2) -> y1

This obscures where y1 comes from. But since ~ is symmetric, we can replace y2 with (x1, y1) to yield

(.) snd snd  :: (x2, (x1, y1)) -> y1

which is equivalent to (a1, (a2, c)) -> c up to alpha renaming.