Monocle.Getter

Definitions

record Getter : Type -> Type -> Type -> Type -> Type

  Getters allows us to extract exactly one piece of data of type `a` from
  a source value of type `s`. They are therefore like Folds but with
  stronger guarantees.
  
  Just like Folds and other optics, Getters can be composed sequentially,
  and just like Folds, Getters have two additional type parameters
  (`t` and `b`), which have no runtime relevance and are only used to
  compose them with other optics.

Totality: total
Visibility: public export
Constructor: 

G : (s -> a) -> Getter s t a b

Projection: 

.to_ : Getter s t a b -> s -> a

Hints:

OSeq Iso Getter Getter

OSeq Lens Getter Getter

OSeq Prism Getter Fold

OSeq Optional Getter Fold

OSeq Traversal Getter Fold

OSeq Getter Getter Getter

OSeq Getter Iso Getter

OSeq Getter Lens Getter

OSeq Getter Prism Fold

OSeq Getter Optional Fold

OSeq Getter Traversal Fold

OSeq Getter Fold Fold

OSeq Fold Getter Fold

ToFold Getter

ToGetter Getter

.to_ : Getter s t a b -> s -> a

Totality: total
Visibility: public export

to_ : Getter s t a b -> s -> a

Totality: total
Visibility: public export

(~>) : Getter s t a b -> Getter a b c d -> Getter s t c d

  Sequential composition of Getters.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 0

interface ToGetter : (Type -> Type -> Type -> Type -> Type) -> Type

  Interface for converting other optics to Getters.

Parameters: o
Methods:

toGetter : o s t a b -> Getter s t a b

Implementations:

ToGetter Iso

ToGetter Getter

ToGetter Lens

toGetter : ToGetter o => o s t a b -> Getter s t a b

Totality: total
Visibility: public export

to : ToGetter o => o s t a b -> s -> a

  Use a Getter to extract a piece of data from a source value.

Totality: total
Visibility: public export

getST : Monad m => ToGetter o => o s t a b -> StateT s m a

  View the current state through a `Getter`

Totality: total
Visibility: export

withST : Monad m => ToGetter o => o s s a a -> (a -> StateT s m t) -> StateT s m t

Totality: total
Visibility: export