0 | ||| Additional utility functions for the `Bifoldable` interface.
  1 | module Data.Bifoldable
  2 |
  3 | %default total
  4 |
  5 | ||| Left associative monadic bifold over a structure.
  6 | public export
  7 | bifoldlM : Monad m => Bifoldable p =>
  8 |           (f: a -> b -> m a) ->
  9 |           (g: a -> c -> m a) ->
 10 |           (init: a) ->
 11 |           (input: p b c) -> m a
 12 | bifoldlM f g a0 = bifoldl (\ma,b => ma >>= flip f b)
 13 |                           (\ma,c => ma >>= flip g c)
 14 |                           (pure a0)
 15 |
 16 | ||| Combines the elements of a structure using a monoid.
 17 | public export
 18 | biconcat : Monoid m => Bifoldable p => p m m -> m
 19 | biconcat = bifoldr (<+>) (<+>) neutral
 20 |
 21 | ||| Combines the elements of a structure,
 22 | ||| given ways of mapping them to a common monoid.
 23 | public export
 24 | biconcatMap : Monoid m => Bifoldable p => (a -> m) -> (b -> m) -> p a b -> m
 25 | biconcatMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral
 26 |
 27 | ||| The conjunction of all elements of a structure containing lazy boolean
 28 | ||| values.  `biand` short-circuits from left to right, evaluating until either an
 29 | ||| element is `False` or no elements remain.
 30 | public export
 31 | biand : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
 32 | biand = bifoldl (&&) (&&) True
 33 |
 34 | ||| The disjunction of all elements of a structure containing lazy boolean
 35 | ||| values.  `bior` short-circuits from left to right, evaluating either until an
 36 | ||| element is `True` or no elements remain.
 37 | public export
 38 | bior : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
 39 | bior = bifoldl (||) (||) False
 40 |
 41 | ||| The disjunction of the collective results of applying a predicate to all
 42 | ||| elements of a structure. `biany` short-circuits from left to right.
 43 | public export
 44 | biany : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
 45 | biany f g = bifoldl (\x,y => x || f y) (\x,y => x || g y) False
 46 |
 47 | ||| The disjunction of the collective results of applying a predicate to all
 48 | ||| elements of a structure.  `biall` short-circuits from left to right.
 49 | public export
 50 | biall : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
 51 | biall f g = bifoldl (\x,y => x && f y) (\x,y => x && g y) True
 52 |
 53 | ||| Add together all the elements of a structure.
 54 | public export
 55 | bisum : Num a => Bifoldable p => p a a -> a
 56 | bisum = bifoldr (+) (+) 0
 57 |
 58 | ||| Add together all the elements of a structure.
 59 | ||| Same as `bisum` but tail recursive.
 60 | export
 61 | bisum' : Num a => Bifoldable p => p a a -> a
 62 | bisum' = bifoldl (+) (+) 0
 63 |
 64 | ||| Multiply together all elements of a structure.
 65 | public export
 66 | biproduct : Num a => Bifoldable p => p a a -> a
 67 | biproduct = bifoldr (*) (*) 1
 68 |
 69 | ||| Multiply together all elements of a structure.
 70 | ||| Same as `product` but tail recursive.
 71 | export
 72 | biproduct' : Num a => Bifoldable p => p a a -> a
 73 | biproduct' = bifoldl (*) (*) 1
 74 |
 75 | ||| Map each element of a structure to a computation, evaluate those
 76 | ||| computations and discard the results.
 77 | public export
 78 | bitraverse_ :  (Bifoldable p, Applicative f)
 79 |             => (a -> f x)
 80 |             -> (b -> f y)
 81 |             -> p a b
 82 |             -> f ()
 83 | bitraverse_ f g = bifoldr ((*>) . f) ((*>) . g) (pure ())
 84 |
 85 | ||| Evaluate each computation in a structure and discard the results.
 86 | public export
 87 | bisequence_ : Applicative f => Bifoldable p => p (f a) (f b) -> f ()
 88 | bisequence_ = bifoldr (*>) (*>) (pure ())
 89 |
 90 | ||| Like `bitraverse_` but with the arguments flipped.
 91 | public export
 92 | bifor_ :  (Bifoldable p, Applicative f)
 93 |        => p a b
 94 |        -> (a -> f x)
 95 |        -> (b -> f y)
 96 |        -> f ()
 97 | bifor_ p f g = bitraverse_ f g p
 98 |
 99 | ||| Bifold using Alternative.
100 | |||
101 | ||| If you have a left-biased alternative operator `<|>`, then `choice` performs
102 | ||| left-biased choice from a list of alternatives, which means that it
103 | ||| evaluates to the left-most non-`empty` alternative.
104 | public export
105 | bichoice : Alternative f => Bifoldable p => p (Lazy (f a)) (Lazy (f a)) -> f a
106 | bichoice t = bifoldr {a = Lazy (f a)} {b = Lazy (f a)} {acc = Lazy (f a)}
107 |                  (\ x, xs => x <|> xs)
108 |                  (\ x, xs => x <|> xs)
109 |                  empty
110 |                  t
111 |
112 | ||| A fused version of `bichoice` and `bimap`.
113 | public export
114 | bichoiceMap : (Bifoldable p, Alternative f)
115 |             => (a -> f x)
116 |             -> (b -> f x)
117 |             -> p a b ->
118 |             f x
119 | bichoiceMap fa fb t = bifoldr {a} {b} {acc = Lazy (f x)}
120 |                         (\e, fx => fa e <|> fx)
121 |                         (\e, fx => fb e <|> fx)
122 |                         empty
123 |                         t
124 |