Add Each interface

This commit is contained in:
Kiana Sheibani 2023-04-25 13:40:03 -04:00
parent 810404b305
commit 4c19ed5209
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
7 changed files with 69 additions and 5 deletions

View file

@ -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

34
src/Control/Lens/Each.idr Normal file
View file

@ -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_

View file

@ -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`.

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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