0 | module Data.These
  1 |
  2 | import Control.Function
  3 |
  4 | import Data.Zippable
  5 |
  6 | %default total
  7 |
  8 | public export
  9 | data These a b = This a | That b | Both a b
 10 |
 11 | public export
 12 | fromEither : Either a b -> These a b
 13 | fromEither = either This That
 14 |
 15 | public export
 16 | fromThis : These a b -> Maybe a
 17 | fromThis (This a) = Just a
 18 | fromThis (That _) = Nothing
 19 | fromThis (Both a _) = Just a
 20 |
 21 | public export
 22 | fromThat : These a b -> Maybe b
 23 | fromThat (This _) = Nothing
 24 | fromThat (That b) = Just b
 25 | fromThat (Both _ b) = Just b
 26 |
 27 | public export
 28 | fromBoth : (defaultL : Lazy a) -> (defaultR : Lazy b) -> These a b -> (a, b)
 29 | fromBoth _ y (This x)   = (x, y)
 30 | fromBoth x _ (That y)   = (x, y)
 31 | fromBoth _ _ (Both x y) = (x, y)
 32 |
 33 | public export
 34 | these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
 35 | these l r lr (This a)   = l a
 36 | these l r lr (That b)   = r b
 37 | these l r lr (Both a b) = lr a b
 38 |
 39 | public export
 40 | these' : (defualtL : Lazy a) -> (defaultR : Lazy b) -> (a -> b -> c) -> These a b -> c
 41 | these' _ y f (This x)   = f x y
 42 | these' x _ f (That y)   = f x y
 43 | these' _ _ f (Both x y) = f x y
 44 |
 45 | public export
 46 | swap : These a b -> These b a
 47 | swap (This a)   = That a
 48 | swap (That b)   = This b
 49 | swap (Both a b) = Both b a
 50 |
 51 | export
 52 | Injective This where
 53 |   injective Refl = Refl
 54 |
 55 | export
 56 | Injective That where
 57 |   injective Refl = Refl
 58 |
 59 | export
 60 | {x : _} -> Injective (Both x) where
 61 |   injective Refl = Refl
 62 |
 63 | export
 64 | {y : _} -> Injective (`Both` y) where
 65 |   injective Refl = Refl
 66 |
 67 | export
 68 | Biinjective Both where
 69 |   biinjective Refl = (Refl, Refl)
 70 |
 71 | public export
 72 | (Show a, Show b) => Show (These a b) where
 73 |   showPrec d (This x)   = showCon d "This" $ showArg x
 74 |   showPrec d (That x)   = showCon d "That" $ showArg x
 75 |   showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y
 76 |
 77 | public export
 78 | Eq a => Eq b => Eq (These a b) where
 79 |   This x   == This x'    = x == x'
 80 |   That x   == That x'    = x == x'
 81 |   Both x y == Both x' y' = x == x' && y == y'
 82 |   _ == _ = False
 83 |
 84 | public export
 85 | Semigroup a => Semigroup b => Semigroup (These a b) where
 86 |   This x <+> This x'   = This $ x <+> x'
 87 |   This x <+> That y    = Both x y
 88 |   This x <+> Both x' y = Both (x <+> x') y
 89 |
 90 |   That y <+> This x    = Both x y
 91 |   That y <+> That y'   = That $ y <+> y'
 92 |   That y <+> Both x y' = Both x $ y <+> y'
 93 |
 94 |   Both x y <+> This x'    = Both (x <+> x') y
 95 |   Both x y <+> That y'    = Both x (y <+> y')
 96 |   Both x y <+> Both x' y' = Both (x <+> x') (y <+> y')
 97 |
 98 | %inline
 99 | public export
100 | Bifunctor These where
101 |   bimap f g (This a)   = This (f a)
102 |   bimap f g (That b)   = That (g b)
103 |   bimap f g (Both a b) = Both (f a) (g b)
104 |
105 | %inline
106 | public export
107 | Bifoldable These where
108 |   bifoldr f _ acc (This a)   = f a acc
109 |   bifoldr _ g acc (That b)   = g b acc
110 |   bifoldr f g acc (Both a b) = f a (g b acc)
111 |
112 |   bifoldl f _ acc (This a)   = f acc a
113 |   bifoldl _ g acc (That b)   = g acc b
114 |   bifoldl f g acc (Both a b) = g (f acc a) b
115 |
116 |   binull _ = False
117 |
118 | %inline
119 | public export
120 | Bitraversable These where
121 |   bitraverse f _ (This a)   = This <$> f a
122 |   bitraverse _ g (That b)   = That <$> g b
123 |   bitraverse f g (Both a b) = [| Both (f a) (g b) |]
124 |
125 | %inline
126 | public export
127 | Functor (These a) where
128 |   map = mapSnd
129 |
130 | public export
131 | bifold : Semigroup m => These m m -> m
132 | bifold (This a)   = a
133 | bifold (That b)   = b
134 | bifold (Both a b) = a <+> b
135 |
136 | ||| A right-biased applicative implementation that combines lefts with a semigroup operation
137 | |||
138 | ||| This implementation does its best to not to lose any data from the original arguments.
139 | public export
140 | Semigroup a => Applicative (These a) where
141 |   pure = That
142 |
143 |   This e <*> That _    = This e
144 |   This e <*> This e'   = This $ e <+> e'
145 |   This e <*> Both e' _ = This $ e <+> e'
146 |
147 |   That f <*> That x   = That $ f x
148 |   That f <*> This e   = This e
149 |   That f <*> Both e x = Both e $ f x
150 |
151 |   Both e _ <*> This e'   = This $ e <+> e'
152 |   Both e f <*> That x    = Both e $ f x
153 |   Both e f <*> Both e' x = Both (e <+> e') $ f x
154 |
155 | public export
156 | Foldable (These a) where
157 |   foldr _  init $ This _   = init
158 |   foldr op init $ That x   = x `op` init
159 |   foldr op init $ Both _ x = x `op` init
160 |
161 |   foldl _  init $ This _   = init
162 |   foldl op init $ That x   = init `op` x
163 |   foldl op init $ Both _ x = init `op` x
164 |
165 |   null $ This _   = True
166 |   null $ That _   = False
167 |   null $ Both _ _ = False
168 |
169 | public export
170 | Traversable (These a) where
171 |   traverse _ $ This e   = pure $ This e
172 |   traverse f $ That x   = That <$> f x
173 |   traverse f $ Both x y = Both x <$> f y
174 |
175 | public export
176 | Semigroup a => Zippable (These a) where
177 |   zipWith f  x y = [| f x y |]
178 |   zipWith3 f x y z = [| f x y z |]
179 |
180 |   unzipWith f (This x)   = (This x, This x)
181 |   unzipWith f (That x)   = let (u, v) = f x in (That u, That v)
182 |   unzipWith f (Both x y) = let (u, v) = f y in (Both x u, Both x v)
183 |
184 |   unzipWith3 f (This x)   = (This x, This x, This x)
185 |   unzipWith3 f (That x)   = let (u, v, w) = f x in (That u, That v, That w)
186 |   unzipWith3 f (Both x y) = let (u, v, w) = f y in (Both x u, Both x v, Both x w)
187 |