0 | module Monocle.Prism
  1 |
  2 | import Monocle.Fold
  3 | import Monocle.Optional
  4 | import Monocle.Setter
  5 | import Monocle.Traversal
  6 | import Data.List.Quantifiers.Extra
  7 | import Data.List1
  8 | import Data.Maybe
  9 |
 10 | %default total
 11 |
 12 | ||| A Prism is the categorical dual of a Lens: While a Lens allows
 13 | ||| us to extract values from a larger type, a Prism allows us to inject
 14 | ||| values into a larger type, while extracting such a value might not
 15 | ||| be possible.
 16 | |||
 17 | ||| Prisms are therefore a natural fit for inspecting sum types,
 18 | ||| (as opposed to lenses, which are preferrably used for product types),
 19 | ||| where we typically have one Prism per data constructor.
 20 | |||
 21 | ||| An other use case where Prisms shine are refinement type, where
 22 | ||| "injecting" a value means extracting a value of the parent type from
 23 | ||| refinement type. An example for this is the `nat` Prism, which allows
 24 | ||| us to convert ("inject") a `Nat` into an `Integer`, while extracting a
 25 | ||| `Nat` from an `Integer` might fail.
 26 | |||
 27 | ||| A Prism is parameterized over four parameters, because in general
 28 | ||| we can not only try and extract a value from some object
 29 | ||| but also refine the object in case extraction fails.
 30 | ||| Consider lens `fst`, where `s` corresponds to `(a,c)` and
 31 | ||| `t` corresponds to `(b,c)`. Accordingly, if we have a function from
 32 | ||| `a` to `b`, we can convert a pair of type `(a,c)` to one of type `(b,c)`.
 33 | public export
 34 | record Prism s t a b where
 35 |   constructor P
 36 |   getOrModify : s -> Either t a
 37 |   reverseGet  : b -> t
 38 |
 39 | ||| Convenience alias for monomorphic Prisms, which do not allow
 40 | ||| us to change the value and source types.
 41 | public export
 42 | 0 Prism' : (s,a : Type) -> Type
 43 | Prism' s a = Prism s s a a
 44 |
 45 | ||| Convenience constructor for monomorphic Prisms.
 46 | public export
 47 | prism : (a -> Maybe b) -> (b -> a) -> Prism' a b
 48 | prism f = P (\v => maybe (Left v) Right (f v))
 49 |
 50 | ||| Adjust the focus of a Prism with an effectful computation.
 51 | public export
 52 | mapA : Applicative f => Prism s t a b -> (a -> f b) -> s -> f t
 53 | mapA (P g r) f v = either pure (map r . f) (g v)
 54 |
 55 | --------------------------------------------------------------------------------
 56 | --          Interface
 57 | --------------------------------------------------------------------------------
 58 |
 59 | ||| Interface for converting other optics to Prisms.
 60 | public export
 61 | interface ToPrism (0 o : Type -> Type -> Type -> Type -> Type) where
 62 |   toPrism : o s t a b -> Prism s t a b
 63 |
 64 | public export %inline
 65 | ToPrism Prism where toPrism = id
 66 |
 67 | --------------------------------------------------------------------------------
 68 | --          Conversions
 69 | --------------------------------------------------------------------------------
 70 |
 71 | public export
 72 | ToOptional Prism where
 73 |   toOptional (P g r) = O g (\f => either id (r . f) . g)
 74 |
 75 | public export
 76 | ToSetter Prism where
 77 |   toSetter (P g r) = S $ \f,vs => either id (r . f) (g vs)
 78 |
 79 | public export
 80 | ToFold Prism where
 81 |   toFold (P g r) = F $ \f => either (const neutral) f . g
 82 |
 83 | public export
 84 | ToTraversal Prism where
 85 |   toTraversal o = T (mapA o) (toFold o) (toSetter o)
 86 |
 87 | --------------------------------------------------------------------------------
 88 | --          Utilities
 89 | --------------------------------------------------------------------------------
 90 |
 91 | ||| Sequential composition of Prisms.
 92 | public export
 93 | (~>) : Prism s t a b -> Prism a b c d -> Prism s t c d
 94 | P g1 r1 ~> P g2 r2 =
 95 |   P (\v => g1 v >>= mapFst r1 . g2)
 96 |     (r1 . r2)
 97 |
 98 | --------------------------------------------------------------------------------
 99 | --          Predefined Prisms
100 | --------------------------------------------------------------------------------
101 |
102 | ||| A Prism focussing on the `Left` data constructor of `Either a b`.
103 | public export
104 | left' : Prism (Either a b) (Either c b) a c
105 | left' = P (either Right (Left . Right)) Left
106 |
107 | ||| Monomorphic version of `left'`.
108 | |||
109 | ||| This can improve type inference for those cases where the versatility
110 | ||| of `left'` is not needed.
111 | public export %inline
112 | left : Prism' (Either a b) a
113 | left = left'
114 |
115 | ||| A Prism focussing on the `Right` data constructor of `Either a b`.
116 | public export
117 | right' : Prism (Either a b) (Either a c) b c
118 | right' = P (either (Left . Left) Right) Right
119 |
120 | ||| Monomorphic version of `right'`.
121 | |||
122 | ||| This can improve type inference for those cases where the versatility
123 | ||| of `right'` is not needed.
124 | public export %inline
125 | right : Prism' (Either a b) b
126 | right = right'
127 |
128 | ||| A Prism focussing on the `Just` data constructor of a `Maybe`.
129 | public export
130 | just' : Prism (Maybe a) (Maybe b) a b
131 | just' = P (maybe (Left Nothing) Right) Just
132 |
133 | ||| Monomorphic version of `just'`.
134 | |||
135 | ||| This can improve type inference for those cases where the versatility
136 | ||| of `just'` is not needed.
137 | public export %inline
138 | just : Prism' (Maybe a) a
139 | just = just'
140 |
141 | ||| A Prism focussing on the `Nothing` data constructor of a `Maybe`.
142 | public export
143 | nothing : Prism' (Maybe a) ()
144 | nothing = P (maybe (Right ()) (Left . Just)) (const Nothing)
145 |
146 | ||| A Prism focussing on the `(::)` ("cons") data constructor of a
147 | ||| `List`.
148 | public export
149 | cons' : Prism (List a) (List b) (a,List a) (b,List b)
150 | cons' = P (\case Nil => Left Nil; h::t => Right (h,t)) (uncurry (::))
151 |
152 | ||| A Prism focussing on the `Nil` data constructor of a
153 | ||| `List`.
154 | public export
155 | nil : Prism' (List a) ()
156 | nil = prism (\case Nil => Just (); _ => Nothing) (const Nil)
157 |
158 | ||| Monomorphic version of `cons'`.
159 | |||
160 | ||| This can improve type inference for those cases where the versatility
161 | ||| of `cons'` is not needed.
162 | public export %inline
163 | cons : Prism' (List a) (a,List a)
164 | cons = cons'
165 |
166 | ||| A Prism focussing on the `(:<)` ("snoc") data constructor of a
167 | ||| `SnocList`.
168 | public export
169 | snoc' : Prism (SnocList a) (SnocList b) (SnocList a,a) (SnocList b,b)
170 | snoc' = P (\case Lin => Left Lin; i :< l => Right (i,l)) (uncurry (:<))
171 |
172 | ||| A Prism focussing on the `Lin` data constructor of a
173 | ||| `SnocList`.
174 | public export
175 | lin : Prism' (SnocList a) ()
176 | lin = prism (\case Lin => Just (); _ => Nothing) (const Lin)
177 |
178 | ||| Monomorphic version of `snoc'`.
179 | |||
180 | ||| This can improve type inference for those cases where the versatility
181 | ||| of `snoc'` is not needed.
182 | public export %inline
183 | snoc : Prism' (SnocList a) (SnocList a,a)
184 | snoc = snoc'
185 |
186 | ||| A Prism for converting between non-empty lists and regular lists.
187 | public export
188 | list1' : Prism (List a) (List b) (List1 a) (List1 b)
189 | list1' = P (\case Nil => Left Nil; h::t => Right (h ::: t)) forget
190 |
191 | public export %inline
192 | list1 : Prism' (List a) (List1 a)
193 | list1 = list1'
194 |
195 | ||| A Prism focussing on a single option in a heterogeneous sum.
196 | public export
197 | sum :
198 |      {0 ks : List k}
199 |   -> {0 f  : k -> Type}
200 |   -> (0 t : k)
201 |   -> {auto e : Elem t ks}
202 |   -> Prism' (Any f ks) (f t)
203 | sum t = prism project' inject
204 |
205 | public export
206 | anyHead : Prism' (Any f (k::ks)) (f k)
207 | anyHead = prism (\case Here v => Just v; _ => Nothing) Here
208 |
209 | public export
210 | anyTail : Prism' (Any f (k::ks)) (Any f ks)
211 | anyTail = prism (\case There v => Just v; _ => Nothing) There
212 |
213 | ||| A Prism focussing on non-negative integers.
214 | public export
215 | nat : Prism' Integer Nat
216 | nat = prism (\x => toMaybe (x >= 0) (cast x)) cast
217 |