on master help sign in
Merge pull request #933 from JanBessai/transpose

Transpose on lists of lists

commit3bc484605f98b90a6253fbf4c4b69dbfdbd0ddf2 authorEdwin Brady <edwin.brady@gmail.com> dateTue 25 Feb 2014, 22:56 (13 years ago) parente42e698a4102e6
1 file changed+17
libs/prelude/Prelude/List.idr+17
libs/prelude/Prelude/List.idr+17
@@ -269,6 +269,23 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
269269intercalate : List a -> List (List a) -> List a
270270intercalate sep l = concat $ intersperse sep l
271271
272+-- | Transposes rows and columns of a list of lists.
273+--
274+-- > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
275+--
276+-- This also works for non square scenarios, thus
277+-- involution does not always hold:
278+--
279+-- > transpose [[], [1, 2]] = [[1], [2]]
280+-- > transpose (transpose [[], [1, 2]]) = [[1, 2]]
281+--
282+-- TODO: Solution which satisfies the totality checker?
283+%assert_total
284+transpose : List (List a) -> List (List a)
285+transpose [] = []
286+transpose ([] :: xss) = transpose xss
287+transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))
288+
272289--------------------------------------------------------------------------------
273290-- Membership tests
274291--------------------------------------------------------------------------------