toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Add documentation for indexed optics, etc.

Browse source
This commit is contained in:
Kiana Sheibani 2023-04-20 13:24:43 -04:00
parent 07b3028eda
commit 53df8dfced
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
14 changed files with 154 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/Control/Lens/At.idr
View file

@ -9,8 +9,12 @@ import Control.Lens.Setter
%default total
||| An interface that provides an `Optional` to access a given index in a
||| container, such as an ordinal position in a `List` or `Vect` or a key in a
||| map.
public export
interface Ixed i v a | a where
||| An optional that possibly accesses a value at a given index of a container.
ix : i -> Optional' a v
public export
@ -18,8 +22,14 @@ public export
ix k = optional' (Just . ($ k)) (\f,x,k' => if k == k' then x else f k')
||| An interface that provides a lens to access a given index in a collection.
||| This is different from `Ixed` in that the lens cannot fail to get a value.
|||
||| Implementations of this interface may use different index types for `ix` and
||| `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
||| An lens that infallibly accesses a value at a given index of a container.
ix' : i' -> Lens' a v
public export
@ -27,10 +37,27 @@ public export
ix' k = lens ($ k) (\f,x,k' => if k == k' then x else f k')
||| This interface provides a lens to read, write, add or delete the value
||| associated to a key in a map or map-like container.
|||
||| This lens must follow the law:
||| * `ix == at . Just_`
|||
||| If you do not need to add or delete keys, `ix` is more convenient.
public export
interface Ixed i v a => At i v a | a where
||| A lens that can be used to read, write, add or delete a value associated
||| with a key in a map-like container.
|||
||| If you do not need to add or delete keys, `ix` is more convenient.
at : i -> Lens' a (Maybe v)
||| Delete the value at a particular key in a container using `At`.
public export
sans : At i v a => i -> a -> a
sans k = at k .~ Nothing
||| Add a value at a particular key in a container using `At`.
public export
add : At i v a => i -> v -> a -> a
add k = (at k ?~)

43
src/Control/Lens/Fold.idr
View file

@ -42,6 +42,7 @@ public export
0 Fold : (s,a : Type) -> Type
Fold = Simple (Optic IsFold)
||| An indexed fold returns indices while getting.
public export
0 IndexedFold : (i,s,a : Type) -> Type
IndexedFold = Simple . IndexedOptic IsFold
@ -73,6 +74,7 @@ public export
folding : Foldable f => (s -> f a) -> Fold s a
folding @{_} f @{MkIsFold _} = rphantom . contramapFst f . wander traverse_
||| Construct an indexed fold from a function into a foldable container.
public export
ifolding : Foldable f => (s -> f (i, a)) -> IndexedFold i s a
ifolding @{_} f @{MkIsFold _} @{ind} =
@ -109,6 +111,8 @@ public export
foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m
foldMapOf l = runForget . l . MkForget
||| Map each focus of an optic to a monoid value with access to the index and
||| combine them.
public export
ifoldMapOf : Monoid m => IndexedFold i s a -> (i -> a -> m) -> s -> m
ifoldMapOf l = runForget . l @{%search} @{Idxed} . MkForget . uncurry
@ -119,6 +123,8 @@ public export
foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc
foldrOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup (.)} id} l
||| Combine the focuses of an optic using the provided function with access to
||| the index, starting from the right.
public export
ifoldrOf : IndexedFold i s a -> (i -> a -> acc -> acc) -> acc -> s -> acc
ifoldrOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup (.)} id} l
@ -129,6 +135,8 @@ public export
foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc
foldlOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . flip
||| Combine the focuses of an optic using the provided function with access to
||| the index, starting from the left.
public export
ifoldlOf : IndexedFold i s a -> (i -> acc -> a -> acc) -> acc -> s -> acc
ifoldlOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . (flip .)
@ -158,6 +166,8 @@ traverseOf_ l f =
let _ = MkMonoid @{MkSemigroup (*>)} (pure ())
in foldMapOf l (ignore . f)
||| Map each focus of an optic to a computation with access to the index,
||| evaluate those computations and discard the results.
public export
itraverseOf_ : Applicative f => IndexedFold i s a -> (i -> a -> f b) -> s -> f ()
itraverseOf_ l f =
@ -169,6 +179,7 @@ public export
forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f ()
forOf_ = flip . traverseOf_
||| A version of `itraverseOf_` with the arguments flipped.
public export
iforOf_ : Applicative f => IndexedFold i s a -> s -> (i -> a -> f b) -> f ()
iforOf_ = flip . itraverseOf_
@ -188,11 +199,21 @@ public export
allOf : Fold s a -> (a -> Bool) -> s -> Bool
allOf = foldMapOf @{All}
||| Return `True` if all focuses of the indexed optic satisfy the predicate.
public export
iallOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool
iallOf = ifoldMapOf @{All}
||| Return `True` if any focuses of the optic satisfy the predicate.
public export
anyOf : Fold s a -> (a -> Bool) -> s -> Bool
anyOf = foldMapOf @{Any}
||| Return `True` if any focuses of the indexed optic satisfy the predicate.
public export
ianyOf : IndexedFold i s a -> (i -> a -> Bool) -> s -> Bool
ianyOf = ifoldMapOf @{Any}
||| Return `True` if the element occurs in the focuses of the optic.
public export
@ -212,6 +233,10 @@ public export
firstOf : Fold s a -> s -> Maybe a
firstOf l = foldMapOf l Just
||| Access the first focus value and index of an indexed optic, returning Nothing
||| if there are no focuses.
|||
||| This is identical to `ipreview`.
public export
ifirstOf : IndexedFold i s a -> s -> Maybe (i, a)
ifirstOf l = runForget $ l @{%search} @{Idxed} $ MkForget Just
@ -222,6 +247,8 @@ public export
lastOf : Fold s a -> s -> Maybe a
lastOf l = foldMapOf @{MkMonoid @{MkSemigroup $ flip (<+>)} neutral} l Just
||| Access the last focus value and index of an indexed optic, returning Nothing
||| if there are no focuses.
public export
ilastOf : IndexedFold i s a -> s -> Maybe (i, a)
ilastOf l =
@ -271,12 +298,20 @@ public export
(^?) x l = preview l x
||| Access the first focus value and index of an indexed optic, returning Nothing
||| if there are no focuses.
|||
||| This is an alias for `ifirstOf`.
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.
|||
||| This is the operator form of `ipreview`.
public export
(^@?) : s -> IndexedFold i s a -> Maybe (i, a)
(^@?) x l = ipreview l x
@ -289,6 +324,10 @@ public export
pre : Fold s a -> OptionalFold s a
pre = folding . preview
||| Convert an `IndexedFold` into an `IndexedOptionalFold` that accesses the
||| first focus element.
|||
||| For the traversal version of this, see `isingular`.
public export
ipre : IndexedFold i s a -> IndexedOptionalFold i s a
ipre = ifolding . ipreview
@ -309,12 +348,16 @@ public export
(^..) s l = toListOf l s
||| Return a list of all focuses and indices of an indexed fold.
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`.
public export
(^@..) : s -> IndexedFold i s a -> List (i, a)
(^@..) x l = itoListOf l x

2
src/Control/Lens/Getter.idr
View file

@ -36,6 +36,7 @@ public export
0 Getter : (s,a : Type) -> Type
Getter = Simple (Optic IsGetter)
||| An indexed getter returns an index while getting.
public export
0 IndexedGetter : (i,s,a : Type) -> Type
IndexedGetter = Simple . IndexedOptic IsGetter
@ -51,6 +52,7 @@ public export
to : (s -> a) -> Getter s a
to f @{MkIsGetter _} = lmap f . rphantom
||| Construct an indexed getter from a function.
public export
ito : (s -> (i, a)) -> IndexedGetter i s a
ito f @{MkIsGetter _} @{ind} = lmap f . rphantom . indexed @{ind}

15
src/Control/Lens/Indexed.idr
View file

@ -83,7 +83,8 @@ indexedIso @{MkIsIso _} = MkIsIso %search
||| Compose two indexed optics, using a function to combine the indices of each
||| optic.
public export
icompose : IsIso p => (i -> j -> k) ->
IndexedOptic' p i s t a b -> IndexedOptic' (Indexed i p) j a b a' b' ->
@ -96,24 +97,36 @@ infixr 9 <.>
infixr 9 .>
infixr 9 <.
||| Compose two indexed optics, returning an optic indexed by a pair of indices.
|||
||| Mnemonically, the angle brackets point to the fact that we want to preserve
||| both indices.
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 (,)
||| Compose a non-indexed optic with an indexed optic.
|||
||| Mnemonically, the angle bracket points to the index that we want to preserve.
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'
||| Compose an indexed optic with a non-indexed optic.
|||
||| Mnemonically, the angle bracket points to the index that we want to preserve.
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}
||| Augment an optic with a constant index.
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}
||| Modify the indices of an indexed optic.
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}

12
src/Control/Lens/Lens.idr
View file

@ -53,10 +53,16 @@ public export
0 Lens' : (s,a : Type) -> Type
Lens' = Simple Lens
||| An indexed lens allows access to the index of a focus while setting it.
|||
||| Any indexed lens can be coerced into a regular lens and used in normal lens
||| functions, but there are also special functions that take indexed lenses
||| (i.e. `iover` instead of `over`).
public export
0 IndexedLens : (i,s,t,a,b : Type) -> Type
IndexedLens = IndexedOptic IsLens
||| `IndexedLens'` is the `Simple` version of `IndexedLens`.
public export
0 IndexedLens' : (i,s,a : Type) -> Type
IndexedLens' = Simple . IndexedLens
@ -76,16 +82,12 @@ public export
lens : (get : s -> a) -> (set : s -> b -> t) -> Lens s t a b
lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
||| Construct an indexed lens given getter and setter functions.
public export
ilens : (get : s -> (i, a)) -> (set : s -> b -> t) -> IndexedLens i s t a b
ilens get set @{_} @{ind} = lens get set . indexed @{ind}
public export
withIndex : i -> Lens s t a b -> IndexedLens i s t a b
withIndex i l @{MkIsLens _} @{ind} = l . lmap (i,) . indexed @{ind}
||| Extract getter and setter functions from a lens.
public export
getLens : Lens s t a b -> (s -> a, s -> b -> t)

4
src/Control/Lens/Optional.idr
View file

@ -43,10 +43,12 @@ public export
0 Optional' : (s,a : Type) -> Type
Optional' = Simple Optional
||| An `IndexedOptional` allows access to the index of a focus.
public export
0 IndexedOptional : (i,s,t,a,b : Type) -> Type
IndexedOptional = IndexedOptic IsOptional
||| `IndexedOptional'` is the `Simple` version of `IndexedOptional`.
public export
0 IndexedOptional' : (i,s,a : Type) -> Type
IndexedOptional' = Simple . IndexedOptional
@ -74,10 +76,12 @@ public export
optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b
optional' prj = optional (\x => maybe (Left x) Right (prj x))
||| Construct an indexed optional from a projection and a setter function.
public export
ioptional : (s -> Either t (i, a)) -> (s -> b -> t) -> IndexedOptional i s t a b
ioptional prj set @{_} @{ind} = optional prj set . indexed @{ind}
||| Construct a simple indexed optional from a projection and a setter function.
public export
ioptional' : (s -> Maybe (i, a)) -> (s -> b -> s) -> IndexedOptional i s s a b
ioptional' prj = ioptional (\x => maybe (Left x) Right (prj x))

2
src/Control/Lens/OptionalFold.idr
View file

@ -40,6 +40,7 @@ public export
0 OptionalFold : (s,a : Type) -> Type
OptionalFold = Simple (Optic IsOptFold)
||| An `IndexedOptionalFold` returns an index while getting.
public export
0 IndexedOptionalFold : (i,s,a : Type) -> Type
IndexedOptionalFold = Simple . IndexedOptic IsOptFold
@ -56,6 +57,7 @@ folding : (s -> Maybe a) -> OptionalFold s a
folding f @{MkIsOptFold _} =
contrabimap (\x => maybe (Left x) Right (f x)) Left . right
||| Construct an `IndexedOptionalFold` from a function.
public export
ifolding : (s -> Maybe (i, a)) -> IndexedOptionalFold i s a
ifolding f @{MkIsOptFold _} @{ind} =

13
src/Control/Lens/Setter.idr
View file

@ -49,10 +49,12 @@ public export
0 Setter' : (s,a : Type) -> Type
Setter' = Simple Setter
||| An indexed setter allows access to an index while setting.
public export
0 IndexedSetter : (i,s,t,a,b : Type) -> Type
IndexedSetter = IndexedOptic IsSetter
||| `IndexedSetter'` is the `Simple` version of `IndexedSetter`.
public export
0 IndexedSetter' : (i,s,a : Type) -> Type
IndexedSetter' = Simple . IndexedSetter
@ -68,6 +70,7 @@ public export
sets : ((a -> b) -> s -> t) -> Setter s t a b
sets f @{MkIsSetter _} = roam f
||| Construct an indexed setter from a modifying function.
public export
isets : ((i -> a -> b) -> s -> t) -> IndexedSetter i s t a b
isets f @{MkIsSetter _} @{ind} = roam (f . curry) . indexed @{ind}
@ -98,12 +101,16 @@ public export
(%~) = over
||| Modify the focus or focuses of an indexed optic, having access to the index.
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`.
public export
(%@~) : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
(%@~) = iover
@ -124,12 +131,16 @@ public export
(.~) = set
||| Set the focus or focuses of an indexed optic, having access to the index.
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`.
public export
(.@~) : IndexedSetter i s t a b -> (i -> b) -> s -> t
(.@~) = iset
@ -215,6 +226,7 @@ public export
(%=) : MonadState s m => Setter s s a b -> (a -> b) -> m ()
(%=) = modify .: over
||| Modify the focus of an optic within a state monad, having access to the index.
public export
(%@=) : MonadState s m => IndexedSetter i s s a b -> (i -> a -> b) -> m ()
(%@=) = modify .: iover
@ -224,6 +236,7 @@ public export
(.=) : MonadState s m => Setter s s a b -> b -> m ()
(.=) = modify .: set
||| Set the focus of an optic within a state monad, having access to the index.
public export
(.@=) : MonadState s m => IndexedSetter i s s a b -> (i -> b) -> m ()
(.@=) = modify .: iset

28
src/Control/Lens/Traversal.idr
View file

@ -44,10 +44,13 @@ public export
0 Traversal' : (s,a : Type) -> Type
Traversal' = Simple Traversal
||| An indexed traversal allows access to the indices of the values as they are
||| being modified.
public export
0 IndexedTraversal : (i,s,t,a,b : Type) -> Type
IndexedTraversal = IndexedOptic IsTraversal
||| `IndexedTraversal'` is the `Simple` version of `IndexedTraversal`.
public export
0 IndexedTraversal' : (i,s,a : Type) -> Type
IndexedTraversal' = Simple . IndexedTraversal
@ -58,6 +61,8 @@ IndexedTraversal' = Simple . IndexedTraversal
------------------------------------------------------------------------------
||| Convert a traversal into an indexed traversal, adding an index for the
||| ordinal position of the focus.
public export
iordinal : Num i => Traversal s t a b -> IndexedTraversal i s t a b
iordinal @{_} l @{MkIsTraversal _} @{ind} = wander (func . curry) . indexed @{ind}
@ -71,6 +76,7 @@ public export
traversed : Traversable t => Traversal (t a) (t b) a b
traversed @{_} @{MkIsTraversal _} = traverse'
||| Derive an indexed traversal from a `Traversable` implementation.
public export
itraversed : Num i => Traversable t => IndexedTraversal i (t a) (t b) a b
itraversed = iordinal traversed
@ -96,6 +102,8 @@ public export
traverseOf : Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t
traverseOf l = applyStar . l . MkStar {f}
||| Map each focus of a traversal to a computation with acces to the index,
||| evaluate those computations and combine the results.
public export
itraverseOf : Applicative f => IndexedTraversal i s t a b -> (i -> a -> f b) -> s -> f t
itraverseOf l = traverseOf (l @{%search} @{Idxed}) . uncurry
@ -105,6 +113,7 @@ public export
forOf : Applicative f => Traversal s t a b -> s -> (a -> f b) -> f t
forOf = flip . traverseOf
||| A version of `itraverseOf` but with the arguments flipped.
public export
iforOf : Applicative f => IndexedTraversal i s t a b -> s -> (i -> a -> f b) -> f t
iforOf = flip . itraverseOf
@ -161,6 +170,7 @@ failover l f x =
(b, y) = traverseOf l ((True,) . f) x
in guard b $> y
||| Try to map over an indexed traversal, failing if the traversal has no focuses.
public export
ifailover : Alternative f => IndexedTraversal i s t a b -> (i -> a -> b) -> s -> f t
ifailover l = failover (l @{%search} @{Idxed}) . uncurry
@ -181,6 +191,12 @@ partsOf : Traversal s t a a -> Lens s t (List a) (List a)
partsOf l = lens (runForget $ l $ MkForget pure)
(flip evalState . traverseOf l partsOf_update)
||| Convert an indexed traversal into an indexed lens over a list of values, with
||| access to a list of indices.
|||
||| Note that this is only a true lens if the invariant of the list's length is
||| maintained. You should avoid mapping `over` this lens with a function that
||| changes the list's length.
public export
ipartsOf : IndexedTraversal i s t a a -> IndexedLens (List i) s t (List a) (List a)
ipartsOf l = ilens (unzip . (runForget $ l @{%search} @{Idxed} $ MkForget pure))
@ -198,6 +214,18 @@ singular l = optional' (runForget $ l (MkForget Just)) set
set str x = evalState True $ traverseOf l
(\y => if !get then put False $> x else pure y) str
||| Construct an indexed optional that focuses on the first value of an
||| indexed traversal.
|||
||| For the fold version of this, see `ipre`.
public export
isingular : IndexedTraversal' i s a -> IndexedOptional' i s a
isingular l = ioptional' (runForget $ l @{%search} @{Idxed} (MkForget Just)) set
where
set : s -> a -> s
set str x = evalState True $ itraverseOf l
(\_,y => if !get then put False $> x else pure y) str
||| Filter the focuses of a traversal by a predicate on their ordinal positions.
public export
elementsOf : Traversal s t a a -> (Nat -> Bool) -> Traversal s t a a

2
src/Data/Either/Lens.idr
View file

@ -6,10 +6,12 @@ import public Control.Lens
%default total
||| A prism to the left of an `Either`.
public export
Left_ : Prism (Either a c) (Either b c) a b
Left_ @{MkIsPrism _} = left
||| A prism to the right of an `Either`.
public export
Right_ : Prism (Either c a) (Either c b) a b
Right_ @{MkIsPrism _} = right

3
src/Data/List/Lens.idr
View file

@ -29,15 +29,18 @@ stripSuffix qs xs0 = go xs0 zs
go [] _ = Nothing
||| A prism that strips a prefix from a list of values.
public export
prefixed : Eq a => List a -> Prism' (List a) (List a)
prefixed xs = prism' (xs ++) (stripPrefix xs)
||| A prism that strips a suffix from a list of values.
public export
suffixed : Eq a => List a -> Prism' (List a) (List a)
suffixed xs = prism' (++ xs) (stripSuffix xs)
||| An isomorphism between a list and its reverse.
public export
reversed : Iso (List a) (List b) (List a) (List b)
reversed = iso reverse reverse

4
src/Data/Maybe/Lens.idr
View file

@ -7,10 +7,12 @@ import public Control.Lens
%default total
||| A prism of the `Nothing` case of a `Maybe`.
public export
Nothing_ : Prism' (Maybe a) ()
Nothing_ = prism' (const Nothing) (guard . isNothing)
||| A prism of the `Just` case of a `Maybe`.
public export
Just_ : Prism (Maybe a) (Maybe b) a b
Just_ = prism Just $ \case
@ -19,6 +21,8 @@ Just_ = prism Just $ \case
infixl 9 .?
||| The composition `l .? l'` is equivalent to `l . Just_ . l'`.
||| Useful for optics who focus type is a `Maybe`, such as `at`.
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'

4
src/Data/Tuple/Lens.idr
View file

@ -7,19 +7,23 @@ import public Control.Lens
%default total
||| A lens to the first element of a pair.
public export
fst_ : Lens (a, c) (b, c) a b
fst_ @{MkIsLens _} = first
||| A lens to the second element of a pair.
public export
snd_ : Lens (c, a) (c, b) a b
snd_ @{MkIsLens _} = second
||| An indexed lens to the first element of a pair, indexed by the other element.
public export
ifst_ : IndexedLens i (a, i) (b, i) a b
ifst_ = ilens swap (flip $ mapFst . const)
||| An indexed lens to the second element of a pair, indexed by the other element.
public export
isnd_ : IndexedLens i (i, a) (i, b) a b
isnd_ = ilens id (flip $ mapSnd . const)

1
src/Data/Vect/Lens.idr
View file

@ -6,6 +6,7 @@ import Control.Lens
%default total
||| An isomorphism between a `Vect` and its reverse.
public export
reversed : Iso (Vect n a) (Vect n b) (Vect n a) (Vect n b)
reversed = iso reverse reverse