0 | module Monocle.Optional
  1 |
  2 | import Control.Monad.State
  3 | import Data.List
  4 | import Monocle.Fold
  5 | import Monocle.Setter
  6 | import Monocle.Traversal
  7 |
  8 | %default total
  9 |
 10 | ||| An Optional allows us to focus on a single piece of
 11 | ||| information in a larger data object that might or might not
 12 | ||| be there.
 13 | |||
 14 | ||| An Optional is related to but less powerful than a Prism, because
 15 | ||| it does not allow us to directly inject a value into a larger data
 16 | ||| object, but only supports updating such a value if it exists.
 17 | |||
 18 | ||| Optionals play an important role when we sequentially combine different
 19 | ||| types of optics: The sequential composition of a Lens with a Prism or
 20 | ||| vice verca results in an optional: We can no longer be certain that
 21 | ||| the value we focus on is still there (the Prism prevents that), nor can
 22 | ||| we directly inject the value into the larger data object
 23 | ||| (the Lens prevents that).
 24 | public export
 25 | record Optional s t a b where
 26 |   constructor O
 27 |   getOrModify : s -> Either t a
 28 |   replace     : (a -> b) -> s -> t
 29 |
 30 | ||| Convenience alias for monomorphic Optionals, which do not allow
 31 | ||| us to change the value and source types.
 32 | public export
 33 | 0 Optional' : (s,a : Type) -> Type
 34 | Optional' s a = Optional s s a a
 35 |
 36 | ||| Utility constructor for monomorphic optionals.
 37 | public export
 38 | optional : (s -> Maybe a) -> ((a -> a) -> s -> s) -> Optional' s a
 39 | optional f g = O (\v => maybe (Left v) Right (f v)) g
 40 |
 41 | ||| Adjust the focus sof an Optional with an effectful computation.
 42 | public export
 43 | mapA : Applicative f => Optional s t a b -> (a -> f b) -> s -> f t
 44 | mapA (O g r) f v =
 45 |   case g v of
 46 |     Left x  => pure x
 47 |     Right x => map (\vb => r (const vb) v) (f x)
 48 |
 49 | --------------------------------------------------------------------------------
 50 | --          Interface
 51 | --------------------------------------------------------------------------------
 52 |
 53 | ||| Interface for converting other optics to Optionals.
 54 | public export
 55 | interface ToOptional (0 o : Type -> Type -> Type -> Type -> Type) where
 56 |   toOptional : o s t a b -> Optional s t a b
 57 |
 58 | public export %inline
 59 | ToOptional Optional where toOptional = id
 60 |
 61 | --------------------------------------------------------------------------------
 62 | --          Conversions
 63 | --------------------------------------------------------------------------------
 64 |
 65 | public export %inline
 66 | ToSetter Optional where
 67 |   toSetter (O g r) = S r
 68 |
 69 | public export
 70 | ToFold Optional where
 71 |   toFold (O g r) = F $ \f => either (const neutral) f . g
 72 |
 73 | public export
 74 | ToTraversal Optional where
 75 |   toTraversal o = T (mapA o) (toFold o) (toSetter o)
 76 |
 77 | --------------------------------------------------------------------------------
 78 | --          Utilities
 79 | --------------------------------------------------------------------------------
 80 |
 81 | ||| Sequential composition of Optionals.
 82 | public export
 83 | (~>) : Optional s t a b -> Optional a b c d -> Optional s t c d
 84 | O g1 r1 ~> O g2 r2 =
 85 |   O (\v => g1 v >>= mapFst (\vb => r1 (const vb) v) . g2)
 86 |     (r1 . r2)
 87 |
 88 | --------------------------------------------------------------------------------
 89 | --          Predefined Optionals
 90 | --------------------------------------------------------------------------------
 91 |
 92 | ||| The empty Optional, which does not focus on anything at all.
 93 | public export
 94 | emptyO : Optional' s a
 95 | emptyO = O Left (const id)
 96 |
 97 | ||| Tries to extract a value at the given index from a List.
 98 | public export
 99 | getIx : Nat -> List a -> Maybe a
100 | getIx 0     (h::_) = Just h
101 | getIx (S k) (_::t) = getIx k t
102 | getIx _     Nil    = Nothing
103 |
104 | ||| Modifies the value at the given index in a List.
105 | |||
106 | ||| Returns the unchanged List if the index is out of bounds.
107 | public export
108 | modIx : Nat -> (a -> a) -> List a -> List a
109 | modIx 0     f (h::xs) = f h :: xs
110 | modIx (S k) f (h::xs) = h :: modIx k f xs
111 | modIx _     _ []      = []
112 |
113 | ||| An Optional focussing on the n-th element in a List.
114 | public export
115 | ix : Nat -> Optional' (List a) a
116 | ix n = optional (getIx n) (modIx n)
117 |
118 | ||| An Optional for focussing on those values that fulfill a given
119 | ||| predicate.
120 | public export
121 | select : (a -> Bool) -> Optional' a a
122 | select p =
123 |   optional
124 |     (\v => if p v then Just v else Nothing)
125 |     (\f,o => if p o then f o else o)
126 |
127 | ||| An Optional for focussing on those values that are equivalent to `v`
128 | ||| according to the given comparison function.
129 | public export %inline
130 | eqBy : Eq b => (v : b) -> (a -> b) -> Optional' a a
131 | eqBy v f = select ((v ==) . f)
132 |
133 | public export
134 | modWhere : SnocList a -> (a -> Bool) -> (a -> a) -> List a -> List a
135 | modWhere sa f g []        = sa <>> []
136 | modWhere sa f g (x :: xs) =
137 |   if f x then sa <>> (g x :: xs) else modWhere (sa :< x) f g xs
138 |
139 | ||| An Optional for focussing on the first value in a list
140 | ||| that fulfills the given predicate.
141 | public export %inline
142 | first : (a -> Bool) -> Optional' (List a) a
143 | first f = optional (find f) (modWhere [<] f)
144 |
145 | ||| An Optional for focussing on the first value in a List
146 | ||| that is equivalent to `v` according to the given comparison function.
147 | public export %inline
148 | eqFirst : Eq b => b -> (a -> b) -> Optional' (List a) a
149 | eqFirst v f = first ((v ==) . f)
150 |
151 | --------------------------------------------------------------------------------
152 | --          State
153 | --------------------------------------------------------------------------------
154 |
155 | ||| View a stateful computation resulting in a monoid through an
156 | ||| optional.
157 | export
158 | stO : Applicative m => Monoid x => Optional' t s -> StateT s m x -> StateT t m x
159 | stO o (ST f) =
160 |   ST $ \v => case first o v of
161 |     Nothing  => pure (v, neutral)
162 |     Just vs  => (\(vs2,w) => (set o vs2 v, w)) <$> f vs
163 |