@@ -0,0 +1,54 @@
1+module Interfaces.Zippable
2+
3+import Data.Vect
4+
5+%access public export
6+%default total
7+
8+||| The Zippable interface describes the operation of combining
9+||| two parameterized container elementwise using a provided function
10+||| into a new container with the function's return values.
11+interface Zippable (t : Type -> Type) where
12+ ||| Combine two containers elementwise using some function.
13+ ||| If the container type is Sized, the following should hold:
14+ ||| size (zipWith f xs ys) = minimum (size xs) (size ys)
15+ zipWith : (f : a -> b -> c) -> t a -> t b -> t c
16+
17+||| Combine two container of pairs from two containers.
18+zip : Zippable t => t a -> t b -> t (a, b)
19+zip = zipWith (\x, y => (x, y))
20+
21+||| Combine three containers by applying a function elementwise.
22+zipWith3 : Zippable t => (f : a -> b -> c -> d) -> t a -> t b -> t c -> t d
23+zipWith3 f xs ys zs = zipWith (\x, (y, z) => f x y z) xs (zip ys zs)
24+
25+||| Combine three containers into a container of tuples.
26+zip3 : Zippable t => t a -> t b -> t c -> t (a, b, c)
27+zip3 = zipWith3 (\x, y, z => (x, y, z))
28+
29+||| Convert a container of pairs until a pair of containers.
30+unzip : Functor t => t (a, b) -> (t a, t b)
31+unzip xs = (map fst xs, map snd xs)
32+
33+||| Convert a container of tuples into a tuple of containers.
34+unzip3 : Functor t => t (a, b, c) -> (t a, t b, t c)
35+unzip3 xs = (map fst xs, unzip (map snd xs))
36+
37+Zippable Maybe where
38+ zipWith f Nothing _ = Nothing
39+ zipWith f (Just x) Nothing = Nothing
40+ zipWith f (Just x) (Just y) = Just (f x y)
41+
42+Zippable (Either a) where
43+ zipWith f (Left lx) _ = Left lx
44+ zipWith f (Right x) (Left ly) = Left ly
45+ zipWith f (Right x) (Right y) = Right (f x y)
46+
47+Zippable List where
48+ zipWith = Prelude.List.zipWith
49+
50+Zippable Stream where
51+ zipWith = Prelude.Stream.zipWith
52+
53+Zippable (Vect n) where
54+ zipWith = Data.Vect.zipWith