Idris2Doc : Monocle.Prism

Monocle.Prism

(source)
Definitions
record Prism : Type -> Type -> Type -> Type -> Type
  A Prism is the categorical dual of a Lens: While a Lens allows
  us to extract values from a larger type, a Prism allows us to inject
  values into a larger type, while extracting such a value might not
  be possible.
  
  Prisms are therefore a natural fit for inspecting sum types,
  (as opposed to lenses, which are preferrably used for product types),
  where we typically have one Prism per data constructor.
  
  An other use case where Prisms shine are refinement type, where
  "injecting" a value means extracting a value of the parent type from
  refinement type. An example for this is the `nat` Prism, which allows
  us to convert ("inject") a `Nat` into an `Integer`, while extracting a
  `Nat` from an `Integer` might fail.
  
  A Prism is parameterized over four parameters, because in general
  we can not only try and extract a value from some object
  but also refine the object in case extraction fails.
  Consider lens `fst`, where `s` corresponds to `(a,c)` and
  `t` corresponds to `(b,c)`. Accordingly, if we have a function from
  `a` to `b`, we can convert a pair of type `(a,c)` to one of type `(b,c)`.

  Totality: total
  Visibility: public export
  Constructor: 
P : (s -> Either t a) -> (b -> t) -> Prism s t a b

  Projections:
  
.getOrModify : Prism s t a b -> s -> Either t a
  
.reverseGet : Prism s t a b -> b -> t

  Hints:
  
OSeq Iso Prism Prism
  
OSeq Lens Prism Optional
  
OSeq Prism Prism Prism
  
OSeq Prism Iso Prism
  
OSeq Prism Lens Optional
  
OSeq Prism Optional Optional
  
OSeq Prism Traversal Traversal
  
OSeq Prism Getter Fold
  
OSeq Prism Setter Setter
  
OSeq Prism Fold Fold
  
OSeq Optional Prism Optional
  
OSeq Traversal Prism Traversal
  
OSeq Setter Prism Setter
  
OSeq Getter Prism Fold
  
OSeq Fold Prism Fold
  
ToFold Prism
  
ToOptional Prism
  
ToPrism Prism
  
ToSetter Prism
  
ToTraversal Prism
.getOrModify : Prism s t a b -> s -> Either t a
  Totality: total
  Visibility: public export
getOrModify : Prism s t a b -> s -> Either t a
  Totality: total
  Visibility: public export
.reverseGet : Prism s t a b -> b -> t
  Totality: total
  Visibility: public export
reverseGet : Prism s t a b -> b -> t
  Totality: total
  Visibility: public export
0 Prism' : Type -> Type -> Type
  Convenience alias for monomorphic Prisms, which do not allow
  us to change the value and source types.

  Totality: total
  Visibility: public export
prism : (a -> Maybe b) -> (b -> a) -> Prism' a b
  Convenience constructor for monomorphic Prisms.

  Totality: total
  Visibility: public export
mapA : Applicative f => Prism s t a b -> (a -> f b) -> s -> f t
  Adjust the focus of a Prism with an effectful computation.

  Totality: total
  Visibility: public export
interface ToPrism : (Type -> Type -> Type -> Type -> Type) -> Type
  Interface for converting other optics to Prisms.

  Parameters: o
Methods:
  
toPrism : o s t a b -> Prism s t a b

Implementations:
  
ToPrism Iso
  
ToPrism Prism
toPrism : ToPrism o => o s t a b -> Prism s t a b
  Totality: total
  Visibility: public export
(~>) : Prism s t a b -> Prism a b c d -> Prism s t c d
  Sequential composition of Prisms.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
left' : Prism (Either a b) (Either c b) a c
  A Prism focussing on the `Left` data constructor of `Either a b`.

  Totality: total
  Visibility: public export
left : Prism' (Either a b) a
  Monomorphic version of `left'`.
  
  This can improve type inference for those cases where the versatility
  of `left'` is not needed.

  Totality: total
  Visibility: public export
right' : Prism (Either a b) (Either a c) b c
  A Prism focussing on the `Right` data constructor of `Either a b`.

  Totality: total
  Visibility: public export
right : Prism' (Either a b) b
  Monomorphic version of `right'`.
  
  This can improve type inference for those cases where the versatility
  of `right'` is not needed.

  Totality: total
  Visibility: public export
just' : Prism (Maybe a) (Maybe b) a b
  A Prism focussing on the `Just` data constructor of a `Maybe`.

  Totality: total
  Visibility: public export
just : Prism' (Maybe a) a
  Monomorphic version of `just'`.
  
  This can improve type inference for those cases where the versatility
  of `just'` is not needed.

  Totality: total
  Visibility: public export
nothing : Prism' (Maybe a) ()
  A Prism focussing on the `Nothing` data constructor of a `Maybe`.

  Totality: total
  Visibility: public export
cons' : Prism (List a) (List b) (a, List a) (b, List b)
  A Prism focussing on the `(::)` ("cons") data constructor of a
  `List`.

  Totality: total
  Visibility: public export
nil : Prism' (List a) ()
  A Prism focussing on the `Nil` data constructor of a
  `List`.

  Totality: total
  Visibility: public export
cons : Prism' (List a) (a, List a)
  Monomorphic version of `cons'`.
  
  This can improve type inference for those cases where the versatility
  of `cons'` is not needed.

  Totality: total
  Visibility: public export
snoc' : Prism (SnocList a) (SnocList b) (SnocList a, a) (SnocList b, b)
  A Prism focussing on the `(:<)` ("snoc") data constructor of a
  `SnocList`.

  Totality: total
  Visibility: public export
lin : Prism' (SnocList a) ()
  A Prism focussing on the `Lin` data constructor of a
  `SnocList`.

  Totality: total
  Visibility: public export
snoc : Prism' (SnocList a) (SnocList a, a)
  Monomorphic version of `snoc'`.
  
  This can improve type inference for those cases where the versatility
  of `snoc'` is not needed.

  Totality: total
  Visibility: public export
list1' : Prism (List a) (List b) (List1 a) (List1 b)
  A Prism for converting between non-empty lists and regular lists.

  Totality: total
  Visibility: public export
list1 : Prism' (List a) (List1 a)
  Totality: total
  Visibility: public export
sum : (0 t : k) -> Elem t ks => Prism' (Any f ks) (f t)
  A Prism focussing on a single option in a heterogeneous sum.

  Totality: total
  Visibility: public export
anyHead : Prism' (Any f (k :: ks)) (f k)
  Totality: total
  Visibility: public export
anyTail : Prism' (Any f (k :: ks)) (Any f ks)
  Totality: total
  Visibility: public export
nat : Prism' Integer Nat
  A Prism focussing on non-negative integers.

  Totality: total
  Visibility: public export