0 | module Data.Validated
  1 |
  2 | import Control.Function
  3 |
  4 | import Data.List1
  5 |
  6 | import Decidable.Equality
  7 |
  8 | %default total
  9 |
 10 | ||| `Validated` is like an `Either` but accumulates all errors with semigroup operation.
 11 | public export
 12 | data Validated e a = Valid a | Invalid e
 13 |
 14 | --- Instances of standard interfaces ---
 15 |
 16 | public export
 17 | (Eq e, Eq a) => Eq (Validated e a) where
 18 |   Valid x   == Valid y   = x == y
 19 |   Invalid e == Invalid f = e == f
 20 |   _ == _ = False
 21 |
 22 | export
 23 | (Show e, Show a) => Show (Validated e a) where
 24 |   showPrec d $ Valid   x = showCon d "Valid" $ showArg x
 25 |   showPrec d $ Invalid e = showCon d "Invalid" $ showArg e
 26 |
 27 | export
 28 | Injective Valid where
 29 |   injective Refl = Refl
 30 |
 31 | export
 32 | Injective Invalid where
 33 |   injective Refl = Refl
 34 |
 35 | public export
 36 | Functor (Validated e) where
 37 |   map f $ Valid x   = Valid $ f x
 38 |   map _ $ Invalid e = Invalid e
 39 |
 40 | public export
 41 | Bifunctor Validated where
 42 |   bimap _ s $ Valid x   = Valid   $ s x
 43 |   bimap f _ $ Invalid e = Invalid $ f e
 44 |
 45 | public export
 46 | Bifoldable Validated where
 47 |   bifoldr _ g acc (Valid a)   = g a acc
 48 |   bifoldr f _ acc (Invalid e) = f e acc
 49 |
 50 |   bifoldl _ g acc (Valid a)   = g acc a
 51 |   bifoldl f _ acc (Invalid e) = f acc e
 52 |
 53 |   binull _ = False
 54 |
 55 | public export
 56 | Bitraversable Validated where
 57 |   bitraverse _ g (Valid a)   = Valid <$> g a
 58 |   bitraverse f _ (Invalid e) = Invalid <$> f e
 59 |
 60 | ||| Applicative composition preserves invalidity sequentially accumulating all errors.
 61 | public export
 62 | Semigroup e => Applicative (Validated e) where
 63 |   pure = Valid
 64 |
 65 |   Valid f    <*> Valid x    = Valid $ f x
 66 |   Invalid e1 <*> Invalid e2 = Invalid $ e1 <+> e2
 67 |   Invalid e  <*> Valid _    = Invalid e
 68 |   Valid _    <*> Invalid e  = Invalid e
 69 |
 70 | -- There is no `Monad` implementation because it can't be coherent with the accumulating `Applicative` one.
 71 |
 72 | ||| Semigroup operation selects the leftmost valid value.
 73 | ||| If both sides are invalid, errors are accumulated.
 74 | public export
 75 | Semigroup e => Semigroup (Validated e a) where
 76 |   l@(Valid _) <+> _           = l
 77 |   _           <+> r@(Valid _) = r
 78 |   Invalid e1  <+> Invalid e2  = Invalid $ e1 <+> e2
 79 |
 80 | public export
 81 | Monoid e => Monoid (Validated e a) where
 82 |   neutral = Invalid neutral
 83 |
 84 | ||| Alternative composition preserves validity selecting the leftmost valid value.
 85 | ||| If both sides are invalid, errors are accumulated.
 86 | public export
 87 | Monoid e => Alternative (Validated e) where
 88 |   empty = neutral
 89 |   l@(Valid _) <|> _           = l
 90 |   _           <|> r@(Valid _) = r
 91 |   Invalid e1  <|> Invalid e2  = Invalid $ e1 <+> e2
 92 |
 93 | public export
 94 | Foldable (Validated e) where
 95 |   foldr op init $ Valid x   = x `op` init
 96 |   foldr _  init $ Invalid _ = init
 97 |
 98 |   foldl op init $ Valid x   = init `op` x
 99 |   foldl _  init $ Invalid _ = init
100 |
101 |   null $ Valid _   = False
102 |   null $ Invalid _ = True
103 |
104 | public export
105 | Traversable (Validated e) where
106 |   traverse f $ Valid x   = Valid <$> f x
107 |   traverse _ $ Invalid e = pure $ Invalid e
108 |
109 | public export
110 | Semigroup e => Zippable (Validated e) where
111 |   zipWith f (Valid l)   (Valid r)   = Valid $ f l r
112 |   zipWith _ (Valid _)   (Invalid r) = Invalid r
113 |   zipWith _ (Invalid l) (Valid _)   = Invalid l
114 |   zipWith _ (Invalid l) (Invalid r) = Invalid $ l <+> r
115 |
116 |   zipWith3 f (Valid x)   (Valid y)   (Valid z)   = Valid $ f x y z
117 |   zipWith3 _ (Valid _)   (Valid _)   (Invalid z) = Invalid z
118 |   zipWith3 _ (Valid _)   (Invalid y) (Valid _)   = Invalid y
119 |   zipWith3 _ (Valid _)   (Invalid y) (Invalid z) = Invalid $ y <+> z
120 |   zipWith3 _ (Invalid x) (Valid _)   (Valid _)   = Invalid x
121 |   zipWith3 _ (Invalid x) (Valid _)   (Invalid z) = Invalid $ x <+> z
122 |   zipWith3 _ (Invalid x) (Invalid y) (Valid _)   = Invalid $ x <+> y
123 |   zipWith3 _ (Invalid x) (Invalid y) (Invalid z) = Invalid $ x <+> y <+> z
124 |
125 |   unzipWith f (Valid x)   = let (a, b) = f x in (Valid a, Valid b)
126 |   unzipWith _ (Invalid e) = (Invalid e, Invalid e)
127 |
128 |   unzipWith3 f (Valid x)   = let (a, b, c) = f x in (Valid a, Valid b, Valid c)
129 |   unzipWith3 _ (Invalid e) = (Invalid e, Invalid e, Invalid e)
130 |
131 | public export
132 | Uninhabited (Valid x = Invalid e) where
133 |   uninhabited Refl impossible
134 |
135 | public export
136 | Uninhabited (Invalid e = Valid x) where
137 |   uninhabited Refl impossible
138 |
139 | public export
140 | (DecEq e, DecEq a) => DecEq (Validated e a) where
141 |   decEq (Valid x) (Valid y) = decEqCong $ decEq x y
142 |   decEq (Invalid x) (Invalid y) = decEqCong $ decEq x y
143 |   decEq (Valid x) (Invalid y) = No uninhabited
144 |   decEq (Invalid x) (Valid y) = No uninhabited
145 |
146 | --- Convenience representations ---
147 |
148 | ||| Special case of `Validated` with a `List1` as an error accumulator.
149 | public export %inline
150 | ValidatedL : Type -> Type -> Type
151 | ValidatedL = Validated . List1
152 |
153 | public export %inline
154 | oneInvalid : Applicative f => e -> Validated (f e) a
155 | oneInvalid = Invalid . pure
156 |
157 | --- Conversions to and from `Either` ---
158 |
159 | public export %inline
160 | fromEither : Either e a -> Validated e a
161 | fromEither $ Right x = Valid x
162 | fromEither $ Left  e = Invalid e
163 |
164 | public export %inline
165 | fromEitherL : Either e a -> ValidatedL e a
166 | fromEitherL $ Right x = Valid x
167 | fromEitherL $ Left  e = oneInvalid e
168 |
169 | public export %inline
170 | toEither : Validated e a -> Either e a
171 | toEither $ Valid   x = Right x
172 | toEither $ Invalid e = Left e
173 |
174 | --- Conversions to and from `Maybe` ---
175 |
176 | public export %inline
177 | fromMaybe : Monoid e => Maybe a -> Validated e a
178 | fromMaybe $ Just x  = Valid x
179 | fromMaybe $ Nothing = empty
180 |
181 | public export %inline
182 | toMaybe : Validated e a -> Maybe a
183 | toMaybe $ Valid x   = Just x
184 | toMaybe $ Invalid _ = Nothing
185 |
186 | --- Property of being valid ---
187 |
188 | public export
189 | data IsValid : Validated e a -> Type where
190 |   ItIsValid : IsValid $ Valid x
191 |
192 | export
193 | Uninhabited (IsValid $ Invalid e) where
194 |   uninhabited ItIsValid impossible
195 |
196 | public export
197 | isItValid : (v : Validated e a) -> Dec (IsValid v)
198 | isItValid $ Valid _   = Yes ItIsValid
199 | isItValid $ Invalid _ = No absurd
200 |