Agda-2.5.4: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Lens

Description

A cut-down implementation of lenses, with names taken from Edward Kmett's lens package.

Synopsis

Documentation

type LensMap i o = (i -> i) -> o -> o #

type LensSet i o = i -> o -> o #

type LensGet i o = o -> i #

type Lens' i o = forall f. Functor f => (i -> f i) -> o -> f o #

Van Laarhoven style homogeneous lenses. Mnemoic: "Lens inner outer".

lFst :: Lens' a (a, b) #

lSnd :: Lens' b (a, b) #

(^.) :: o -> Lens' i o -> i infixl 8 #

Get inner part i of structure o as designated by Lens' i o.

set :: Lens' i o -> LensSet i o #

Set inner part i of structure o as designated by Lens' i o.

over :: Lens' i o -> LensMap i o #

Modify inner part i of structure o using a function i -> i.

focus :: Monad m => Lens' i o -> StateT i m a -> StateT o m a #

Focus on a part of the state for a stateful computation.

use :: MonadState o m => Lens' i o -> m i #

Read a part of the state.

(.=) :: MonadState o m => Lens' i o -> i -> m () infix 4 #

Write a part of the state.

(%=) :: MonadState o m => Lens' i o -> (i -> i) -> m () infix 4 #

Modify a part of the state.

(%==) :: MonadState o m => Lens' i o -> (i -> m i) -> m () infix 4 #

Modify a part of the state monadically.

(%%=) :: MonadState o m => Lens' i o -> (i -> m (i, r)) -> m r infix 4 #

Modify a part of the state monadically, and return some result.

locallyState :: MonadState o m => Lens' i o -> (i -> i) -> m r -> m r #

Modify a part of the state locally.

view :: MonadReader o m => Lens' i o -> m i #

Ask for part of read-only state.

locally :: MonadReader o m => Lens' i o -> (i -> i) -> m a -> m a #

Modify a part of the state in a subcomputation.

locally' :: ((o -> o) -> m a -> m a) -> Lens' i o -> (i -> i) -> m a -> m a #

key :: Ord k => k -> Lens' (Maybe v) (Map k v) #

(<&>) :: Functor f => f a -> (a -> b) -> f b infixl 1 #

Flipped version of <$>.

(<&>) = flip fmap

Examples

Expand

Apply (+1) to a list, a Just and a Right:

>>> Just 2 <&> (+1)
Just 3
>>> [1,2,3] <&> (+1)
[2,3,4]
>>> Right 3 <&> (+1)
Right 4

Since: base-4.11.0.0