From 090b06a899e800455efae1fe41dbb935de10655a Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sat, 8 Apr 2023 16:18:03 -0400
Subject: [PATCH] Basic package structure

---
 lens.ipkg                     |   6 +-
 src/Control/Lens/Equality.idr |  50 ++++++++++++
 src/Control/Lens/Iso.idr      | 143 ++++++++++++++++++++++++++++++++++
 src/Control/Lens/Lens.idr     |  63 +++++++++++++++
 src/Control/Lens/Optic.idr    |  14 ++++
 5 files changed, 275 insertions(+), 1 deletion(-)
 create mode 100644 src/Control/Lens/Equality.idr
 create mode 100644 src/Control/Lens/Iso.idr
 create mode 100644 src/Control/Lens/Lens.idr
 create mode 100644 src/Control/Lens/Optic.idr

diff --git a/lens.ipkg b/lens.ipkg
index d1affcc..a9c35a4 100644
--- a/lens.ipkg
+++ b/lens.ipkg
@@ -10,5 +10,9 @@ sourcedir = "src"
 readme = "README.md"
 
 langversion >= 0.6.0
+depends = profunctors >= 1.1.2
 
-modules =
+modules = Control.Lens.Optic,
+          Control.Lens.Equality,
+          Control.Lens.Iso,
+          Control.Lens.Lens
diff --git a/src/Control/Lens/Equality.idr b/src/Control/Lens/Equality.idr
new file mode 100644
index 0000000..cead56b
--- /dev/null
+++ b/src/Control/Lens/Equality.idr
@@ -0,0 +1,50 @@
+module Control.Lens.Equality
+
+import Control.Lens.Optic
+
+%default total
+
+
+public export
+record IsEquality {0 k,k' : _} (p : k -> k' -> Type) where
+  constructor MkIsEquality
+
+public export
+0 Equality : k -> k' -> k -> k' -> Type
+Equality s t a b = forall p. IsEquality p => p a b -> p s t
+
+public export
+0 Equality' : k -> k -> Type
+Equality' s a = Equality s s a a
+
+
+public export
+runEq : Equality s t a b -> (s = a, t = b)
+runEq l = (l {p = \x,_ => x = a} Refl,
+           l {p = \_,y => y = b} Refl)
+
+public export
+runEq' : Equality s t a b -> s = a
+runEq' l = l {p = \x,_ => x = a} Refl
+
+
+public export
+substEq : forall p. Equality s t a b -> p a b a b -> p s t a b
+substEq {p} l = l {p = \x,y => p x y a b}
+
+public export
+congEq : forall f,g. Equality s t a b -> Equality (f s) (g t) (f a) (g b)
+congEq l {p} = l {p = \x,y => p (f x) (g y)}
+
+public export
+symEq : Equality s t a b -> Equality b a t s
+symEq l = case runEq l of (Refl, Refl) => id
+
+
+public export
+refl : Equality a b a b
+refl = id
+
+public export
+simple : Equality' a a
+simple = id
diff --git a/src/Control/Lens/Iso.idr b/src/Control/Lens/Iso.idr
new file mode 100644
index 0000000..493be10
--- /dev/null
+++ b/src/Control/Lens/Iso.idr
@@ -0,0 +1,143 @@
+module Control.Lens.Iso
+
+import Data.Maybe
+import Data.Contravariant
+import Data.Tensor
+import Data.Profunctor
+import Control.Lens.Optic
+import Control.Lens.Equality
+
+%default total
+
+
+public export
+record IsIso p where
+  constructor MkIsIso
+  runIsIso : Profunctor p
+
+
+
+public export
+0 Iso : (s,t,a,b : Type) -> Type
+Iso = Optic IsIso
+
+public export
+0 Iso' : (s,a : Type) -> Type
+Iso' s a = Iso s s a a
+
+
+public export
+getIso : Iso s t a b -> (s -> a, b -> t)
+getIso l = l @{MkIsIso coexp} (id, id)
+  where
+    [coexp] Profunctor (\x,y => (x -> a, b -> y)) where
+      dimap f g (f', g') = (f' . f, g . g')
+
+public export
+withIso : Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+withIso l f = uncurry f (getIso l)
+
+public export
+under : Iso s t a b -> (t -> s) -> (b -> a)
+under l = let (f,g) = getIso l in (f .) . (. g)
+
+
+public export
+iso : (s -> a) -> (b -> t) -> Iso s t a b
+iso f g @{MkIsIso _} = dimap f g
+
+public export
+fromEqv : s <=> a -> Iso' s a
+fromEqv (MkEquivalence l r) = iso l r
+
+public export
+from : Iso s t a b -> Iso b a t s
+from l @{MkIsIso _} = withIso l (flip dimap)
+
+
+
+public export
+au : Functor f => Iso s t a b -> ((b -> t) -> f s) -> f a
+au l f = withIso l $ \g,h => g <$> f h
+
+public export
+auf : (Functor f, Functor g) => Iso s t a b -> (f t -> g s) -> f b -> g a
+auf l f x = withIso l $ \g,h => g <$> f (h <$> x)
+
+public export
+xplat : Functor f => Iso s t a b -> ((s -> a) -> f b) -> f t
+xplat l f = withIso l $ \g,h => h <$> f g
+
+public export
+xplatf : (Functor f, Functor g) => Iso s t a b -> (f a -> g b) -> f s -> g t
+xplatf l f x = withIso l $ \g,h => h <$> f (g <$> x)
+
+
+-- Example Isos
+
+public export
+constant : a -> Iso (a -> b) (a' -> b') b b'
+constant x = iso ($ x) const
+
+public export
+involuted : (a -> a) -> Iso' a a
+involuted f = iso f f
+
+public export
+flipped : Iso (a -> b -> c) (a' -> b' -> c') (b -> a -> c) (b' -> a' -> c')
+flipped = iso flip flip
+
+public export
+swapped : Symmetric f => Iso (f a b) (f a' b') (f b a) (f b' a')
+swapped = iso swap' swap'
+
+public export
+casted : (Cast s a, Cast b t) => Iso s t a b
+casted = iso cast cast
+
+public export
+non : Eq a => a -> Iso' (Maybe a) a
+non x = iso (fromMaybe x) (\y => guard (x /= y) $> y)
+
+-- Mapping
+
+public export
+mapping : (Functor f, Functor g) => Iso s t a b -> Iso (f s) (g t) (f a) (g b)
+mapping l = withIso l $ \f,g => iso (map f) (map g)
+
+public export
+contramapping : (Contravariant f, Contravariant g) => Iso s t a b -> Iso (f a) (g b) (f s) (g t)
+contramapping l = withIso l $ \f,g => iso (contramap f) (contramap g)
+
+public export
+bimapping : (Bifunctor f, Bifunctor g) => Iso s t a b -> Iso s' t' a' b' ->
+              Iso (f s s') (g t t') (f a a') (g b b')
+bimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
+  iso (bimap f f') (bimap g g')
+
+public export
+mappingFst : (Bifunctor f, Bifunctor g) => Iso s t a b ->
+              Iso (f s x) (g t y) (f a x) (g b y)
+mappingFst l = withIso l $ \f,g => iso (mapFst f) (mapFst g)
+
+public export
+mappingSnd : (Bifunctor f, Bifunctor g) => Iso s t a b ->
+              Iso (f x s) (g y t) (f x a) (g y b)
+mappingSnd l = withIso l $ \f,g => iso (mapSnd f) (mapSnd g)
+
+public export
+dimapping : (Profunctor f, Profunctor g) => Iso s t a b -> Iso s' t' a' b' ->
+              Iso (f a s') (g b t') (f s a') (g t b')
+dimapping l r = withIso l $ \f,g => withIso r $ \f',g' =>
+  iso (dimap f f') (dimap g g')
+
+public export
+lmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
+              Iso (f a x) (g b y) (f s x) (g t y)
+lmapping l = withIso l $ \f,g => iso (lmap f) (lmap g)
+
+public export
+rmapping : (Profunctor f, Profunctor g) => Iso s t a b ->
+              Iso (f x s) (g y t) (f x a) (g y b)
+rmapping l = withIso l $ \f,g => iso (rmap f) (rmap g)
+
diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
new file mode 100644
index 0000000..3d52d64
--- /dev/null
+++ b/src/Control/Lens/Lens.idr
@@ -0,0 +1,63 @@
+module Control.Lens.Lens
+
+import Data.Profunctor
+import Data.Profunctor.Yoneda
+import Control.Lens.Optic
+import Control.Lens.Equality
+import Control.Lens.Iso
+
+%default total
+
+
+public export
+record IsLens p where
+  constructor MkIsLens
+  runIsLens : Strong p
+
+export %hint
+lensToIso : IsLens p => IsIso p
+lensToIso @{MkIsLens _} = MkIsIso %search
+
+
+public export
+0 Lens : (s,t,a,b : Type) -> Type
+Lens = Optic IsLens
+
+public export
+0 Lens' : (s,a : Type) -> Type
+Lens' s a = Lens s s a a
+
+
+public export
+lens : (s -> a) -> (s -> b -> t) -> Lens s t a b
+lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
+
+public export
+getLens : Lens s t a b -> (s -> a, s -> b -> t)
+getLens l = l @{MkIsLens strong} (id, const id)
+  where
+    Profunctor (\x,y => (x -> a, x -> b -> y)) where
+      dimap f g (get, set) = (get . f, (g .) . set . f)
+
+    [strong] GenStrong Pair (\x,y => (x -> a, x -> b -> y)) where
+      strongl (get, set) = (get . fst, \(a,c),b => (set a b, c))
+      strongr (get, set) = (get . snd, \(c,a),b => (c, set a b))
+
+public export
+withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
+withLens l f = uncurry f (getLens l)
+
+
+public export
+devoid : Lens Void Void a b
+devoid @{MkIsLens _} = dimap absurd snd . first
+
+public export
+united : Lens' a ()
+united @{MkIsLens _} = dimap ((),) snd . first
+
+
+
+public export
+fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
+fusing @{MkIsIso _} l = proextract . l . propure
diff --git a/src/Control/Lens/Optic.idr b/src/Control/Lens/Optic.idr
new file mode 100644
index 0000000..764c4a1
--- /dev/null
+++ b/src/Control/Lens/Optic.idr
@@ -0,0 +1,14 @@
+module Control.Lens.Optic
+
+import Data.Profunctor
+
+%default total
+
+
+public export
+Optic' : (p : Type -> Type -> Type) -> (s,t,a,b : Type) -> Type
+Optic' p s t a b = p a b -> p s t
+
+public export
+0 Optic : ((Type -> Type -> Type) -> Type) -> (s,t,a,b : Type) -> Type
+Optic constr s t a b = forall p. constr p => Optic' p s t a b