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 Reader
s is like having multiple independent kinds of global, immutable state.
Or like having multiple input arguments which aren't being affected by the fmap
ing. 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.