Instantly share code, notes, and snippets.

Embed
What would you like to do?
Compositions of compositions in Haskell, pursuant to https://github.com/ekmett/lens/wiki/Derivation
In https://github.com/ekmett/lens/wiki/Derivation, we see some types for
composition of compositions: (.).(.), (.).(.).(.), and so on. Let's prove that
the type of (.).(.) is (a -> b) -> (c -> d -> a) -> c -> d -> b, as stated in
the site. We'll stick with prefix notation, meaning that we want the type of
(.)(.)(.).
Recall the type of composition. This should be intuitive:
(.) :: (b -> c) -> (a -> b) -> a -> c [1]
Apply this to a function of type b -> c. Be concrete so that we don't get fooled
by renaming and unification in the type-checker. Start with a function of type
(b = Int) -> (c = String).
((\x -> show x) :: Int -> String) :: Int -> String [2]
( (.) ((\x -> show x) :: Int -> String) ) :: (a -> Int) -> a -> String [3]
This is good: the combination ((.) ...) is waiting for an (a -> Int); when it
gets one, it will yield an (a -> String), as expected.
What if we feed (.) to (.)? Look at the type of the second (.) and map its
components to (Int -> String) from the first example.
(.) :: (b -> c) -> (a -> b) -> a -> c [4]
`--.---' `-------.--------'
~~~ :: Int -> String
Replace Int with (b -> c) and String with (a' -> b) -> a' -> c in equation 3,
(the two a's are different) we get an expected type for (.) (.):
(a -> Int) -> a -> String
,--'--. ,---------'--------.
((.)(.)) :: (a -> b -> c) -> a -> (a' -> b) -> a' -> c [5]
does GHCi agree?
((.)(.)) :: (a1 -> b -> c) -> a1 -> (a2 -> b) -> a2 -> c [6]
Yup, with a <- a1 and a' <- a2. This is hard to intuit, so go back to concrete
types. ((.)(.)) is waiting for a another function. Remember that ((.) ...) is
waiting for an (a -> Int), and, when it gets one, will yield a (a -> String).
Our new thing, ((.)(.)), must be waiting for an (a1 -> b -> c), and, when it
gets one, will yield an a1 -> (a2 -> b) -> a2 -> c. Try giving it an Int ->
String -> Bool, that is, a function where a1 == Int, b == String, and c == Bool.
One such function is:
(\x -> \y -> show x == y) :: Int -> String -> Bool [7]
Test it in the REPL as follows:
((\x -> \y -> show x == y) :: Int -> String -> Bool) 42 "42" ~~> True
((\x -> \y -> show x == y) :: Int -> String -> Bool) 42 "foobar" ~~> False
What happens when ((.)(.)) gets an Int -> String -> Bool?
((.)(.)) ((\x -> \y -> show x == y) :: Int -> String -> Bool) [8]
:: Int -> (a -> String) -> a -> Bool
which is a1 -> (a2 -> b) -> a2 -> c when a1 == Int, b == String, c == Bool, and
a2 is renamed (by the type-checker) to a. Score one for equational reasoning!
Ok, this bad boy, ((.)(.)), from equation 6, is waiting for a function of type
a1 -> b -> c. There is one laying around: (.) --- after some renaming:
(.) :: (b -> c) -> (a -> b) -> a -> c
`---.--' `---.--' `--.-'
a1 -> b -> c [9]
If ((.)(.)) gets a (.) from equations 6 and 9, we expect to see
a1 -> (a2 -> b ) -> a2 -> c
`---.--' `---.--' `---.--'
(b -> c) -> (a2 -> (a -> b) ) -> a2 -> (a -> c) [10]
What does GHCi say?
(b -> c) -> (a1 -> a2 -> b ) -> a1 -> a2 -> c [11]
This works when we replace or rename, in equation 11, a1 becoming a2 and a2
becoming a.
Now intuit the pattern: A composition takes two 1-functions and returns a
1-function, where a 1-function takes one argument and produces a value. The
composition of compositions, namely (.)(.)(.) or (.).(.), takes a 1-function and
a 2-function and produces a 2-function. Call that a cc. Going further, the
composition of composition and cc, namely ccc = ((.)(.)((.)(.)(.))), takes a
1-function and a 3-function, and returns a 3-function. Remove some
parentheses and nesting by noting that ccc = (.).(.).(.), remembering that prefix
notations fix to the left (have left fixity). Keep composing composition
with cc..c's, adding one more arity to the second argument and the result:
((.)(.)((.)(.)((.)(.)(.)))) is the same as (.).(.).(.).(.).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment