(Compose) Compose (Compose).md

(Compose) Compose (Compose)

Motivation

Multiple times I've wanted to understand how to derive the following by hand:

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

Which is the point free version of:

compose2 :: (c -> d) -> (a -> b -> c) -> a -> b -> d
compose2 f1 f2 = (f1 . ) . f2

Here f2 takes 2 parameters and f1 takes one.

The default (.) composes functions that take one parameter. If you want a function like compose2 which lets the first function exectuted, i.e. f2, take 2 parameters you need something like compose2 or better yet (.).(.).

Derivation

First thing to do when doing Type Tetris™ is to make sure that you don't get confused by all the a's, b's and c's. So let's first rewrite the function prefixed and lets label the two different compose functions with subscripts:

(.)ₐ . (.)ₓ == (.) (.)ₐ (.)ₓ

Then let's create unique type parameter names for each compose function:

(.)ₓ :: (y -> z) -> (x -> y) -> (x -> z)
(.)ₐ :: (b -> c) -> (a -> b) -> (a -> c)
(.)  :: (s -> t) -> (r -> s) -> (r -> t)

Now we're ready to apply (.)ₐ to (.):

(.) (.)ₐ :: ???

Here's where it can can confusing. Let's make it easier by adding redundant parenthesis to (.) and (.)ₐ and line them up with each other to help us keep track of things:

(.)  :: (   s     ->           t          ) -> ((r -> s) -> (r -> t))
(.)ₐ :: ((b -> c) -> ((a -> b) -> (a -> c))

Once we do the application, we can see the following is true:

s = b -> c
t = ((a -> b) -> (a -> c))

Next we substitute into the remaining parameters of (.), viz. (r -> s) -> (r -> t):

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

Now to make things easier we remove redundant parenthesis. This can only be done on the right-hand side since -> commutes to the right. To make sure that we understand how this is done, we'll do it one step at a time:

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

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

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

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

This simplified form will help us with the next step which is to apply (.)ₓ to (.) (.)ₐ. We line things up again to get the substitution values:

(.) (.)ₐ :: (  r     ->    b     ->    c   ) -> r -> (a -> b) -> a -> c
(.)ₓ     :: (y -> z) -> (x -> y) -> (x -> z)

So our new substitutions are:

r = y -> z
b = x -> y
c = x -> z

So applying those substitutions to the remaining parts of (.) (.)ₐ, viz. r -> (a -> b) -> a -> c we get:

(.) (.)ₐ (.)ₓ :: (y -> z) -> (a -> (x -> y)) -> a -> (x -> z)

And removing redundant parenthesis like before one step at a time yields:

(.) (.)ₐ (.)ₓ :: (y -> z) -> (a -> x -> y) -> a -> (x -> z)

(.) (.)ₐ (.)ₓ :: (y -> z) -> (a -> x -> y) -> a -> x -> z

Now we should see if we can make it look like the very first signature which is:

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

To do that, the following substitutions are needed:

y = c
z = d
a = a
x = b

Giving us:

(.) (.)ₐ (.)ₓ :: (c -> d) -> (a -> b -> c) -> a -> b -> d

And we have successfully survived Type Tetris™.