diff --git a/src/Control/Lens.idr b/src/Control/Lens.idr index d2970ef..80d1096 100644 --- a/src/Control/Lens.idr +++ b/src/Control/Lens.idr @@ -2,6 +2,7 @@ module Control.Lens import public Control.Lens.At import public Control.Lens.Cons +import public Control.Lens.Each import public Control.Lens.Equality import public Control.Lens.Fold import public Control.Lens.Getter diff --git a/src/Control/Lens/Each.idr b/src/Control/Lens/Each.idr new file mode 100644 index 0000000..3193db4 --- /dev/null +++ b/src/Control/Lens/Each.idr @@ -0,0 +1,34 @@ +module Control.Lens.Each + +import Control.Monad.Identity +import Control.Applicative.Const +import Control.Lens.Optic +import Control.Lens.Iso +import Control.Lens.Lens +import Control.Lens.Optional +import Control.Lens.Traversal + +%default total + + +||| An interface for accessing every element of a container. +||| +||| This can be thought of as a generalized version of `traversed` for +||| containers that do not have a `Traversable` implementation. +public export +interface Each s t a b | s where + + ||| Access every element of a container at the same time. + ||| + ||| This can be thought of as a generalized version of `traversed` for + ||| containers that do not have a `Traversable` implementation. + each : Traversal s t a b + + +public export +Each (Identity a) (Identity b) a b where + each = Id_ + +public export +Each (Const a b) (Const c d) a c where + each = Const_ diff --git a/src/Control/Lens/Iso.idr b/src/Control/Lens/Iso.idr index d2b5873..c8cd9e7 100644 --- a/src/Control/Lens/Iso.idr +++ b/src/Control/Lens/Iso.idr @@ -4,6 +4,8 @@ import Data.Maybe import Data.Contravariant import Data.Tensor import Data.Profunctor +import Control.Monad.Identity +import Control.Applicative.Const import Control.Lens.Optic import Control.Lens.Equality @@ -145,6 +147,15 @@ non : Eq a => a -> Iso' (Maybe a) a non x = iso (fromMaybe x) (\y => guard (x /= y) $> y) +public export +Id_ : Iso (Identity a) (Identity b) a b +Id_ = iso runIdentity Id + +public export +Const_ : Iso (Const a b) (Const c d) a c +Const_ = iso runConst MkConst + + -- Mapping ||| Lift an isomorphism through a `Functor`. diff --git a/src/Data/List/Lens.idr b/src/Data/List/Lens.idr index 483c95c..c8b9a82 100644 --- a/src/Data/List/Lens.idr +++ b/src/Data/List/Lens.idr @@ -75,3 +75,7 @@ Snoc (List a) (List b) a b where snoc_ = prism (uncurry snoc) (\case [] => Left [] x :: xs => Right $ unsnoc x xs) + +public export +Each (List a) (List b) a b where + each = traversed diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr index 74db5cb..fa0b9ca 100644 --- a/src/Data/Maybe/Lens.idr +++ b/src/Data/Maybe/Lens.idr @@ -26,3 +26,9 @@ infixl 9 .? public export (.?) : IsPrism p => Optic' p s t (Maybe a) (Maybe b) -> Optic' p a b a' b' -> Optic' p s t a' b' l .? l' = l . Just_ . l' + + +public export +Each (Maybe a) (Maybe b) a b where + -- each = Just_ + each = traversed diff --git a/src/Data/String/Lens.idr b/src/Data/String/Lens.idr index ee4aaf1..ee61913 100644 --- a/src/Data/String/Lens.idr +++ b/src/Data/String/Lens.idr @@ -55,3 +55,7 @@ public export Snoc String String Char Char where snocIso = iso unsnoc (maybe "" $ uncurry snoc) snoc_ = prism' (uncurry snoc) unsnoc + +public export +Each String String Char Char where + each = unpacked . traversed diff --git a/src/Data/Vect/Lens.idr b/src/Data/Vect/Lens.idr index f47ba31..9ff08e7 100644 --- a/src/Data/Vect/Lens.idr +++ b/src/Data/Vect/Lens.idr @@ -28,11 +28,6 @@ Ixed Nat a (Vect n a) where set (S n) (x :: xs) y = x :: set n xs y -public export -Ixed' Nat (Fin n) a (Vect n a) where - ix' n = lens (index n) (flip $ replaceAt n) - - public export cons_ : Iso (Vect (S n) a) (Vect (S n) b) (a, Vect n a) (b, Vect n b) cons_ = iso (\(x :: xs) => (x,xs)) (uncurry (::)) @@ -56,3 +51,12 @@ init_ = snoc_ . fst_ public export last_ : Lens' (Vect (S n) a) a last_ = snoc_ . snd_ + + +public export +Ixed' Nat (Fin n) a (Vect n a) where + ix' n = lens (index n) (flip $ replaceAt n) + +public export +Each (Vect n a) (Vect n b) a b where + each = traversed