0 | module Monocle.Fold
  1 |
  2 | import Data.List
  3 | import Data.SnocList
  4 |
  5 | %default total
  6 |
  7 | export
  8 | infixl 0 ~>
  9 |
 10 | ||| A Fold is a composable data accessor, allowing us to extract
 11 | ||| zero or more values of type `a` from a value of type `s`.
 12 | |||
 13 | ||| Like other optics, `Folds` can be composed sequentially via operator
 14 | ||| `(~>)`.
 15 | |||
 16 | ||| This is a type constructor parameterized over four type parameters
 17 | ||| of which two (`t` and `b`) are phantom types without any runtime
 18 | ||| relevance. We need them in order to compose Folds with other
 19 | ||| optics (see module `Monocle.Compose`).
 20 | |||
 21 | ||| Folds are mainly useful because almost all other optics can be
 22 | ||| converted to Folds (with the exception of `Setter`s).
 23 | public export
 24 | record Fold (s,t,a,b : Type) where
 25 |   constructor F
 26 |   foldMap_ : {0 m : _} -> Monoid m => (a -> m) -> s -> m
 27 |
 28 | ||| We can fold over every `Foldable`.
 29 | public export %inline
 30 | fold_ : Foldable t => Fold (t a) (t a) a a
 31 | fold_ = F foldMap
 32 |
 33 | ||| The empty Fold, which always yields zero values.
 34 | public export %inline
 35 | empty : Fold s t a b
 36 | empty = F $ \_,_ => neutral
 37 |
 38 | ||| Sequential composition of Folds.
 39 | public export %inline
 40 | (~>) : Fold s t a b -> Fold a b c d -> Fold s t c d
 41 | F f ~> F g = F $ f . g
 42 |
 43 | --------------------------------------------------------------------------------
 44 | --          Interface
 45 | --------------------------------------------------------------------------------
 46 |
 47 | ||| Interface for converting other optics to Folds.
 48 | public export
 49 | interface ToFold (0 o : Type -> Type -> Type -> Type -> Type) where
 50 |   toFold : o s t a b -> Fold s t a b
 51 |
 52 | public export %inline
 53 | ToFold Fold where toFold = id
 54 |
 55 | --------------------------------------------------------------------------------
 56 | --          Monoids
 57 | --------------------------------------------------------------------------------
 58 |
 59 | public export
 60 | [SFirst] Semigroup (Maybe a) where
 61 |   Nothing <+> y = y
 62 |   x       <+> _ = x
 63 |
 64 | public export
 65 | [First] Monoid (Maybe a) using SFirst where neutral = Nothing
 66 |
 67 | public export
 68 | [SLast] Semigroup (Maybe a) where
 69 |   x <+> Nothing = x
 70 |   _ <+> y       = y
 71 |
 72 | public export
 73 | [Last] Monoid (Maybe a) using SLast where neutral = Nothing
 74 |
 75 | --------------------------------------------------------------------------------
 76 | --          Utility Functions
 77 | --------------------------------------------------------------------------------
 78 |
 79 | ||| Use a Fold to extract data from a source value and accumulate it
 80 | ||| via a `Monoid`.
 81 | public export %inline
 82 | foldMap : Monoid m => ToFold o => o s t a b -> (a -> m) -> s -> m
 83 | foldMap f = foldMap_ (toFold f)
 84 |
 85 | ||| Use a Fold to extract and accumulate data with a `Monoid` implementation
 86 | ||| from a source value.
 87 | public export %inline
 88 | fold : ToFold o => Monoid a => o s t a b -> s -> a
 89 | fold f = foldMap f id
 90 |
 91 | ||| Use a Fold to extract data from a source value and store it in a `List`.
 92 | public export %inline
 93 | asList : ToFold o => o s t a b -> s -> List a
 94 | asList f = foldMap f pure
 95 |
 96 | ||| Use a Fold to extract data from a source value and
 97 | ||| store it in a `SnocList`.
 98 | public export %inline
 99 | asSnocList : ToFold o => o s t a b -> s -> SnocList a
100 | asSnocList f = foldMap f pure
101 |
102 | ||| Use a Fold to try and extract the first piece of data from a source value.
103 | public export %inline
104 | first : ToFold o => o s t a b -> s -> Maybe a
105 | first f = foldMap @{First} f Just
106 |
107 | ||| Use a Fold to try and extract the last piece of data from a source value.
108 | public export
109 | last : ToFold o => o s t a b -> s -> Maybe a
110 | last f = foldMap @{Last} f Just
111 |
112 | ||| Use a Fold to try and extract the first piece of data
113 | ||| fulfilling a predicate from a source value.
114 | public export
115 | find : ToFold o => o s t a b -> (a -> Bool) -> s -> Maybe a
116 | find f g = foldMap @{First} f (\x => if g x then Just x else Nothing)
117 |