Monocle.Iso

Definitions

record Iso : Type -> Type -> Type -> Type -> Type

  An Iso describes an isomorphism between two types.
  
  Two types are isomorphic, if there is a lossless conversion
  from one to the other and vice versa. Examples include the
  (monomorphic) isomorphism from `String` to `List Char` and the
  (polymorphic) isomorphism from `Either a b` to `Either b a`.
  
  Isomorphisms must obey two identity laws:
  
  `get_ . reverseGet` must be the identity function. The same holds
  for `reverseGet . get_`.
  
  Isomorphisms are the most powerful kinds of optics, and they can
  be converted to all other optics in this library.

Totality: total
Visibility: public export
Constructor: 

I : (s -> a) -> (b -> t) -> Iso s t a b

Projections:

.get_ : Iso s t a b -> s -> a

.reverseGet : Iso s t a b -> b -> t

Hints:

OSeq Iso Iso Iso

OSeq Iso Lens Lens

OSeq Iso Prism Prism

OSeq Iso Optional Optional

OSeq Iso Traversal Traversal

OSeq Iso Getter Getter

OSeq Iso Setter Setter

OSeq Iso Fold Fold

OSeq Lens Iso Lens

OSeq Prism Iso Prism

OSeq Optional Iso Optional

OSeq Traversal Iso Traversal

OSeq Setter Iso Setter

OSeq Getter Iso Getter

OSeq Fold Iso Fold

ToFold Iso

ToGetter Iso

ToIso Iso

ToLens Iso

ToOptional Iso

ToPrism Iso

ToSetter Iso

ToTraversal Iso

.get_ : Iso s t a b -> s -> a

Totality: total
Visibility: public export

get_ : Iso s t a b -> s -> a

Totality: total
Visibility: public export

.reverseGet : Iso s t a b -> b -> t

Totality: total
Visibility: public export

reverseGet : Iso s t a b -> b -> t

Totality: total
Visibility: public export

0 Iso' : Type -> Type -> Type

  Convenience alias for monomorphic Isos, which do not allow
  us to change the value and source types.

Totality: total
Visibility: public export

interface ToIso : (Type -> Type -> Type -> Type -> Type) -> Type

  Interface for converting other optics to Isos.

Parameters: o
Methods:

toIso : o s t a b -> Iso s t a b

Implementation: 

ToIso Iso

toIso : ToIso o => o s t a b -> Iso s t a b

Totality: total
Visibility: public export

rev : Iso s t a b -> Iso b a t s

  Isomorphisms are symmetric: If `x` is isomorphic to `y` then `y` is
  isomorphic to `x`. This function describes this symmetry.

Totality: total
Visibility: public export

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

  Sequential composition of Isos.
  
  This describes the transitivity of isomorphisms: If `x` is isomorphic to
  `y` and `y` is isomorhic to `z`, then `x` is isomorphic to `z`.

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

identity : Iso' a a

  Isomorphisms are reflexive: Every type is trivially isomorphic to itself.

Totality: total
Visibility: export

idL : Lens' a a

  The identity lens, derived from the corresponding isomorphism.

Totality: total
Visibility: export

idP : Prism' a a

  The identity prism, derived from the corresponding isomorphism.

Totality: total
Visibility: export

idO : Optional' a a

  The identity optional, derived from the corresponding isomorphism.

Totality: total
Visibility: export

idT : Traversal' a a

  The identity traversal, derived from the corresponding isomorphism.

Totality: total
Visibility: export

pack : Iso' (List Char) String

  Isomorphism between `List Char` and `String`.

Totality: total
Visibility: export

unpack : Iso' String (List Char)

  Isomorphism between `String` and `List Char`.

Totality: total
Visibility: export

chips : Iso (SnocList a) (SnocList b) (List a) (List b)

  Isomorphism between `SnocList` and `List`.

Totality: total
Visibility: export

fish : Iso (List a) (List b) (SnocList a) (SnocList b)

  Isomorphism between `List` and `SnocList`.

Totality: total
Visibility: export

swap : Iso (a, b) (c, d) (b, a) (d, c)

  Isomorphism between pairs with their values swapped.

Totality: total
Visibility: export

flip : Iso (a -> b -> c) (d -> e -> f) (b -> a -> c) (e -> d -> f)

  Isomorphism between binary functions with their arguments
  swapped.

Totality: total
Visibility: export

uncurry : Iso (a -> b -> c) (d -> e -> f) ((a, b) -> c) ((d, e) -> f)

  Isomorphism between binary functions and functions taking
  a pair of values as their argument.

Totality: total
Visibility: export

curry : Iso ((a, b) -> c) ((d, e) -> f) (a -> b -> c) (d -> e -> f)

  Isomorphism between functions taking a pair as their argument
  and binary functions.

Totality: total
Visibility: export

swapE : Iso (Either a b) (Either c d) (Either b a) (Either d c)

  Isomorphism between `Either a b` and `Either b a`.

Totality: total
Visibility: export

withDefault : a -> Iso' (Maybe a) a

  Given a default value of type `a`, we can create an isomorphism between
  `Maybe a` and values of type `a`.
  
  This wraps every value of type `a` in a `Just`. In the other direction,
  we use `fromMaybe` with the provided default value to extract a value
  from a `Nothing`.

Totality: total
Visibility: export

leftVoid : Iso (Either Void a) (Either Void b) a b

  Isomorphism between `Either Void a` and `a`: The `Left` case
  is impossible because `Void` is uninhabited.

Totality: total
Visibility: export

rightVoid : Iso (Either a Void) (Either b Void) a b

  Isomorphism between `Either a Void` and `a`: The `Right` case
  is impossible because `Void` is uninhabited.

Totality: total
Visibility: export

any1 : Iso (Any f [a]) (Any g [b]) (f a) (g b)

  Isomorphism between a unary sum type and the wrapped value.

Totality: total
Visibility: export