Skip to content

Instantly share code, notes, and snippets.

# rebcabin/CompositionsOfCompositions.txt Last active May 8, 2019

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  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  ( (.) ((\x -> show x) :: Int -> String) ) :: (a -> Int) -> a -> String  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  `--.---' `-------.--------' ~~~ :: 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  does GHCi agree? ((.)(.)) :: (a1 -> b -> c) -> a1 -> (a2 -> b) -> a2 -> c  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  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)  :: 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  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)  What does GHCi say? (b -> c) -> (a1 -> a2 -> b ) -> a1 -> a2 -> c  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 (.).(.).(.).(.).
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.