
  0 | ||| A withering is something which can be run on any IndWitherable.
  1 | |||
  2 | ||| Since IndWitherable has a large family of superclasses, there are
  3 | ||| many such things.
  4 | |||
  5 | ||| The interest in these things is that they are the sorts of things
  6 | ||| one wants to do in merging operations.
  7 | module Data.Withering
  8 | 
  9 | import Data.Indexed.Fixed
 10 | import Data.Witherable.Indexed
 11 | 
 12 | 
 13 | public export
 14 | data Withering : (Type -> Type) -> Type -> Type -> Type -> Type where
 15 |   MkWithering : Applicative f
 16 |              => ({0 t : Type -> Type} -> (IndWitherable i t) => t a -> f (t b))
 17 |              -> Withering f i a b
 18 | 
 19 | export
 20 | runWither : (IndWitherable i t) => Withering f i a b -> t a -> f (t b)
 21 | runWither (MkWithering w) m = w m
 22 | 
 23 | export
 24 | witherOne : Withering f i a b -> i -> a -> f (Maybe b)
 25 | witherOne (MkWithering w) x y = let
 26 |   z : FixIndex x Maybe a
 27 |   z = WithIndex (Just y)
 28 |   in unIndex <$> w z
 29 | 
 30 | 
 31 | 
 32 | export
 33 | preserving : Applicative f => Withering f i a a
 34 | preserving = MkWithering (pure . id)
 35 | 
 36 | export
 37 | flushing : Applicative f => Withering f i a b
 38 | flushing = MkWithering (pure . flush)
 39 | 
 40 | export
 41 | mapping : Applicative f => (a -> b) -> Withering f i a b
 42 | mapping f = MkWithering (pure . map f)
 43 | 
 44 | export
 45 | imapping : Applicative f => (i -> a -> b) -> Withering f i a b
 46 | imapping f = MkWithering (pure . imap f)
 47 | 
 48 | export
 49 | mapMaybeing : Applicative f => (a -> Maybe b) -> Withering f i a b
 50 | mapMaybeing f = MkWithering (pure . mapMaybe f)
 51 | 
 52 | export
 53 | imapMaybeing : Applicative f => (i -> a -> Maybe b) -> Withering f i a b
 54 | imapMaybeing f = MkWithering (pure . imapMaybe f)
 55 | 
 56 | export
 57 | traversing : Applicative f => (a -> f b) -> Withering f i a b
 58 | traversing f = MkWithering (traverse f)
 59 | 
 60 | export
 61 | itraversing : Applicative f => (i -> a -> f b) -> Withering f i a b
 62 | itraversing f = MkWithering (itraverse f)
 63 | 
 64 | export
 65 | withering : Applicative f => (a -> f (Maybe b)) -> Withering f i a b
 66 | withering f = MkWithering (wither f)
 67 | 
 68 | export
 69 | iwithering : Applicative f => (i -> a -> f (Maybe b)) -> Withering f i a b
 70 | iwithering f = MkWithering (iwither f)
 71 |