0

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.

Caramiriel
  • 7,029
  • 3
  • 30
  • 50
xyz123
  • 1
  • 1
    This is a very broad question. You will want to find a text or tutorial that covers this as it's a complex subject. This question has been asked before at https://stackoverflow.com/questions/17148385/unifying-types-in-haskell – bsoist Aug 03 '20 at 14:07
  • unify them structurally. – Will Ness Aug 03 '20 at 14:30

1 Answers1

3

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.

chepner
  • 497,756
  • 71
  • 530
  • 681