How to manually infer the type of '(.) . (.) . (.)'?

Question

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.

Gigantean

You might like the "semantic editor combinators" view of function composition, where we rename (.) to result. The intuition given in this post is quite nice, and in my opinion makes it quite clear why stacking compositions of (.) results in the types it does. – Subsoil

@DanielWagner, thanks for the link. I'll read it soon. Actually I was about to google 'semantic editor combinators' as Edward mentioned it a lot in the talk. – Gigantean

Answer 1

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.

Retrospection

Thanks for the beautiful answer. It answers both of my questions:). – Gigantean

Answer 2

(.) . (.) . (.) reduces in two steps: first reduce dots without parentheses around:

((.) . (.) . (.)) f = (.) ((.) ((.) f))
                    = (.) ((.) (f .))
                    = (.) ((f .) .)
                    = ((f .) .) .)

second reduce the remaining expression

((f .) .) .) g = ((f .) .) . g
               = \x -> ((f .) .) (g x)
               = \x -> (f .) . g x
               = \x y -> (f .) (g x y)
               = \x y -> f . g x y
               = \x y z -> f (g x y z)

So first you compose n dots in parentheses using n - 1 dots. Then you apply this construction to functions f :: a -> b and g and get (...((f .) .) ... .) g where each dot corresponds to an argument that g receives — that's why there is a pattern: each dot in parentheses handles one argument of g and you need another dot to compose this dot with all previous. After all reductions the expression becomes

\x1 x2 ... xn -> f (g x1 x2 ... xn)

and its type is obvious.

---

One nice thing is that if we would have postfix operators we could write (the code is in Agda)

open import Function renaming (_∘′_ to _∘_) using ()

_% = _∘_

postulate
  a b c d e : Set
  f : a -> b
  g : c -> d -> e -> a

fg : c -> d -> e -> b
fg = f % % ∘ g

instead of ((f .) .) . g.

Dearth

Thanks! That is what I initially tried to achieve. If I could mark two correct answers, I would mark you answer as correct too. – Gigantean