0 | module Monocle.Lens
  1 |
  2 | import Monocle.Fold
  3 | import Monocle.Getter
  4 | import Monocle.Optional
  5 | import Monocle.Setter
  6 | import Monocle.Traversal
  7 | import Control.Monad.State
  8 | import Data.List.Quantifiers.Extra
  9 | import Data.List1
 10 | import Data.Maybe
 11 | import Data.SortedMap
 12 | import Data.Vect
 13 |
 14 | %default total
 15 |
 16 | --------------------------------------------------------------------------------
 17 | --          Lens
 18 | --------------------------------------------------------------------------------
 19 |
 20 | ||| A Lens unifies a `Setter` and a Getter, and is therefore typically used
 21 | ||| to focus on a single value in a larger data type.
 22 | |||
 23 | ||| Lenses are best known for allowing us to extract and update record fields,
 24 | ||| but they can also be used with other types of data.
 25 | |||
 26 | ||| A Lens is parameterized over four parameters, because in general
 27 | ||| we could not only update a value but also its type with an updating
 28 | ||| function. Consider Lens `fst`, where `s` corresponds to `(a,c)` and
 29 | ||| `t` corresponds to `(b,c)`. Accordingly, if we have a function from
 30 | ||| `a` to `b`, we can convert a pair of type `(a,c)` to one of type `(b,c)`.
 31 | public export
 32 | record Lens (s,t,a,b : Type) where
 33 |   constructor L
 34 |   get_ : s -> a
 35 |   mod_ : (a -> b) -> s -> t
 36 |
 37 | ||| Convenience alias for monomorphic lenses, which do not allow
 38 | ||| us to change the value and source types.
 39 | public export
 40 | 0 Lens' : (s,a : Type) -> Type
 41 | Lens' s a = Lens s s a a
 42 |
 43 | ||| Alternative constructor for creating a Lens from a getting and
 44 | ||| a setting function.
 45 | public export
 46 | lens : (s -> a) -> (b -> s -> t) -> Lens s t a b
 47 | lens f g = L f $ \h,v => g (h $ f v) v
 48 |
 49 | --------------------------------------------------------------------------------
 50 | --          Interface
 51 | --------------------------------------------------------------------------------
 52 |
 53 | ||| Interface for converting other optics to lenses.
 54 | public export
 55 | interface ToLens (0 o : Type -> Type -> Type -> Type -> Type) where
 56 |   toLens : o s t a b -> Lens s t a b
 57 |
 58 | public export %inline
 59 | ToLens Lens where toLens = id
 60 |
 61 | --------------------------------------------------------------------------------
 62 | --          Utilities
 63 | --------------------------------------------------------------------------------
 64 |
 65 | ||| Specialized version of `set` that sometimes helps with type inference.
 66 | public export %inline
 67 | setL : Lens s t a b -> b -> s -> t
 68 | setL l = mod_ l . const
 69 |
 70 | ||| Modify the value focussed on by the given Lens with an effectful
 71 | ||| computation.
 72 | public export %inline
 73 | modF : Functor f => Lens s t a b -> (a -> f b) -> s -> f t
 74 | modF l g v = (\x => setL l x v) <$> g (get_ l v)
 75 |
 76 | ||| Sequential composition of lenses.
 77 | public export
 78 | (~>) : Lens s t x y -> Lens x y a b -> Lens s t a b
 79 | L g1 s1 ~> L g2 s2 = L (g2 . g1) (s1 . s2)
 80 |
 81 | --------------------------------------------------------------------------------
 82 | --          Conversions
 83 | --------------------------------------------------------------------------------
 84 |
 85 | public export %inline
 86 | ToGetter Lens where
 87 |   toGetter  = G . get_
 88 |
 89 | public export %inline
 90 | ToFold Lens where
 91 |   toFold = toFold . toGetter
 92 |
 93 | public export
 94 | ToOptional Lens where
 95 |   toOptional l = O (Right . l.get_) l.mod_
 96 |
 97 | public export %inline
 98 | ToSetter Lens where
 99 |   toSetter = S . mod_
100 |
101 | public export %inline
102 | ToTraversal Lens where
103 |   toTraversal l = T (modF l) (toFold l) (toSetter l)
104 |
105 | --------------------------------------------------------------------------------
106 | --          Lenses
107 | --------------------------------------------------------------------------------
108 |
109 | ||| A Lens focussing on the first element of a pair.
110 | public export %inline
111 | fst : Lens (a,c) (b,c) a b
112 | fst = L fst mapFst
113 |
114 | ||| A Lens focussing on the second element of a pair.
115 | public export
116 | snd : Lens (c,a) (c,b) a b
117 | snd = L snd mapSnd
118 |
119 | ||| A Lens focussing on the head of a non-empty vector.
120 | public export
121 | head : Lens' (Vect (S n) a) a
122 | head = lens head $ \x,v => x :: tail v
123 |
124 | ||| A Lens focussing on the tail of a non-empty vector.
125 | public export
126 | tail : Lens' (Vect (S n) a) (Vect n a)
127 | tail = lens tail $ \x,v => head v :: x
128 |
129 | ||| A Lens focussing on a specific element in a vector.
130 | public export
131 | ix : Fin n -> Lens' (Vect n a) a
132 | ix x = L (index x) (updateAt x)
133 |
134 | ||| A Lens focussing on the head of a non-empty list.
135 | public export
136 | head1 : Lens' (List1 a) a
137 | head1 = lens head $ \x,v => x ::: tail v
138 |
139 | ||| A Lens focussing on the tail of a non-empty list.
140 | public export
141 | tail1 : Lens' (List1 a) (List a)
142 | tail1 = lens tail $ \x,v => head v ::: x
143 |
144 | ||| A Lens focussing on the value associated with the given
145 | ||| key in a `SortedMap`.
146 | |||
147 | ||| Note: Unlike a related `Optional`, which we get via `at k .> just`,
148 | |||       this Lens allows us to remove a key from a dictionary by
149 | |||       setting the corresponding value to `Nothing`.
150 | public export
151 | at : Ord k => k -> Lens' (SortedMap k v) (Maybe v)
152 | at x = lens (lookup x) $ \mv,m => maybe (delete x m) (\v => insert x v m) mv
153 |
154 | ||| Like `at` but yields the given default value in case no
155 | ||| value has been associated with the given key.
156 | export
157 | atDflt : Ord k => k -> v -> Lens' (SortedMap k v) v
158 | atDflt x v = lens (fromMaybe v . lookup x) (insert x)
159 |
160 | ||| Like `atDflt` but using an auto-implicit argument for the default
161 | ||| value.
162 | export %inline
163 | atAuto : Ord k => k -> {auto prf : v} -> Lens' (SortedMap k v) v
164 | atAuto x = atDflt x prf
165 |
166 | public export
167 | allGet :
168 |      {0 ks : List k}
169 |   -> {0 f  : k -> Type}
170 |   -> {auto e : Elem t ks}
171 |   -> All f ks
172 |   -> f t
173 | allGet @{Here}    (h::_)  = h
174 | allGet @{There _} (_::vs) = allGet vs
175 |
176 | public export
177 | allUpd :
178 |      {0 ks : List k}
179 |   -> {0 f  : k -> Type}
180 |   -> {auto e : Elem t ks}
181 |   -> (f t -> f t)
182 |   -> All f ks
183 |   -> All f ks
184 | allUpd @{Here}    g (h::vs) = g h :: vs
185 | allUpd @{There _} g (h::vs) = h :: allUpd g vs
186 |
187 | ||| Lens focussing on a single element in a heterogeneous list.
188 | public export
189 | prod :
190 |      {0 ks : List k}
191 |   -> {0 f  : k -> Type}
192 |   -> (0 t : k)
193 |   -> {auto e : Elem t ks}
194 |   -> Lens' (All f ks) (f t)
195 | prod t = L allGet allUpd
196 |
197 | public export
198 | allHead : Lens' (All f (k::ks)) (f k)
199 | allHead = lens (\(v::_) => v) (\v,(_::vs) => v::vs)
200 |
201 | public export
202 | allTail : Lens' (All f (k::ks)) (All f ks)
203 | allTail = lens (\(_::vs) => vs) (\vs,(v::_) => v::vs)
204 |
205 | --------------------------------------------------------------------------------
206 | --          State
207 | --------------------------------------------------------------------------------
208 |
209 | ||| View a state through a lens
210 | export
211 | stL : Functor m => Lens' t s -> StateT s m x -> StateT t m x
212 | stL l (ST f) = ST $ \v => (\(w,r) => (setL l w v, r)) <$> f (l.get_ v)
213 |
214 | -- ||| View a stateful computation resulting in a monoid through an
215 | -- ||| optional.
216 | -- export
217 | -- stateO : Monoid x => Optional' t s -> State s x -> State t x
218 | -- stateO o (ST f) =
219 | --   ST $ \v => case first o v of
220 | --     Nothing  => Id (v, neutral)
221 | --     Just vs  => let Id (vs2,w) := f vs in Id (set o vs2 v, w)
222 | --
223 |