Может кто-нибудь объяснить, как объединить типы (Haskell)?

Question

Может кто-нибудь объяснить унификацию типов в Haskell? Например: snd . snd :: (a1, (a2, c)) -> c

Пример

Как нам добраться, (a1, (a2, c)) -> c, от snd . snd?

Заранее благодарим за помощь.

Answer 1

Начните с

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

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

Применение (.) к snd со следующими парами

b ~ (x1, y1)
c ~ y1

даст

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

Теперь применим это к snd снова со следующими парами

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

дает

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

Это скрывает, откуда взялось y1. Но поскольку ~ - это симметри c, мы можем заменить y2 на (x1, y1), чтобы получить

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

, что эквивалентно (a1, (a2, c)) -> c с точностью до альфа-переименования.