Implement composition of indexed optics

src/Control/Applicative/Indexing.idr

@@ -6,17 +6,17 @@ import Data.Contravariant
 
 
 public export
-record Indexing {0 k : Type} f (a : k) where
+record Indexing {0 k : Type} i f (a : k) where
   constructor MkIndexing
-  runIndexing : Nat -> (Nat, f a)
+  runIndexing : i -> (i, f a)
 
 
 public export
-Functor f => Functor (Indexing f) where
+Functor f => Functor (Indexing i f) where
   map f (MkIndexing g) = MkIndexing (mapSnd (map f) . g)
 
 public export
-Applicative f => Applicative (Indexing f) where
+Applicative f => Applicative (Indexing i f) where
   pure x = MkIndexing $ \i => (i, pure x)
   MkIndexing mf <*> MkIndexing ma = MkIndexing $ \i =>
     let (j, ff) = mf i
@@ -24,10 +24,10 @@ Applicative f => Applicative (Indexing f) where
     in (k, ff <*> fa)
 
 public export
-Contravariant f => Contravariant (Indexing f) where
+Contravariant f => Contravariant (Indexing i f) where
   contramap f (MkIndexing g) = MkIndexing (mapSnd (contramap f) . g)
 
 
 public export
-indexing : ((a -> Indexing f b) -> s -> Indexing f t) -> (Nat -> a -> f b) -> s -> f t
-indexing l fn s = snd $ runIndexing {f} (l (\x => MkIndexing $ \i => (S i, fn i x)) s) 0
+indexing : Num i => ((a -> Indexing i f b) -> s -> Indexing i f t) -> (i -> a -> f b) -> s -> f t
+indexing l fn s = snd $ runIndexing {f} (l (\x => MkIndexing $ \i => (1 + i, fn i x)) s) 0

src/Control/Lens/Fold.idr

@@ -23,7 +23,7 @@ import Control.Lens.Traversal
 public export
 record IsFold p where
   constructor MkIsFold
-  runIsFold : (Traversing p, Cochoice p, Bicontravariant p)
+  runIsFold : (Traversing p, Bicontravariant p)
 
 export %hint
 foldToOptFold : IsFold p => IsOptFold p

src/Control/Lens/Getter.idr

@@ -18,12 +18,16 @@ import Control.Lens.Lens
 public export
 record IsGetter p where
   constructor MkIsGetter
-  runIsGetter : (Strong p, Cochoice p, Bicontravariant p)
+  runIsGetter : (Strong p, Bicontravariant p)
 
 export %hint
 getterToLens : IsGetter p => IsLens p
 getterToLens @{MkIsGetter _} = MkIsLens %search
 
+export %hint
+indexedGetter : IsGetter p => IsGetter (Indexed i p)
+indexedGetter @{MkIsGetter _} = MkIsGetter %search
+
 
 ||| A getter is an optic that only supports getting, not setting.
 |||

src/Control/Lens/Indexed.idr

@@ -1,6 +1,11 @@
 module Control.Lens.Indexed
 
+import Data.Tensor
 import Data.Profunctor
+import Data.Profunctor.Costrong
+import Data.Profunctor.Traversing
+import Data.Profunctor.Mapping
+import Data.Bicontravariant
 import Control.Lens.Optic
 import Control.Lens.Iso
 
@@ -31,3 +36,84 @@ public export
 0 IndexedOptic : ((Type -> Type -> Type) -> Type) -> (i,s,t,a,b : Type) -> Type
 IndexedOptic constr i s t a b =
   forall p,p'. constr p => Indexable i p p' => p' a b -> p s t
+
+
+
+public export
+record Indexed i (p : Type -> Type -> Type) a b where
+  constructor MkIndexed
+  runIndexed : p (i, a) b
+
+public export
+Bifunctor p => Bifunctor (Indexed i p) where
+  bimap f g (MkIndexed k) = MkIndexed $ bimap (mapSnd f) g k
+  mapFst f (MkIndexed k) = MkIndexed $ mapFst (mapSnd f) k
+  mapSnd f (MkIndexed k) = MkIndexed $ mapSnd f k
+
+public export
+Bicontravariant p => Bicontravariant (Indexed i p) where
+  contrabimap f g (MkIndexed k) = MkIndexed $ contrabimap (mapSnd f) g k
+
+public export
+Profunctor p => Profunctor (Indexed i p) where
+  dimap f g (MkIndexed k) = MkIndexed $ dimap (mapSnd f) g k
+  lmap f (MkIndexed k) = MkIndexed $ lmap (mapSnd f) k
+  rmap f (MkIndexed k) = MkIndexed $ rmap f k
+
+public export
+Bifunctor ten => GenStrong ten p => GenStrong ten (Indexed i p) where
+  strongl (MkIndexed k) = MkIndexed $ lmap (\(i,x) => mapFst (i,) x) (strongl {ten,p} k)
+  strongr (MkIndexed k) = MkIndexed $ lmap (\(i,x) => mapSnd (i,) x) (strongr {ten,p} k)
+
+public export
+Traversing p => Traversing (Indexed i p) where
+  wander tr (MkIndexed k) = MkIndexed $ wander (\f,(i,x) => tr (f . (i,)) x) k
+
+public export
+Closed p => Closed (Indexed i p) where
+  closed (MkIndexed k) = MkIndexed $ lmap (\(i,f),x => (i, f x)) (closed k)
+
+public export
+Mapping p => Mapping (Indexed i p) where
+  roam mp (MkIndexed k) = MkIndexed $ roam (\f,(i,x) => mp (f . (i,)) x) k
+
+export %hint
+indexedIso : IsIso p => IsIso (Indexed i p)
+indexedIso @{MkIsIso _} = MkIsIso %search
+
+
+
+
+public export
+icompose : IsIso p => (i -> j -> k) ->
+            IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' ->
+            IndexedOptic' p k s t a' b'
+icompose @{MkIsIso _} f l l' @{ind} =
+  l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
+  . lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
+
+infixr 9 <.>
+infixr 9 .>
+infixr 9 <.
+
+public export
+(<.>) : IsIso p => IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' ->
+                    IndexedOptic' p (i, j) s t a' b'
+(<.>) = icompose (,)
+
+public export
+(.>) : Optic' p s t a b -> IndexedOptic' p i a b a' b' -> IndexedOptic' p i s t a' b'
+(.>) l l' = l . l'
+
+public export
+(<.) : IndexedOptic' p i s t a b -> Optic' (Indexed i p) a b a' b' -> IndexedOptic' p i s t a' b'
+(<.) l l' @{ind} = l @{Idxed} . runIndexed . l' . MkIndexed {p} . indexed @{ind}
+
+
+public export
+constIndex : IsIso p => i -> Optic' p s t a b -> IndexedOptic' p i s t a b
+constIndex i l @{MkIsIso _} @{ind} = l . lmap (i,) . indexed @{ind}
+
+public export
+reindexed : IsIso p => (i -> j) -> IndexedOptic' p i s t a b -> IndexedOptic' p j s t a b
+reindexed @{MkIsIso _} f l @{ind} = l @{Idxed} . lmap (mapFst f) . indexed @{ind}

src/Control/Lens/Lens.idr

@@ -25,6 +25,10 @@ export %hint
 lensToIso : IsLens p => IsIso p
 lensToIso @{MkIsLens _} = MkIsIso %search
 
+export %hint
+indexedLens : IsLens p => IsLens (Indexed i p)
+indexedLens @{MkIsLens _} = MkIsLens %search
+
 
 ||| A *lens* is a functional reference to a value within a larger data structure.
 ||| Lenses allow one to access or modify the value that they reference, called

src/Control/Lens/Optional.idr

@@ -27,6 +27,10 @@ export %hint
 optionalToPrism : IsOptional p => IsPrism p
 optionalToPrism @{MkIsOptional _} = MkIsPrism %search
 
+export %hint
+indexedOptional : IsOptional p => IsOptional (Indexed i p)
+indexedOptional @{MkIsOptional _} = MkIsOptional %search
+
 
 ||| An `Optional` is a lens that may or may not contain the focus value.
 ||| As such, accesses will return a `Maybe` value.

src/Control/Lens/OptionalFold.idr

@@ -19,7 +19,7 @@ import Control.Lens.Getter
 public export
 record IsOptFold p where
   constructor MkIsOptFold
-  runIsOptFold : (Strong p, Choice p, Cochoice p, Bicontravariant p)
+  runIsOptFold : (Strong p, Choice p, Bicontravariant p)
 
 export %hint
 optFoldToOptional : IsOptFold p => IsOptional p
@@ -29,6 +29,10 @@ export %hint
 optFoldToGetter : IsOptFold p => IsGetter p
 optFoldToGetter @{MkIsOptFold _} = MkIsGetter %search
 
+export %hint
+indexedOptFold : IsOptFold p => IsOptFold (Indexed i p)
+indexedOptFold @{MkIsOptFold _} = MkIsOptFold %search
+
 
 ||| An `OptionalFold` is a getter that may not return a focus value.
 ||| `OptionalFold s a` is equivalent to `s -> Maybe a`.

src/Control/Lens/Prism.idr

@@ -22,6 +22,10 @@ export %hint
 prismToIso : IsPrism p => IsIso p
 prismToIso @{MkIsPrism _} = MkIsIso %search
 
+export %hint
+indexedPrism : IsPrism p => IsPrism (Indexed i p)
+indexedPrism @{MkIsPrism _} = MkIsPrism %search
+
 
 ||| A prism is a first-class reference to one of the cases of a sum type.
 ||| Prisms allow one to determine whether a value matches the focused case

src/Control/Lens/Setter.idr

@@ -23,11 +23,15 @@ record IsSetter p where
   constructor MkIsSetter
   runIsSetter : Mapping p
 
-
 export %hint
 setterToTraversal : IsSetter p => IsTraversal p
 setterToTraversal @{MkIsSetter _} = MkIsTraversal %search
 
+export %hint
+indexedSetter : IsSetter p => IsSetter (Indexed i p)
+indexedSetter @{MkIsSetter _} = MkIsSetter %search
+
+
 
 ||| A setter is an optic that only supports setting, not getting.
 |||

src/Control/Lens/Traversal.idr

@@ -29,6 +29,10 @@ export %hint
 traversalToOptional : IsTraversal p => IsOptional p
 traversalToOptional @{MkIsTraversal _} = MkIsOptional %search
 
+export %hint
+indexedTraversal : IsTraversal p => IsTraversal (Indexed i p)
+indexedTraversal @{MkIsTraversal _} = MkIsTraversal %search
+
 
 ||| A traversal is a lens that may have more than one focus.
 public export
@@ -55,11 +59,11 @@ IndexedTraversal' = Simple . IndexedTraversal
 
 
 public export
-iordinal : Traversal s t a b -> IndexedTraversal Nat s t a b
-iordinal l @{MkIsTraversal _} @{ind} = wander (func . curry) . indexed @{ind}
+iordinal : Num i => Traversal s t a b -> IndexedTraversal i s t a b
+iordinal @{_} l @{MkIsTraversal _} @{ind} = wander (func . curry) . indexed @{ind}
   where
-    func : forall f. Applicative f => (Nat -> a -> f b) -> s -> f t
-    func = indexing $ applyStar . l . MkStar {f = Indexing f}
+    func : forall f. Applicative f => (i -> a -> f b) -> s -> f t
+    func = indexing $ applyStar . l . MkStar {f = Indexing i f}
 
 
 ||| Derive a traversal from a `Traversable` implementation.
@@ -68,7 +72,7 @@ traversed : Traversable t => Traversal (t a) (t b) a b
 traversed @{_} @{MkIsTraversal _} = traverse'
 
 public export
-itraversed : Traversable t => IndexedTraversal Nat (t a) (t b) a b
+itraversed : Num i => Traversable t => IndexedTraversal i (t a) (t b) a b
 itraversed = iordinal traversed
 
 ||| Contstruct a traversal over a `Bitraversable` container with matching types.

src/Data/Either/Lens.idr

@@ -18,9 +18,7 @@ Right_ @{MkIsPrism _} = right
 public export
 chosen : IndexedLens (Either () ()) (Either a a) (Either b b) a b
 chosen = ilens
-  (\case
-    Left x => (Left (), x)
-    Right x => (Right (), x))
+  (either (Left (),) (Right (),))
   (\case
     Left _ => Left
     Right _ => Right)