0 | module Data.Zippable
 1 |
 2 | %default total
 3 |
 4 | ---------------------------
 5 | -- Zips and unzips --
 6 | ---------------------------
 7 |
 8 | ||| The `Zippable` interface describes how you can combine and split the
 9 | ||| elements in a parameterised type.
10 | ||| @ z the parameterised type
11 | public export
12 | interface Zippable z where
13 |   ||| Combine two parameterised types by applying a function.
14 |   ||| @ z the parameterised type
15 |   ||| @ func the function to combine elements with
16 |   zipWith : (func : a -> b -> c) -> z a -> z b -> z c
17 |
18 |   ||| Combine two parameterised types into a parameterised type of pairs.
19 |   ||| @ z the parameterised type
20 |   zip : z a -> z b -> z (a, b)
21 |   zip = zipWith (,)
22 |
23 |   export infixr 6 `zip`
24 |
25 |   ||| Combine three parameterised types by applying a function.
26 |   ||| @ z the parameterised type
27 |   ||| @ func the function to combine elements with
28 |   zipWith3 : (func : a -> b -> c -> d) -> z a -> z b -> z c -> z d
29 |   zipWith3 f = zipWith (uncurry f) .: zip
30 |
31 |   ||| Combine three parameterised types into a parameterised type of triplets.
32 |   ||| @ z the parameterised type
33 |   zip3 : z a -> z b -> z c -> z (a, b, c)
34 |   zip3 = zipWith3 (,,)
35 |
36 |   ||| Split a parameterised type by applying a function into a pair of
37 |   ||| parameterised types.
38 |   ||| @ z the parameterised type
39 |   ||| @ func the function to split elements with
40 |   unzipWith : (func : a -> (b, c)) -> z a -> (z b, z c)
41 |
42 |   ||| Split a parameterised type of pairs into a pair of parameterised types.
43 |   ||| @ z the parameterised type
44 |   unzip : z (a, b) -> (z a, z b)
45 |   unzip = unzipWith id
46 |
47 |   ||| Split a parameterised type by applying a function into a triplet of
48 |   ||| parameterised types.
49 |   ||| @ z the parameterised type
50 |   ||| @ func the function to split elements with
51 |   unzipWith3 : (func : a -> (b, c, d)) -> z a -> (z b, z c, z d)
52 |   unzipWith3 = mapSnd unzip .: unzipWith
53 |
54 |   ||| Split a parameterised type of triplets into a triplet of parameterised
55 |   ||| types.
56 |   ||| @ z the parameterised type
57 |   unzip3 : z (a, b, c) -> (z a, z b, z c)
58 |   unzip3 = unzipWith3 id
59 |
60 | public export
61 | [Compose] Zippable f => Zippable g => Zippable (f . g) where
62 |   zipWith f = zipWith $ zipWith f
63 |   zipWith3 f = zipWith3 $ zipWith3 f
64 |   unzipWith f = unzipWith $ unzipWith f
65 |   unzipWith3 f = unzipWith3 $ unzipWith3 f
66 |
67 |   zip = zipWith zip
68 |   zip3 = zipWith3 zip3
69 |   unzip = unzipWith unzip
70 |   unzip3 = unzipWith3 unzip3
71 |
72 | ||| Variant of composing and decomposing using existing `Applicative` implementation.
73 | |||
74 | ||| This implementation is lazy during unzipping.
75 | ||| Caution! It may repeat the whole original work, each time the unzipped elements are used.
76 | |||
77 | ||| Please be aware that not every `Applicative` has the same semantics as `Zippable`.
78 | ||| Consider `List` as a simple example.
79 | ||| However, this implementation is applicable for lazy data types or deferred computations.
80 | public export
81 | [FromApplicative] Applicative f => Zippable f where
82 |   zipWith f x y = [| f x y |]
83 |   zipWith3 f x y z = [| f x y z |]
84 |
85 |   unzip u = (map fst u, map snd u)
86 |   unzip3 u = (map fst u, map (fst . snd) u, map (snd . snd) u)
87 |   unzipWith f = unzip . map f
88 |   unzipWith3 f = unzip3 . map f
89 |
90 |  -- To be moved appropriately as soon as we have some module like `Data.Pair`, like other prelude types have.
91 | public export
92 | Semigroup a => Zippable (Pair a) where
93 |   zipWith f (l, x) (r, y) = (l <+> r, f x y)
94 |   zipWith3 f (l, x) (m, y) (r, z) = (l <+> m <+> r, f x y z)
95 |
96 |   unzipWith f (l, x) = bimap (l,) (l,) (f x)
97 |   unzipWith3 f (l, x) = bimap (l,) (bimap (l,) (l,)) (f x)
98 |