Control.Lens.Lens

Definitions

record IsLens : (Type -> Type -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsLens : Strong p -> IsLens p

Projection: 

.runIsLens : IsLens p -> Strong p

Hints:

IsLens p => IsIso p

IsGetter p => IsLens p

IsOptional p => IsLens p

IsLens p => IsLens (Indexed i p)

.runIsLens : IsLens p -> Strong p

Totality: total
Visibility: public export

runIsLens : IsLens p -> Strong p

Totality: total
Visibility: public export

lensToIso : IsLens p => IsIso p

Totality: total
Visibility: export

indexedLens : IsLens p => IsLens (Indexed i p)

Totality: total
Visibility: export

0 Lens : Type -> Type -> Type -> Type -> Type

  A *lens* is a functional reference to a value within a larger data structure.
  Lenses allow one to access or modify the value that they reference, called
  the "focus" or "focus element".
  
  For example, the lens `fst_` from `Data.Tuple.Lens` focuses on the first
  element of a pair. It has the type:
  
  ```idris
  fst_ : Lens (a, c) (b, c) a b
  ```
  
  The types `s, t` correspond to the type of the outside data structure, and
  `a, b` correspond to the type of the focus element. Two of each type is
  provided to allow for operations that change the type of the focus.

Totality: total
Visibility: public export

0 Lens' : Type -> Type -> Type

  `Lens'` is the `Simple` version of `Lens`.

Totality: total
Visibility: public export

0 IndexedLens : Type -> Type -> Type -> Type -> Type -> Type

  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`).

Totality: total
Visibility: public export

0 IndexedLens' : Type -> Type -> Type -> Type

  `IndexedLens'` is the `Simple` version of `IndexedLens`.

Totality: total
Visibility: public export

lens : (s -> a) -> (s -> b -> t) -> Lens s t a b

  Construct a lens given getter and setter functions.
  
  @ get The getter function
  @ set The setter function, where the first argument is the data structure
  to modify and the second argument is the new focus value

Totality: total
Visibility: public export

ilens : (s -> (i, a)) -> (s -> b -> t) -> IndexedLens i s t a b

  Construct an indexed lens given getter and setter functions.

Totality: total
Visibility: public export

getLens : Lens s t a b -> (s -> a, s -> b -> t)

  Extract getter and setter functions from a lens.

Totality: total
Visibility: public export

withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r

  Extract getter and setter functions from a lens.

Totality: total
Visibility: public export

devoid : IndexedLens i Void t a b

  `Void` vacuously "contains" a value of any other type.

Totality: total
Visibility: public export

united : Lens' a ()

  All values contain a unit.

Totality: total
Visibility: public export

alongside : Lens s t a b -> Lens s' t' a' b' -> Lens (s, s') (t, t') (a, a') (b, b')

  Create a lens that operates on pairs from two other lenses.

Totality: total
Visibility: public export

fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b

  Optimize a composition of optics by fusing their uses of `dimap` into one.
  
  This function exploits the Yoneda lemma. `fusing (a . b)` is essentially
  equivalent to `a . b`, but the former will only call `dimap` once.

Totality: total
Visibility: public export

(%%~) : Functor f => Lens s t a b -> (a -> f b) -> s -> f t

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(%%=) : MonadState s m => Lens s s a b -> (a -> (r, b)) -> m r

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(%%@~) : Functor f => IndexedLens i s t a b -> (i -> a -> f b) -> s -> f t

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(%%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> (r, b)) -> m r

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<%~) : Lens s t a b -> (a -> b) -> s -> (b, t)

  Modify a value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<%@~) : IndexedLens i s t a b -> (i -> a -> b) -> s -> (b, t)

  Modify a value with pass-through, having access to the index.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<+~) : Num a => Lens s t a a -> a -> s -> (a, t)

  Add a value to the lens with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<*~) : Num a => Lens s t a a -> a -> s -> (a, t)

  Multiply the lens by a value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)

  Subtract a value from the lens with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)

  Divide the lens by a value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)

  Logically OR the lens with a constant value with pass-through.
  
  Like (||) and (||~), this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)

  Logically AND the lens with a constant value with pass-through.
  
  Like (&&) and (&&~), this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)

  Modify an lens's focus with the semigroup/monoid operator with pass-through.
  
  The constant value is applied to the focus from the right:
  ```
  l <<+>~ x = l <%~ (<+> x)
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<%~) : Lens s t a b -> (a -> b) -> s -> (a, t)

  Modify the value of a lens and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<.~) : Lens s t a b -> b -> s -> (a, t)

  Set the value of a lens and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<?~) : Lens s t a (Maybe b) -> b -> s -> (a, t)

  Set a lens to `Just` a value and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<+~) : Num a => Lens s t a a -> a -> s -> (a, t)

  Add a constant value to a lens's focus and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<*~) : Num a => Lens s t a a -> a -> s -> (a, t)

  Multiply a lens's focus by a constant value and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)

  Subtract a constant value from a lens's focus and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)

  Divide a lens's focus by a constant value and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)

  Logically OR a lens's focus by a constant value and return the old value.
  
  Like (||) and (||~), this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)

  Logically AND a lens's focus by a constant value and return the old value.
  
  Like (&&) and (&&~), this operator takes a lazy second argument.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)

  Modify a lens's focus using the semigroup/monoid operator and return the
  old value.
  
  The constant value is applied to the focus from the right:
  ```
  l <<<+>~ x = l <<%~ (<+> x)
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m b

  Modify within a state monad with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> b) -> m b

  Modify within a state monad with pass-through, having access to the index.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<+=) : Num a => MonadState s m => Lens' s a -> a -> m a

  Add a value to the lens into state with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<*=) : Num a => MonadState s m => Lens' s a -> a -> m a

  Multiply a lens's focus into state by a constant value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a

  Subtract a value from the lens into state with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a

  Divide a lens's focus into state by a constant value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool

  Logically OR a lens's focus into state with a constant value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool

  Logically AND a lens's focus into state with a constant value with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a

  Modify a lens's focus into state using a semigroup operation with pass-through.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m a

  Modify the value of a lens into state and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> b) -> m a

  Modify the value of an indexed lens into state and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<.=) : MonadState s m => Lens s s a b -> b -> m a

  Set the value of a lens into state and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<?=) : MonadState s m => Lens s s a (Maybe b) -> b -> m a

  Set a lens into state to `Just` a value and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<+=) : Num a => MonadState s m => Lens' s a -> a -> m a

  Add a value to the lens into state and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<*=) : Num a => MonadState s m => Lens' s a -> a -> m a

  Multiply a lens's focus into state by a constant value and return the old
  value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a

  Subtract a value from the lens into state and return the old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a

  Divide a lens's focus into state by a constant value and return the old
  value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool

  Logically OR a lens's focus into state with a constant value and return the
  old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool

  Logically AND a lens's focus into state with a constant value and return the
  old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a

  Modify a lens's focus into state using a semigroup operation and return the
  old value.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 4

(<<<~) : MonadState s m => Lens s s a b -> m b -> m a

  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.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 1