diff --git a/README.md b/README.md index fea32fe..ea93c9d 100644 --- a/README.md +++ b/README.md @@ -3,14 +3,10 @@ This package provides utilities for working with lenses, prisms, traversals, and other optics in Idris. This library uses *profunctor optics*. -## Comparison to Monocle +Eventually, this library will also include elaboration scripts to automatically +generate lenses for a particular datatype. -[Monocle](https://github.com/stefan-hoeck/idris2-monocle) is another Idris 2 library -for lenses. That library represents lenses using a datatype, which is often less -efficient at run-time, but results in better error messages and is generally -simpler to understand. - -## Comparisons to Non-Idris Libraries +## Comparisons This library is inspired by the Haskell libraries [lens](https://hackage.haskell.org/package/lens-5.2.2), [optics](https://hackage.haskell.org/package/optics) and [fresnel](https://hackage.haskell.org/package/fresnel), @@ -50,7 +46,3 @@ Or you can install using [pack](https://github.com/stefan-hoeck/idris2-pack): pack install lens ``` -## Thanks - -Special thanks to [Stefan Höck](https://github.com/stefan-hoeck) for assistance -with writing elaboration scripts. diff --git a/lens.ipkg b/lens.ipkg index d9dc720..386b8b5 100644 --- a/lens.ipkg +++ b/lens.ipkg @@ -1,5 +1,5 @@ package lens -version = 0.3.0 +version = 0.2.0 brief = "Batteries-included profunctor optics" diff --git a/src/Control/Lens/At.idr b/src/Control/Lens/At.idr index 3d5bdd6..30e6dc4 100644 --- a/src/Control/Lens/At.idr +++ b/src/Control/Lens/At.idr @@ -37,7 +37,7 @@ public export ||| `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`. public export interface Ixed i v a => Ixed' i i' v a | a where - ||| A lens that infallibly accesses a value at a given index of a container. + ||| An lens that infallibly accesses a value at a given index of a container. ix' : i' -> Lens' a v ||| An indexed version of `ix'`. diff --git a/src/Control/Lens/Fold.idr b/src/Control/Lens/Fold.idr index e98c9ac..e9f9dff 100644 --- a/src/Control/Lens/Fold.idr +++ b/src/Control/Lens/Fold.idr @@ -218,7 +218,7 @@ ianyOf = ifoldMapOf @{Any} ||| Return `True` if the element occurs in the focuses of the optic. public export elemOf : Eq a => Fold s a -> a -> s -> Bool -elemOf l = anyOf l . (==) +elemOf l = allOf l . (==) ||| Calculate the number of focuses of the optic. public export @@ -287,7 +287,7 @@ public export preview : Fold s a -> s -> Maybe a preview = firstOf -export infixl 8 ^?, ^@?, ^., ^@. +infixl 8 ^? ||| Access the first focus value of an optic, returning `Nothing` if there are ||| no focuses. @@ -306,6 +306,8 @@ public export ipreview : IndexedFold i s a -> s -> Maybe (i, a) ipreview = ifirstOf +infixl 8 ^@? + ||| Access the first focus value and index of an indexed optic, returning Nothing ||| if there are no focuses. ||| @@ -336,6 +338,8 @@ public export toListOf : Fold s a -> s -> List a toListOf l = foldrOf l (::) [] +infixl 8 ^.. + ||| Return a list of all focuses of a fold. ||| ||| This is the operator form of `toListOf`. @@ -349,6 +353,8 @@ public export itoListOf : IndexedFold i s a -> s -> List (i, a) itoListOf l = ifoldrOf l ((::) .: (,)) [] +infixl 8 ^@.. + ||| Return a list of all focuses and indices of an indexed fold. ||| ||| This is the operator form of `itoListOf`. diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr index bdaaf04..6b57f21 100644 --- a/src/Control/Lens/Getter.idr +++ b/src/Control/Lens/Getter.idr @@ -85,7 +85,8 @@ iview : IndexedGetter i s a -> s -> (i, a) iview l = runForget $ l @{%search} @{Idxed} $ MkForget id -export infixl 8 ^., ^@. +infixl 8 ^. +infixl 8 ^@. ||| Access the focus value of an optic, particularly a `Getter`. ||| diff --git a/src/Control/Lens/Indexed.idr b/src/Control/Lens/Indexed.idr index a558a63..c48214c 100644 --- a/src/Control/Lens/Indexed.idr +++ b/src/Control/Lens/Indexed.idr @@ -93,7 +93,9 @@ icompose @{MkIsIso _} f l l' @{ind} = l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p} . lmap (mapFst (uncurry f) . assocl) . indexed @{ind} -export infixr 9 <.>, .>, <. +infixr 9 <.> +infixr 9 .> +infixr 9 <. ||| Compose two indexed optics, returning an optic indexed by a pair of indices. ||| diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr index d702d3b..648dbad 100644 --- a/src/Control/Lens/Lens.idr +++ b/src/Control/Lens/Lens.idr @@ -139,15 +139,22 @@ fusing @{MkIsIso _} l = proextract . l . propure -- Operators ------------------------------------------------------------------------------ -export infixr 4 %%~, %%=, %%@~, %%@= +infixr 4 %%~; infix 4 %%=; infix 4 %%@~; infix 4 %%@= -export infixr 4 <%~, <%@~, <+~, <*~, <-~, ~ -export infixr 4 <<%~, <<%@~, <<.~, <~ +infixr 4 <%~; infixr 4 <%@~; infixr 4 <+~; infixr 4 <*~; infixr 4 <-~ +infixr 4 ~ -export infix 4 <%=, <%@=, <+=, <*=, <-=, = -export infix 4 <<%=, <<%@=, <<.=, <= +infixr 4 <<%~; infixr 4 <<%@~; infixr 4 <<.~; infixr 4 <~ -export infixr 1 <<<~ +infix 4 <%=; infix 4 <%@=; infix 4 <+=; infix 4 <*=; infix 4 <-=; infix 4 = + +infix 4 <<%=; infix 4 <<%@=; infix 4 <<.=; infix 4 <= + +infixr 2 <<~ public export @@ -396,8 +403,11 @@ public export ||| Run a monadic action and set the focus of an optic in state to the result. -||| This is different from `(<~)` and `(<<~)` in that it also passes though -||| the old value of the optic. +||| This is different from `(<~)` in that it also passes though the output of +||| the action. public export -(<<<~) : MonadState s m => Lens s s a b -> m b -> m a -(<<<~) l m = l <<.= !m +(<<~) : MonadState s m => Lens s s a b -> m b -> m b +(<<~) l x = do + v <- x + modify $ l @{MkIsLens Function} (const v) + pure v diff --git a/src/Control/Lens/Review.idr b/src/Control/Lens/Review.idr index c49e9c0..0f03544 100644 --- a/src/Control/Lens/Review.idr +++ b/src/Control/Lens/Review.idr @@ -66,7 +66,7 @@ public export review : Review s a -> a -> s review l = reviews l id -export infixr 8 ^$ +infixr 8 ^$ ||| Turn an optic around to inject a focus value into the larger data structure. ||| This function takes a `Review`, which can also be a `Prism` or `Iso`. diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr index 10eabbc..068e411 100644 --- a/src/Control/Lens/Setter.idr +++ b/src/Control/Lens/Setter.idr @@ -91,7 +91,7 @@ public export over : Setter s t a b -> (a -> b) -> s -> t over l = l @{MkIsSetter Function} -export infixr 4 %~, %@~, .~, .@~ +infixr 4 %~ ||| Modify the focus or focuses of an optic. ||| @@ -106,6 +106,8 @@ public export iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t iover l = l @{MkIsSetter Function} @{Idxed} . uncurry +infixr 4 %@~ + ||| Modify the focus or focuses of an indexed optic, having access to the index. ||| ||| This is the operator form of `iover`. @@ -119,6 +121,8 @@ public export set : Setter s t a b -> b -> s -> t set l = over l . const +infixr 4 .~ + ||| Set the focus or focuses of an optic to a constant value. ||| ||| This is the operator form of `set`. @@ -132,6 +136,8 @@ public export iset : IndexedSetter i s t a b -> (i -> b) -> s -> t iset l = iover l . (const .) +infix 4 .@~ + ||| Set the focus or focuses of an indexed optic, having access to the index. ||| ||| This is the operator form of `iset`. @@ -144,9 +150,13 @@ public export -- More operators ------------------------------------------------------------------------------ -export infixr 4 ?~, <.~, ~ -export infix 4 %=, %@=, .=, .@=, ?=, <.=, = -export infix 1 <~, <<~ +infixr 4 ?~; infixr 4 <.~; infixr 4 ~ + +infix 4 %=; infix 4 %@=; infix 4 .=; infix 4 .@=; infix 4 ?=; infix 4 <.= +infix 4 = + ||| Set the focus of an optic to `Just` a value. public export @@ -237,12 +247,12 @@ public export ||| Set within a state monad with pass-through. public export (<.=) : MonadState s m => Setter s s a b -> b -> m b -(<.=) l x = (l .= x) $> x +(<.=) l x = (l .= x) >> pure x ||| Set to `Just` a value within a state monad with pass-through. public export ( Setter s s a (Maybe b) -> b -> m b -( x +(> pure x ||| Add a constant value to the focus of an optic within a state monad. public export @@ -293,11 +303,4 @@ public export ||| variable. public export (<~) : MonadState s m => Setter s s a b -> m b -> m () -(<~) l m = l .= !m - -||| Run a monadic action and set the focus of an optic in state to the result. -||| This is different from `(<~)` in that it also passes though the output of -||| the action. -public export -(<<~) : MonadState s m => Setter s s a b -> m b -> m b -(<<~) l m = l <.= !m +(<~) l m = m >>= (l .=) diff --git a/src/Control/Lens/Traversal.idr b/src/Control/Lens/Traversal.idr index 2b25502..2fc57ac 100644 --- a/src/Control/Lens/Traversal.idr +++ b/src/Control/Lens/Traversal.idr @@ -188,7 +188,7 @@ ifailover l = failover (l @{%search} @{Idxed}) . uncurry partsOf_update : a -> State (List a) a partsOf_update x = get >>= \case - x' :: xs' => put xs' $> x' + x' :: xs' => put xs' >> pure x' [] => pure x ||| Convert a traversal into a lens over a list of values. @@ -263,12 +263,12 @@ element : Traversable t => Nat -> Optional' (t a) a element = elementOf traversed -||| Limit a traversal to its first `n` focuses. +||| Limit a traversal to its first n focuses. public export taking : Nat -> Traversal s t a a -> Traversal s t a a taking n l = elementsOf l (< n) -||| Remove the first `n` focuses from a traversal. +||| Remove the first n focuses from a traversal. public export dropping : Nat -> Traversal s t a a -> Traversal s t a a -dropping n l = elementsOf l (>= n) +dropping i l = elementsOf l (>= i) diff --git a/src/Control/Zipper.idr b/src/Control/Zipper.idr index d293fb3..d6c450a 100644 --- a/src/Control/Zipper.idr +++ b/src/Control/Zipper.idr @@ -27,7 +27,7 @@ fromPointer k x (l, r) = l <>> (k,x) :: r ------------------------------------------------------------------------------ -export infix 9 @> +infix 9 @> ||| A simple type that represents a layer of the zipper as it moves downwards. ||| diff --git a/src/Data/List1/Lens.idr b/src/Data/List1/Lens.idr deleted file mode 100644 index 70a9d49..0000000 --- a/src/Data/List1/Lens.idr +++ /dev/null @@ -1,51 +0,0 @@ -module Data.List1.Lens - -import Data.List1 -import Data.Profunctor -import public Control.Lens -import Data.Tuple.Lens - -%default total - -||| An isomorphism between a list and its reverse. -public export -reversed : Iso (List1 a) (List1 b) (List1 a) (List1 b) -reversed = iso reverse reverse - - -public export -cons_ : Iso (List1 a) (List1 b) (a, List a) (b, List b) -cons_ = iso (\(x:::xs) => (x,xs)) (uncurry (:::)) - -public export -head_ : Lens' (List1 a) a -head_ = cons_ . fst_ - -public export -tail_ : Lens' (List1 a) (List a) -tail_ = cons_ . snd_ - -public export -snoc_ : Iso (List1 a) (List1 b) (List a, a) (List b, b) -snoc_ = iso unsnoc (uncurry lappend . mapSnd singleton) - -public export -init_ : Lens' (List1 a) (List a) -init_ = snoc_ . fst_ - -public export -last_ : Lens' (List1 a) a -last_ = snoc_ . snd_ - - -public export -Ixed Nat a (List1 a) where - ix = element - -public export -Each (List1 a) (List1 b) a b where - each = traversed - -public export -Num i => IEach i (List1 a) (List1 b) a b where - ieach = itraversed diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr index 67a754f..9f0eaad 100644 --- a/src/Data/Maybe/Lens.idr +++ b/src/Data/Maybe/Lens.idr @@ -19,7 +19,7 @@ Just_ = prism Just $ \case Nothing => Left Nothing Just x => Right x -export infixl 9 .? +infixl 9 .? ||| The composition `l .? l'` is equivalent to `l . Just_ . l'`. ||| Useful for optics whose focus type is a `Maybe`, such as `at`. diff --git a/src/Derive/Lens.idr b/src/Derive/Lens.idr index 250e331..cd2bbd6 100644 --- a/src/Derive/Lens.idr +++ b/src/Derive/Lens.idr @@ -5,11 +5,6 @@ import public Language.Reflection.Util %default total -toField : Name -> Name -toField (NS ns nm) = NS ns (toField nm) -toField (UN (Basic nm)) = UN (Field nm) -toField nm = nm - parameters (o : LensOptions) lname : Name -> Name lname n = UN $ Basic (o.fieldName $ nameStr n) @@ -22,7 +17,7 @@ parameters (o : LensOptions) ldef : BoundArg 0 RegularNamed -> Decl ldef (BA x _ _) = - let fld := toField $ argName x + let fld := argName x nme := lname fld u := update [ISetField [nameStr fld] `(y)] `(x) in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]