In Edward Kmett's talk Lenses, Folds, and Traversals, on the slide "The Power is in the Dot", he shows the type of (.) . (.) . (.)
is
(a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b
I can see it by showing its type in GHCI. But I'd also like to know why. The other thing I'd like to understand is why there's the pattern in the regular change of parameters from (.)
to (.) . (.)
and (.) . (.) . (.)
:
(.) :: (a -> b) -> (c -> a) -> c -> b
(.) . (.) :: (a -> b) -> (c -> d -> a) -> c -> d -> b
(.) . (.) . (.) :: (a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b
P.S. I tried to resolve (.) . (.)
myself by expanding the function definition of (.) . (.)
. After applying the definition of (.)
I got:
\x y z t -> x ((y z) t)
So I inferred the types:
x :: a -> b
y :: c -> d -> a
z :: c
t :: d
However I got lost on (.) . (.) . (.)
. And I don't know if this is the right way to do manual type inference.
With functions,
instance Functor ((->) r) where
-- fmap :: (a -> b) -> f a -> f b
-- (a -> b) -> (r -> a) -> (r -> b)
fmap p q x = p (q x) -- fmap = (.)
so what you actually have is fmap . fmap . fmap
:
fmap :: (a -> b) -> f a -> f b
fmap . fmap :: (a -> b) -> f (g a) -> f (g b)
fmap . fmap . fmap :: (a -> b) -> f (g (h a)) -> f (g (h b))
which is
(a -> b) -> (c -> (d -> (e -> a))) -> (c -> (d -> (e -> b))) ~
(a -> b) -> (c -> d -> e -> a) -> (c -> d -> e -> b)
Why is fmap . fmap :: (a -> b) -> f (g a) -> f (g b)
? Because,
(fmap . fmap) foo = fmap (fmap foo)
{-
fmap :: (a -> b) -> f a -> f b
foo :: a -> b
fmap foo :: f a -> f b
fmap foo :: g a -> g b
fmap (fmap foo) :: f (g a) -> f (g b)
-}
Mechanical type derivation is all about substitution and consistent renaming of type variables. See more e.g. here or here.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With