I'm trying to derive the type of (.) (foldr(++)) (map (:))
I start by deriving the type of foldr (++)
foldr :: (a1 -> b1 -> b1) -> b1 -> [a1] -> b1
(++) :: [a2] -> [a2] -> [a2]
a1 ~ [a2]
b1 ~ [a2]
b1 ~ [a2]
So
foldr (++) :: [a2] -> [[a2]] -> [a2] ~ [a] -> [[a]] -> [a]
Then I derive the type of map (:)
map :: (a1 -> b1) -> [a1] -> [b1]
(:) :: a2 -> [a2] -> [a2]
a1 ~ a2
b1 ~ [a2] -> [a2]
So
map (:) :: [a2] -> [[a2] -> [a2]] ~ [a] -> [[a] -> [a]]
Finally the type of (.) (foldr(++)) (map (:))
(.) :: (b1 -> c1) -> (a1 -> b1) -> a1 -> c1
map (:) :: [a2] -> [[a2] -> [a2]]
foldr (++) :: [a3] -> [[a3]] -> [a3]
b1 ~ [a2]
c1 ~ [[a2] -> [a2]]
a1 ~ [a3]
b1 ~ [[a3]] -> [a3]
So I get
(.) (foldr(++)) (map (:)) :: a1 -> c1 ~ [a3] -> [[a2] -> [a2]]
But if I ask GHCi for :t (.) (foldr(++)) (map (:)) I get (.) (foldr(++)) (map (:)) :: [a] -> [[[a] -> [a]]] -> [[a] -> [a]]
Which is different from my result, any help to derive the same result?
Thanks,
Sebastián.
In the final step, you mix up the argument oder. You unify b1 -> c1 with the type of map (:), but you should unify it with the type of foldr (++).
More generally, you might want to learn how to debug such complicated calculations yourself. It is good that you do a sanity check at the end (in this case, by checking the result with ghci). If the sanity check doesn't work, a good next step can be to say or write down what each step is and why you did it. In this case, you would say "and then I unify b1 -> c1 with the type of map (:) because ...", and there you would find the bug because there's no reason to do this.
Maybe rubber duck debugging works for you, where you explain your code to a rubber duck and by explaining, you see what's wrong about the code. .