Agda.Utils.Lens

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

Documentation

type Lens' o i = forall f. 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'.

type LensGet o i = o -> i

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

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

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

Access a map value at a given key.

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

Write a part of the state.

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

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

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

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

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

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

lFst :: Lens' (a, b) a

lSnd :: Lens' (a, b) b

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

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

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

Read a part of the state.

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

Modify a part of the state.

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

Modify a part of the state monadically.

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

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

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

Modify a part of the state locally.

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

Ask for part of read-only state.

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

Modify a part of the state in a subcomputation.

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

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

Focus on given element in a set.

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

Infix version of for.