0 | module Data.Either
  1 |
  2 | import public Control.Function
  3 | import Data.List1
  4 |
  5 | %default total
  6 |
  7 | --------------------------------------------------------------------------------
  8 | -- Checking for a specific constructor
  9 |
 10 | ||| Extract the Left value, if possible
 11 | public export
 12 | getLeft : Either a b -> Maybe a
 13 | getLeft (Left a) = Just a
 14 | getLeft _ = Nothing
 15 |
 16 | ||| Extract the Right value, if possible
 17 | public export
 18 | getRight : Either a b -> Maybe b
 19 | getRight (Right b) = Just b
 20 | getRight _ = Nothing
 21 |
 22 | ||| True if the argument is Left, False otherwise
 23 | public export
 24 | isLeft : Either a b -> Bool
 25 | isLeft (Left _)  = True
 26 | isLeft (Right _) = False
 27 |
 28 | ||| True if the argument is Right, False otherwise
 29 | public export
 30 | isRight : Either a b -> Bool
 31 | isRight (Left _)  = False
 32 | isRight (Right _) = True
 33 |
 34 | ||| Proof that an `Either` is actually a Right value
 35 | public export
 36 | data IsRight : Either a b -> Type where
 37 |   ItIsRight : IsRight (Right x)
 38 |
 39 | export
 40 | Uninhabited (IsRight (Left x)) where
 41 |   uninhabited ItIsRight impossible
 42 |
 43 | ||| Returns the `r` value of an `Either l r` which is proved `Right`.
 44 | public export
 45 | fromRight : (e : Either l r) -> {auto 0 isRight : IsRight e} -> r
 46 | fromRight (Right r) = r
 47 | fromRight (Left _) impossible
 48 |
 49 | ||| Proof that an `Either` is actually a Left value
 50 | public export
 51 | data IsLeft : Either a b -> Type where
 52 |   ItIsLeft : IsLeft (Left x)
 53 |
 54 | export
 55 | Uninhabited (IsLeft (Right x)) where
 56 |   uninhabited ItIsLeft impossible
 57 |
 58 | ||| Returns the `l` value of an `Either l r` which is proved `Left`.
 59 | public export
 60 | fromLeft : (e : Either l r) -> {auto 0 isLeft : IsLeft e} -> l
 61 | fromLeft (Right _) impossible
 62 | fromLeft (Left l) = l
 63 |
 64 | --------------------------------------------------------------------------------
 65 | -- Grouping values
 66 |
 67 | ||| Compress the list of Lefts and Rights by accumulating
 68 | ||| all of the lefts and rights into non-empty blocks.
 69 | export
 70 | compress : List (Either a b) -> List (Either (List1 a) (List1 b))
 71 | compress [] = []
 72 | compress (Left x :: abs) = compressLefts (singleton x) abs where
 73 |   compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
 74 |   compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
 75 |   compressLefts acc abs = Left (reverse acc) :: compress abs
 76 | compress (Right y :: abs) = compressRights (singleton y) abs where
 77 |   compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
 78 |   compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
 79 |   compressRights acc abs = Right (reverse acc) :: compress abs
 80 |
 81 | ||| Decompress a compressed list. This is the left inverse of `compress` but not its
 82 | ||| right inverse because nothing forces the input to be maximally compressed!
 83 | export
 84 | decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
 85 | decompress = concatMap $ \case
 86 |   Left  as => map Left  $ forget as
 87 |   Right bs => map Right $ forget bs
 88 |
 89 | ||| Keep the payloads of all Left constructors in a list of Eithers
 90 | public export
 91 | lefts : List (Either a b) -> List a
 92 | lefts []              = []
 93 | lefts (Left  l :: xs) = l :: lefts xs
 94 | lefts (Right _ :: xs) = lefts xs
 95 |
 96 | ||| Keep the payloads of all Right constructors in a list of Eithers
 97 | public export
 98 | rights : List (Either a b) -> List b
 99 | rights []              = []
100 | rights (Left  _ :: xs) = rights xs
101 | rights (Right r :: xs) = r :: rights xs
102 |
103 | ||| Split a list of Eithers into a list of the left elements and a list of the right elements
104 | public export
105 | partitionEithers : List (Either a b) -> (List a, List b)
106 | partitionEithers l = (lefts l, rights l)
107 |
108 | ||| Remove a "useless" Either by collapsing the case distinction
109 | public export
110 | fromEither : Either a a -> a
111 | fromEither (Left l)  = l
112 | fromEither (Right r) = r
113 |
114 | ||| Right becomes left and left becomes right
115 | public export
116 | mirror : Either a b -> Either b a
117 | mirror (Left  x) = Right x
118 | mirror (Right x) = Left x
119 |
120 | public export
121 | Zippable (Either a) where
122 |   zipWith f x y = [| f x y |]
123 |   zipWith3 f x y z = [| f x y z |]
124 |
125 |   unzipWith f (Left e) = (Left e, Left e)
126 |   unzipWith f (Right xy) = let (x, y) = f xy in (Right x, Right y)
127 |
128 |   unzipWith3 f (Left e) = (Left e, Left e, Left e)
129 |   unzipWith3 f (Right xyz) = let (x, y, z) = f xyz in (Right x, Right y, Right z)
130 |
131 | --------------------------------------------------------------------------------
132 | -- Bifunctor
133 |
134 | export
135 | pushInto : c -> Either a b -> Either (c, a) (c, b)
136 | pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
137 |   -- ^ not using sections to keep it backwards compatible
138 |
139 | --------------------------------------------------------------------------------
140 | -- Conversions
141 | --------------------------------------------------------------------------------
142 |
143 | ||| Convert a Maybe to an Either by using a default value in case of Nothing
144 | ||| @ e the default value
145 | public export
146 | maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
147 | maybeToEither def (Just j) = Right j
148 | maybeToEither def Nothing  = Left  def
149 |
150 | ||| Convert an Either to a Maybe from Right injection
151 | public export
152 | eitherToMaybe : Either e a -> Maybe a
153 | eitherToMaybe (Left _) = Nothing
154 | eitherToMaybe (Right x) = Just x
155 |
156 | export
157 | eitherMapFusion : (f : _) -> (g : _) -> (p : _) -> (e : Either a b) -> either f g (map p e) = either f (g . p) e
158 | eitherMapFusion f g p $ Left x  = Refl
159 | eitherMapFusion f g p $ Right x = Refl
160 |
161 | export
162 | eitherBimapFusion : (f : _) -> (g : _) -> (p : _) -> (q : _) -> (e : _) -> either f g (bimap p q e) = either (f . p) (g . q) e
163 | eitherBimapFusion f g p q $ Left z  = Refl
164 | eitherBimapFusion f g p q $ Right z = Refl
165 |
166 | -- Injectivity of constructors
167 |
168 | ||| Left is injective
169 | export
170 | Injective Left where
171 |   injective Refl = Refl
172 |
173 | ||| Right is injective
174 | export
175 | Injective Right where
176 |   injective Refl = Refl
177 |