0 | module Monocle.Iso
  1 |
  2 | import Monocle.Fold
  3 | import Monocle.Getter
  4 | import Monocle.Lens
  5 | import Monocle.Optional
  6 | import Monocle.Prism
  7 | import Monocle.Setter
  8 | import Monocle.Traversal
  9 | import Data.List.Quantifiers
 10 | import Data.Maybe
 11 |
 12 | %default total
 13 |
 14 | ||| An Iso describes an isomorphism between two types.
 15 | |||
 16 | ||| Two types are isomorphic, if there is a lossless conversion
 17 | ||| from one to the other and vice versa. Examples include the
 18 | ||| (monomorphic) isomorphism from `String` to `List Char` and the
 19 | ||| (polymorphic) isomorphism from `Either a b` to `Either b a`.
 20 | |||
 21 | ||| Isomorphisms must obey two identity laws:
 22 | |||
 23 | ||| `get_ . reverseGet` must be the identity function. The same holds
 24 | ||| for `reverseGet . get_`.
 25 | |||
 26 | ||| Isomorphisms are the most powerful kinds of optics, and they can
 27 | ||| be converted to all other optics in this library.
 28 | public export
 29 | record Iso s t a b where
 30 |   constructor I
 31 |   get_       : s -> a
 32 |   reverseGet : b -> t
 33 |
 34 | ||| Convenience alias for monomorphic Isos, which do not allow
 35 | ||| us to change the value and source types.
 36 | public export
 37 | 0 Iso' : (s,a : Type) -> Type
 38 | Iso' s a = Iso s s a a
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --          Interface
 42 | --------------------------------------------------------------------------------
 43 |
 44 | ||| Interface for converting other optics to Isos.
 45 | public export
 46 | interface ToIso (0 o : Type -> Type -> Type -> Type -> Type) where
 47 |   toIso : o s t a b -> Iso s t a b
 48 |
 49 | public export %inline
 50 | ToIso Iso where toIso = id
 51 |
 52 | --------------------------------------------------------------------------------
 53 | --          Conversions
 54 | --------------------------------------------------------------------------------
 55 |
 56 | public export
 57 | ToPrism Iso where
 58 |   toPrism (I g r) = P (Right . g) r
 59 |
 60 | public export
 61 | ToOptional Iso where
 62 |   toOptional (I g r) = O (Right . g) (\f => r . f . g)
 63 |
 64 | public export
 65 | ToSetter Iso where
 66 |   toSetter (I g r) = S $ \f => r . f . g
 67 |
 68 | public export %inline
 69 | ToFold Iso where
 70 |   toFold (I g r) = F (. g)
 71 |
 72 | public export
 73 | ToGetter Iso where
 74 |   toGetter (I g r) = G g
 75 |
 76 | public export
 77 | ToTraversal Iso where
 78 |   toTraversal i =
 79 |     T (\f,v => i.reverseGet <$> f (i.get_ v))
 80 |       (toFold i)
 81 |       (toSetter i)
 82 |
 83 | public export %inline
 84 | ToLens Iso where
 85 |   toLens (I g r) = L g $ \f => r . f . g
 86 |
 87 | --------------------------------------------------------------------------------
 88 | --          Utilitis
 89 | --------------------------------------------------------------------------------
 90 |
 91 | ||| Isomorphisms are symmetric: If `x` is isomorphic to `y` then `y` is
 92 | ||| isomorphic to `x`. This function describes this symmetry.
 93 | public export %inline
 94 | rev : Iso s t a b -> Iso b a t s
 95 | rev (I f g) = I g f
 96 |
 97 | ||| Sequential composition of Isos.
 98 | |||
 99 | ||| This describes the transitivity of isomorphisms: If `x` is isomorphic to
100 | ||| `y` and `y` is isomorhic to `z`, then `x` is isomorphic to `z`.
101 | public export
102 | (~>) : Iso s t a b -> Iso a b c d -> Iso s t c d
103 | I f1 g1 ~> I f2 g2 = I (f2 . f1) (g1 . g2)
104 |
105 | --------------------------------------------------------------------------------
106 | --          Isomorphisms
107 | --------------------------------------------------------------------------------
108 |
109 | ||| Isomorphisms are reflexive: Every type is trivially isomorphic to itself.
110 | export %inline
111 | identity : Iso' a a
112 | identity = I id id
113 |
114 | ||| The identity lens, derived from the corresponding isomorphism.
115 | export %inline
116 | idL : Lens' a a
117 | idL = toLens identity
118 |
119 | ||| The identity prism, derived from the corresponding isomorphism.
120 | export %inline
121 | idP : Prism' a a
122 | idP = toPrism identity
123 |
124 | ||| The identity optional, derived from the corresponding isomorphism.
125 | export %inline
126 | idO : Optional' a a
127 | idO = toOptional identity
128 |
129 | ||| The identity traversal, derived from the corresponding isomorphism.
130 | export %inline
131 | idT : Traversal' a a
132 | idT = toTraversal identity
133 |
134 | ||| Isomorphism between `List Char` and `String`.
135 | export
136 | pack : Iso' (List Char) String
137 | pack = I pack unpack
138 |
139 | ||| Isomorphism between `String` and `List Char`.
140 | export
141 | unpack : Iso' String (List Char)
142 | unpack = I unpack pack
143 |
144 | ||| Isomorphism between `SnocList` and `List`.
145 | export
146 | chips : Iso (SnocList a) (SnocList b) (List a) (List b)
147 | chips = I (<>> []) ([<] <><)
148 |
149 | ||| Isomorphism between `List` and `SnocList`.
150 | export
151 | fish : Iso (List a) (List b) (SnocList a) (SnocList b)
152 | fish = I ([<] <><) (<>> [])
153 |
154 | ||| Isomorphism between pairs with their values swapped.
155 | export
156 | swap : Iso (a,b) (c,d) (b,a) (d,c)
157 | swap = I swap swap
158 |
159 | ||| Isomorphism between binary functions with their arguments
160 | ||| swapped.
161 | export
162 | flip : Iso (a -> b -> c) (d -> e -> f) (b -> a -> c) (e -> d -> f)
163 | flip = I flip flip
164 |
165 | ||| Isomorphism between binary functions and functions taking
166 | ||| a pair of values as their argument.
167 | export
168 | uncurry : Iso (a -> b -> c) (d -> e -> f) ((a,b) -> c) ((d,e) -> f)
169 | uncurry = I uncurry curry
170 |
171 | ||| Isomorphism between functions taking a pair as their argument
172 | ||| and binary functions.
173 | export
174 | curry : Iso ((a,b) -> c) ((d,e) -> f) (a -> b -> c) (d -> e -> f)
175 | curry = I curry uncurry
176 |
177 | ||| Isomorphism between `Either a b` and `Either b a`.
178 | export
179 | swapE : Iso (Either a b) (Either c d) (Either b a) (Either d c)
180 | swapE = I (either Right Left) (either Right Left)
181 |
182 | ||| Given a default value of type `a`, we can create an isomorphism between
183 | ||| `Maybe a` and values of type `a`.
184 | |||
185 | ||| This wraps every value of type `a` in a `Just`. In the other direction,
186 | ||| we use `fromMaybe` with the provided default value to extract a value
187 | ||| from a `Nothing`.
188 | export
189 | withDefault : a -> Iso' (Maybe a) a
190 | withDefault v = I (fromMaybe v) Just
191 |
192 | ||| Isomorphism between `Either Void a` and `a`: The `Left` case
193 | ||| is impossible because `Void` is uninhabited.
194 | export
195 | leftVoid : Iso (Either Void a) (Either Void b) a b
196 | leftVoid = I (either absurd id) Right
197 |
198 | ||| Isomorphism between `Either a Void` and `a`: The `Right` case
199 | ||| is impossible because `Void` is uninhabited.
200 | export
201 | rightVoid : Iso (Either a Void) (Either b Void) a b
202 | rightVoid = I (either id absurd) Left
203 |
204 | ||| Isomorphism between a unary sum type and the wrapped value.
205 | export
206 | any1 : Iso (Any f [a]) (Any g [b]) (f a) (g b)
207 | any1 = I (\case Here v => v) Here
208 |