Composing function composition: How does (.).(.) work?

Let's first play typechecker for the mechanical proof. I'll describe an intuitive way of thinking about it afterward.

I want to apply (.) to (.) and then I'll apply (.) to the result. The first application helps us to define some equivalences of variables.

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

let b = (b' -> c') 
    c = (a' -> b') -> a' -> c'

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

Then we begin the second, but get stuck quickly...

let a = (b'' -> c'')

This is key: we want to let b = (a'' -> b'') -> a'' -> c'', but we already defined b, so instead we must try to unify --- to match up our two definitions as best we can. Fortunately, they do match

UNIFY b = (b' -> c') =:= (a'' -> b'') -> a'' -> c''
which implies 
      b' = a'' -> b''
      c' = a'' -> c''

and with those definitions/unifications we can continue the application

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

then expand

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

and clean it up

substitute b'' -> b
           c'' -> c
           a'  -> a
           a'' -> a1

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

which, to be honest, is a bit of a counterintuitive result.

Here's the intuition. First take a look at fmap

fmap :: (a -> b) -> (f a -> f b)

it "lifts" a function up into a Functor. We can apply it repeatedly

fmap.fmap.fmap :: (Functor f, Functor g, Functor h) 
               => (a -> b) -> (f (g (h a)) -> f (g (h b)))

allowing us to lift a function into deeper and deeper layers of Functors.

It turns out that the data type (r ->) is a Functor.

instance Functor ((->) r) where
   fmap = (.)

which should look pretty familiar. This means that fmap.fmap translates to (.).(.). Thus, (.).(.) is just letting us transform the parametric type of deeper and deeper layers of the (r ->) Functor. The (r ->) Functor is actually the Reader Monad, so layered Readers is like having multiple independent kinds of global, immutable state.

Or like having multiple input arguments which aren't being affected by the fmaping. Sort of like composing a new continuation function on "just the result" of a (>1) arity function.

It's finally worth noting that if you think this stuff is interesting, it forms the core intuition behind deriving the Lenses in Control.Lens.

Let’s ignore types for a moment and just use lambda calculus.

• Desugar infix notation:
  (.) (.) (.)

• Eta-expand:
  (\ a b -> (.) a b) (\ c d -> (.) c d) (\ e f -> (.) e f)

• Inline the definition of (.):
  (\ a b x -> a (b x)) (\ c d y -> c (d y)) (\ e f z -> e (f z))

• Substitute a:
  (\ b x -> (\ c d y -> c (d y)) (b x)) (\ e f z -> e (f z))

• Substitute b:
  (\ x -> (\ c d y -> c (d y)) ((\ e f z -> e (f z)) x))

• Substitute e:
  (\ x -> (\ c d y -> c (d y)) (\ f z -> x (f z)))

• Substitute c:
  (\ x -> (\ d y -> (\ f z -> x (f z)) (d y)))

• Substitute f:
  (\ x -> (\ d y -> (\ z -> x (d y z))))

• Resugar lambda notation:
  \ x d y z -> x (d y z)

And if you ask GHCi, you’ll find that this has the expected type. Why? Because the function arrow is right-associative to support currying: the type (b -> c) -> (a -> b) -> a -> c really means (b -> c) -> ((a -> b) -> (a -> c)). At the same time, the type variable b can stand for any type, including a function type. See the connection?

Here is a simpler example of the same phenomenon:

id :: a -> a
id x = x

The type of id says that id should take one argument. And indeed, we can call it with one argument:

> id "hello" 
"hello"

But it turns out what we can also call it with two arguments:

> id not True
False

Or even:

> id id "hello"
"hello"

What is going on? The key to understanding id not True is to first look at id not. Clearly, that's allowed, because it applies id to one argument. The type of not is Bool -> Bool, so we know that the a from id's type should be Bool -> Bool, so we know that this occurrence of id has type:

id :: (Bool -> Bool) -> (Bool -> Bool)

Or, with less parentheses:

id :: (Bool -> Bool) -> Bool -> Bool

So this occurrence of id actually takes two arguments.

The same reasoning also works for id id "hello" and (.) . (.).