on master help sign in
Transpose on lists of lists
commita4102e6987c14af0318886ff990fbde6a39ff452 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateTue 25 Feb 2014, 23:12 (13 years ago) parent2f9c617
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--------------------------------------------------------------------------------