0 | module Control.Lens.Indexed
  1 |
  2 | import Data.Tensor
  3 | import Data.Profunctor
  4 | import Data.Profunctor.Costrong
  5 | import Data.Profunctor.Traversing
  6 | import Data.Profunctor.Mapping
  7 | import Data.Bicontravariant
  8 | import Control.Lens.Optic
  9 | import Control.Lens.Iso
 10 |
 11 | %default total
 12 |
 13 |
 14 | public export
 15 | interface Indexable i (0 p, p' : Type -> Type -> Type) | p, p' where
 16 |   indexed : p' a b -> p (i, a) b
 17 |
 18 |
 19 | -- Non-indexed use (default)
 20 | public export
 21 | IsIso p => Indexable i p p where
 22 |   indexed @{MkIsIso _} = lmap snd
 23 |
 24 | -- Indexed use
 25 | public export
 26 | [Idxed] Indexable i p (p . (i,)) where
 27 |   indexed = id
 28 |
 29 |
 30 | public export
 31 | 0 IndexedOptic' : (Type -> Type -> Type) -> (i,s,t,a,b : Type) -> Type
 32 | IndexedOptic' p i s t a b = forall p'. Indexable i p p' => p' a b -> p s t
 33 |
 34 | public export
 35 | 0 IndexedOptic : ((Type -> Type -> Type) -> Type) -> (i,s,t,a,b : Type) -> Type
 36 | IndexedOptic constr i s t a b =
 37 |   forall p,p'. constr p => Indexable i p p' => p' a b -> p s t
 38 |
 39 |
 40 |
 41 | public export
 42 | record Indexed i (p : Type -> Type -> Type) a b where
 43 |   constructor MkIndexed
 44 |   runIndexed : p (i, a) b
 45 |
 46 | public export
 47 | Bifunctor p => Bifunctor (Indexed i p) where
 48 |   bimap f g (MkIndexed k) = MkIndexed $ bimap (mapSnd f) g k
 49 |   mapFst f (MkIndexed k) = MkIndexed $ mapFst (mapSnd f) k
 50 |   mapSnd f (MkIndexed k) = MkIndexed $ mapSnd f k
 51 |
 52 | public export
 53 | Bicontravariant p => Bicontravariant (Indexed i p) where
 54 |   contrabimap f g (MkIndexed k) = MkIndexed $ contrabimap (mapSnd f) g k
 55 |
 56 | public export
 57 | Profunctor p => Profunctor (Indexed i p) where
 58 |   dimap f g (MkIndexed k) = MkIndexed $ dimap (mapSnd f) g k
 59 |   lmap f (MkIndexed k) = MkIndexed $ lmap (mapSnd f) k
 60 |   rmap f (MkIndexed k) = MkIndexed $ rmap f k
 61 |
 62 | public export
 63 | Bifunctor ten => GenStrong ten p => GenStrong ten (Indexed i p) where
 64 |   strongl (MkIndexed k) = MkIndexed $ lmap (\(i,x) => mapFst (i,) x) (strongl {ten,p} k)
 65 |   strongr (MkIndexed k) = MkIndexed $ lmap (\(i,x) => mapSnd (i,) x) (strongr {ten,p} k)
 66 |
 67 | public export
 68 | Traversing p => Traversing (Indexed i p) where
 69 |   wander tr (MkIndexed k) = MkIndexed $ wander (\f,(i,x) => tr (f . (i,)) x) k
 70 |
 71 | public export
 72 | Closed p => Closed (Indexed i p) where
 73 |   closed (MkIndexed k) = MkIndexed $ lmap (\(i,f),x => (i, f x)) (closed k)
 74 |
 75 | public export
 76 | Mapping p => Mapping (Indexed i p) where
 77 |   roam mp (MkIndexed k) = MkIndexed $ roam (\f,(i,x) => mp (f . (i,)) x) k
 78 |
 79 | export %hint
 80 | indexedIso : IsIso p => IsIso (Indexed i p)
 81 | indexedIso @{MkIsIso _} = MkIsIso %search
 82 |
 83 |
 84 |
 85 | ||| Compose two indexed optics, using a function to combine the indices of each
 86 | ||| optic.
 87 | public export
 88 | icompose : IsIso p => (i -> j -> k) ->
 89 |             IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' ->
 90 |             IndexedOptic' p k s t a' b'
 91 | icompose @{MkIsIso _} f l l' @{ind} =
 92 |   l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
 93 |   . lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
 94 |
 95 | export infixr 9 <.>, .>, <.
 96 |
 97 | ||| Compose two indexed optics, returning an optic indexed by a pair of indices.
 98 | |||
 99 | ||| Mnemonically, the angle brackets point to the fact that we want to preserve
100 | ||| both indices.
101 | public export
102 | (<.>) : IsIso p => IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' ->
103 |                     IndexedOptic' p (i, j) s t a' b'
104 | (<.>) = icompose (,)
105 |
106 | ||| Compose a non-indexed optic with an indexed optic.
107 | |||
108 | ||| Mnemonically, the angle bracket points to the index that we want to preserve.
109 | public export
110 | (.>) : Optic' p s t a b -> IndexedOptic' p i a b a' b' -> IndexedOptic' p i s t a' b'
111 | (.>) l l' = l . l'
112 |
113 | ||| Compose an indexed optic with a non-indexed optic.
114 | |||
115 | ||| Mnemonically, the angle bracket points to the index that we want to preserve.
116 | public export
117 | (<.) : IndexedOptic' p i s t a b -> Optic' (Indexed i p) a b a' b' -> IndexedOptic' p i s t a' b'
118 | (<.) l l' @{ind} = l @{Idxed} . runIndexed . l' . MkIndexed {p} . indexed @{ind}
119 |
120 |
121 | ||| Augment an optic with an index that is constant for all inputs.
122 | public export
123 | constIndex : IsIso p => i -> Optic' p s t a b -> IndexedOptic' p i s t a b
124 | constIndex i l @{MkIsIso _} @{ind} = l . lmap (i,) . indexed @{ind}
125 |
126 | ||| Modify the indices of an indexed optic.
127 | public export
128 | reindexed : IsIso p => (i -> j) -> IndexedOptic' p i s t a b -> IndexedOptic' p j s t a b
129 | reindexed @{MkIsIso _} f l @{ind} = l @{Idxed} . lmap (mapFst f) . indexed @{ind}
130 |