ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Lens

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

4 types
21 values

PackageAgda-2.8.0.2
Exports26
LanguageHaskell2010
LicenceMIT
SourceLens.hs

value(%%=) :: MonadState o m => Lens' o i -> (i -> m (i, r)) -> m r

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

value(%=) :: MonadState o m => Lens' o i -> (i -> i) -> m ()

Modify a part of the state.

value(%==) :: MonadState o m => Lens' o i -> (i -> m i) -> m ()

Modify a part of the state monadically.

value(.=) :: MonadState o m => Lens' o i -> i -> m ()

Write a part of the state.

value(^.) :: o -> Lens' o i -> i

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

valuecontains :: Ord k => k -> Lens' (Set k) Bool

Focus on given element in a set.

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

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

valueiso :: (o -> i) -> (i -> o) -> Lens' o i

Build a lens out of an isomorphism.

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

Access a map value at a given key.

valuelFst :: Functor f => (a -> f a) -> (a, b) -> f (a, b)

valuelSnd :: Functor f => (b -> f b) -> (a, b) -> f (a, b)

valuelens :: LensGet o i -> LensSet o i -> Lens' o i

Build a lens from a getter and a setter.

valuelensProduct :: Lens' s a -> Lens' s b -> Lens' s (a, b)

Only sound if the lenses are disjoint!

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

Modify a part of the state in a subcomputation.

valuelocally' :: ((o -> o) -> m a -> m a) -> Lens' o i -> (i -> i) -> m a -> m a

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

Modify a part of the state locally.

valueover :: Lens' o i -> LensMap o i

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

valueset :: Lens' o i -> LensSet o i

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

valueuse :: MonadState o m => Lens' o i -> m i

Read a part of the state.

valueview :: MonadReader o m => Lens' o i -> m i

Ask for part of read-only state.

typetype Lens' o i = forall (f :: Type -> Type). Functor f => (i -> f i) -> o -> f o

Van Laarhoven style homogeneous lenses. Mnemoic: "Lens outer inner", same type argument order as 'get :: o -> i'.

typetype LensGet o i = o -> i

typetype LensMap o i = (i -> i) -> o -> o

typetype LensSet o i = i -> o -> o

value(<&>) :: Functor f => f a -> (a -> b) -> f b

Flipped version of <$>.

(<&>) = flip fmap

Examples

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

Example1 expression

>>> Just 2 <&> (+1)Just 3

Example1 expression

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

Example1 expression

>>> Right 3 <&> (+1)Right 4

method(&&&) :: a b c -> a b c' -> a b (c, c')

Fanout: send the input to both argument arrows and combine their output.

The default definition may be overridden with a more efficient version if desired.

    ╭───────╮ c
  b │ ┌─ f ─┼───>
>───┼─┤     │
    │ └─ g ─┼───>
    ╰───────╯ c'