Search code examples
haskellcurryingpointfree

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


(.) takes two functions that take one value and return a value:

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

Since (.) takes two arguments, I feel like (.).(.) should be invalid, but it's perfectly fine:

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

What is going on here? I realize this question is badly worded...all functions really just take one argument thanks to currying. Maybe a better way to say it is that the types don't match up.


Solution

  • 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.