git.iko.soy/Idris-dev
on master help sign in
remove Interfaces.Zippable in favor of Interfaces.Correlative
42cce7cMichael Morgan
libs/contrib/Interfaces/Correlative.idrnew file+55
compare with master
unifiedsplit
@@ -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+ (</>) = (<*>)
libs/contrib/Interfaces/Zippable.idrdeleted−50
@@ -1,50 +0,0 @@
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 = liftA2
39−
40−Zippable (Either a) where
41− zipWith = liftA2
42−
43−Zippable List where
44− zipWith = Prelude.List.zipWith
45−
46−Zippable Stream where
47− zipWith = Prelude.Stream.zipWith
48−
49−Zippable (Vect n) where
50− zipWith = Data.Vect.zipWith
libs/contrib/contrib.ipkg+1−1
@@ -11,8 +11,8 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
11 Control.Pipeline,
11 Control.Pipeline,
12 Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
12 Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,
13
13
14+ Interfaces.Correlative,
14 Interfaces.Verified,
15 Interfaces.Verified,
15− Interfaces.Zippable,
16
16
17 Data.Fun, Data.Rel,
17 Data.Fun, Data.Rel,
18 Data.Hash,
18 Data.Hash,