Equational Reasoning in Haskell

Tranpose.hs

-- source of `tranpose`: `Applicative programming with effects` by McBride/Paterson 

transpose :: [[a]] -> [[a]]
transpose []         = repeat []
transpose (xs : xss) = zipWith (:) xs (transpose xss)

-- I didn't fully understand this function, so I decided to fully evaluate it by substituion.

transpose [[1,2,3], [4,5,6]] === zipWith (:) [1,2,3] (transpose [[4,5,6]])
                             === zipWith (:) [1,2,3] (zipWith (:) [4,5,6] (transpose []))
                             === zipWith (:) [1,2,3] (zipWith (:) [4,5,6] (repeat []))
                             === zipWith (:) [1,2,3] ([[4], [5], [6]])
                             === [[1,4], [2,5], [3,6]]
                                
-- Let's confirm that the `transpose` function call equals the broken out (by substitution) expression
ghci> transpose [[1,2,3],[4,5,6]]
[[1,4],[2,5],[3,6]]