0 | module Control.Lens.Iso
  1 |
  2 | import Data.Maybe
  3 | import Data.Contravariant
  4 | import Data.Tensor
  5 | import Data.Profunctor
  6 | import Control.Monad.Identity
  7 | import Control.Applicative.Const
  8 | import Control.Lens.Optic
  9 | import Control.Lens.Equality
 10 |
 11 | %default total
 12 |
 13 |
 14 | ------------------------------------------------------------------------------
 15 | -- Type definitions
 16 | ------------------------------------------------------------------------------
 17 |
 18 |
 19 | public export
 20 | record IsIso p where
 21 |   constructor MkIsIso
 22 |   runIsIso : Profunctor p
 23 |
 24 |
 25 | ||| An `Iso` is an isomorphism family between types. It allows a value to be
 26 | ||| converted or updated across this isomorphism.
 27 | public export
 28 | 0 Iso : (s,t,a,b : Type) -> Type
 29 | Iso = Optic IsIso
 30 |
 31 | ||| An `Iso'` is an isomorphism family between types. It allows a value to be
 32 | ||| converted or updated across this isomorphism.
 33 | ||| This is the `Simple` version of `Iso`.
 34 | public export
 35 | 0 Iso' : (s,a : Type) -> Type
 36 | Iso' = Simple Iso
 37 |
 38 |
 39 | ------------------------------------------------------------------------------
 40 | -- Utilities for isomorphisms
 41 | ------------------------------------------------------------------------------
 42 |
 43 |
 44 | -- Eliminators
 45 |
 46 | ||| Extract the conversion functions from an `Iso`.
 47 | public export
 48 | getIso : Iso s t a b -> (s -> a, b -> t)
 49 | getIso l = l @{MkIsIso coexp} (id, id)
 50 |   where
 51 |     [coexp] Profunctor (\x,y => (x -> a, b -> y)) where
 52 |       dimap f g (f', g') = (f' . f, g . g')
 53 |
 54 | ||| Extract the conversion functions from an `Iso`.
 55 | public export
 56 | withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
 57 | withIso l f = uncurry f (getIso l)
 58 |
 59 |
 60 |
 61 | -- Constructors
 62 |
 63 | ||| Construct an `Iso` from two inverse functions.
 64 | public export
 65 | iso : (s -> a) -> (b -> t) -> Iso s t a b
 66 | iso f g @{MkIsIso _} = dimap f g
 67 |
 68 | ||| Construct a simple `Iso` from an equivalence.
 69 | public export
 70 | fromEqv : s <=> a -> Iso' s a
 71 | fromEqv (MkEquivalence l r) = iso l r
 72 |
 73 | ||| Invert an isomorphism.
 74 | public export
 75 | from : Iso s t a b -> Iso b a t s
 76 | from l @{MkIsIso _} = withIso l (flip dimap)
 77 |
 78 |
 79 | -- `au`
 80 |
 81 | ||| Based on Epigram's `ala`.
 82 | public export
 83 | au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
 84 | au l f = withIso l $ \g,h => g <$> f h
 85 |
 86 | ||| Based on Epigram's `ala'`.
 87 | public export
 88 | auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
 89 | auf l f x = withIso l $ \g,h => g <$> f (h <$> x)
 90 |
 91 | ||| An alias for `au . from`.
 92 | public export
 93 | xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
 94 | xplat l f = withIso l $ \g,h => h <$> f g
 95 |
 96 | ||| an alias for `auf . from`.
 97 | public export
 98 | xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
 99 | xplatf l f x = withIso l $ \g,h => h <$> f (g <$> x)
100 |
101 |
102 | ||| Update a value under an `Iso`, as opposed to `over` it.
103 | ||| In other words, this is a convenient alias for `over . from`.
104 | public export
105 | under : Iso s t a b -> (t -> s) -> (b -> a)
106 | under l = let (f,g) = getIso l in (f .) . (. g)
107 |
108 |
109 | -- Examples of isomorphisms
110 |
111 | ||| An "isomorphism" between a function and its result type, assuming that
112 | ||| the parameter type is inhabited.
113 | public export
114 | constant : a -> Iso (a -> b) (a' -> b') b b'
115 | constant x = iso ($ x) const
116 |
117 | ||| Construct an isomorphism given an involution.
118 | public export
119 | involuted : (a -> a) -> Iso' a a
120 | involuted f = iso f f
121 |
122 | ||| Flipping a function's arguments forms an isomorphism.
123 | public export
124 | flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
125 | flipped = iso flip flip
126 |
127 | ||| Swapping a symmetric tensor product's parameters is an isomorphism.
128 | public export
129 | swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
130 | swapped = iso swap' swap'
131 |
132 | ||| Casting between types forms an isomorphism.
133 | ||| WARNING: This is only a true isomorphism if casts in both directions are
134 | ||| lossless and mutually inverse.
135 | public export
136 | casted : (Cast s a, Cast b t) => Iso s t a b
137 | casted = iso cast cast
138 |
139 | ||| The isomorphism `non x` converts between `Maybe a` and `a` sans the
140 | ||| element `x`.
141 | |||
142 | ||| This is useful for working with optics whose focus type is `Maybe a`,
143 | ||| such as `at`.
144 | public export
145 | non : Eq a => a -> Iso' (Maybe a) a
146 | non x = iso (fromMaybe x) (\y => guard (x /= y) $> y)
147 |
148 |
149 | public export
150 | Id_ : Iso (Identity a) (Identity b) a b
151 | Id_ = iso runIdentity Id
152 |
153 | public export
154 | Const_ : Iso (Const a b) (Const c d) a c
155 | Const_ = iso runConst MkConst
156 |
157 |
158 | -- Mapping
159 |
160 | ||| Lift an isomorphism through a `Functor`.
161 | public export
162 | mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
163 | mapping l = withIso l $ \f,g => iso (map f) (map g)
164 |
165 | ||| Lift an isomorphism through a `Contravariant` functor.
166 | public export
167 | contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
168 | contramapping l = withIso l $ \f,g => iso (contramap f) (contramap g)
169 |
170 | ||| Lift isomorphisms through a `Bifunctor`.
171 | public export
172 | bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' ->
173 |               Iso (f s s') (g t t') (f a a') (g b b')
174 | bimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
175 |   iso (bimap f f') (bimap g g')
176 |
177 | ||| Lift an isomorphism through the first parameter of a `Bifunctor`.
178 | public export
179 | mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b ->
180 |               Iso (f s x) (g t y) (f a x) (g b y)
181 | mappingFst l = withIso l $ \f,g => iso (mapFst f) (mapFst g)
182 |
183 | ||| Lift an isomorphism through the second parameter of a `Bifunctor`.
184 | public export
185 | mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b ->
186 |               Iso (f x s) (g y t) (f x a) (g y b)
187 | mappingSnd l = withIso l $ \f,g => iso (mapSnd f) (mapSnd g)
188 |
189 | ||| Lift isomorphisms through a `Profunctor`.
190 | public export
191 | dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' ->
192 |               Iso (f a s') (g b t') (f s a') (g t b')
193 | dimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
194 |   iso (dimap f f') (dimap g g')
195 |
196 | ||| Lift an isomorphism through the first parameter of a `Profunctor`.
197 | public export
198 | lmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
199 |               Iso (f a x) (g b y) (f s x) (g t y)
200 | lmapping l = withIso l $ \f,g => iso (lmap f) (lmap g)
201 |
202 | ||| Lift an isomorphism through the second parameter of a `Profunctor`.
203 | public export
204 | rmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
205 |               Iso (f x s) (g y t) (f x a) (g y b)
206 | rmapping l = withIso l $ \f,g => iso (rmap f) (rmap g)
207 |
208 |