@@ -0,0 +1,55 @@
1+module Interfaces.Correlative
2+
3+import Data.Vect
4+
5+%access public export
6+%default total
7+
8+infixl 2 </>
9+
10+||| A Correlative functor is a functor where, given `(xs, ys : Correlative f)`,
11+||| certain elements from xs and ys can be paired with one another due to some
12+||| intrinsic property of `f`. Elements that cannot be paired are discarded.
13+interface Functor f => Correlative (f : Type -> Type) where
14+ (</>) : f (a -> b) -> f a -> f b
15+
16+||| Combine two containers elementwise using some function.
17+zipWith : Correlative f => (a -> b -> c) -> f a -> f b -> f c
18+zipWith f xs ys = (map f xs) </> ys
19+
20+||| Combine three containers elementwise using some function.
21+zipWith3 : Correlative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
22+zipWith3 f xs ys zs = (map f xs) </> ys </> zs
23+
24+||| Combine two containers elementwise into a container of pairs.
25+zip : Correlative f => f a -> f b -> f (a, b)
26+zip = zipWith (\x, y => (x, y))
27+
28+||| Combine three containers elementwise into a container of tuples.
29+zip3 : Correlative f => f a -> f b -> f c -> f (a, b, c)
30+zip3 = zipWith3 (\x, y, z => (x, y, z))
31+
32+||| Convert a container of pairs into a pair of containers.
33+unzip : Functor t => t (a, b) -> (t a, t b)
34+unzip xs = (map fst xs, map snd xs)
35+
36+||| Convert a container of tuples into a tuple of containers.
37+unzip3 : Functor t => t (a, b, c) -> (t a, t b, t c)
38+unzip3 xs = (map fst xs, unzip (map snd xs))
39+
40+Correlative Maybe where
41+ (</>) = (<*>)
42+
43+Correlative (Either a) where
44+ (</>) = (<*>)
45+
46+Correlative List where
47+ (</>) [] _ = []
48+ (</>) _ [] = []
49+ (</>) (f :: fs) (x :: xs) = f x :: (fs </> xs)
50+
51+Correlative Stream where
52+ (</>) = (<*>)
53+
54+Correlative (Vect n) where
55+ (</>) = (<*>)