profunctor-optics-0.0.2: A compact optics library compatible with the typeclasses in profunctors.

Safe HaskellNone
LanguageHaskell2010

Data.Profunctor.Optic.Property

Contents

Synopsis

Iso

type Iso s t a b = forall p. Profunctor p => Optic p s t a b Source #

\( \mathsf{Iso}\;S\;A = S \cong A \)

fromto_iso :: Eq s => Iso' s a -> s -> Bool Source #

Going back and forth doesn't change anything.

tofrom_iso :: Eq a => Iso' s a -> a -> Bool Source #

Going back and forth doesn't change anything.

Prism

type Prism s t a b = forall p. Choice p => Optic p s t a b Source #

\( \mathsf{Prism}\;S\;A = \exists D, S \cong D + A \)

tofrom_prism :: Eq s => Prism' s a -> s -> Bool Source #

If we are able to view an existing focus, then building it will return the original structure.

  • (id ||| bt) (sta s) ≡ s

fromto_prism :: Eq s => Eq a => Prism' s a -> a -> Bool Source #

If we build a whole from a focus, that whole must contain the focus.

  • sta (bt b) ≡ Right b

idempotent_prism :: Eq s => Eq a => Prism' s a -> s -> Bool Source #

  • left sta (sta s) ≡ left Left (sta s)

Lens

type Lens s t a b = forall p. Strong p => Optic p s t a b Source #

\( \mathsf{Lens}\;S\;A = \exists C, S \cong C \times A \)

id_lens :: Eq s => Lens' s a -> s -> Bool Source #

tofrom_lens :: Eq s => Lens' s a -> s -> Bool Source #

You get back what you put in.

  • view o (set o b a) ≡ b

fromto_lens :: Eq a => Lens' s a -> s -> a -> Bool Source #

Putting back what you got doesn't change anything.

  • set o (view o a) a  ≡ a

idempotent_lens :: Eq s => Lens' s a -> s -> a -> a -> Bool Source #

Setting twice is the same as setting once.

  • set o c (set o b a) ≡ set o c a

Grate

type Grate s t a b = forall p. Closed p => Optic p s t a b Source #

\( \mathsf{Grate}\;S\;A = \exists I, S \cong I \to A \)

id_grate :: Eq s => Grate' s a -> s -> Bool Source #

const_grate :: Eq s => Grate' s a -> s -> Bool Source #

  • sabt ($ s) ≡ s

compose_grate :: Eq s => Functor f => Functor g => Grate' s a -> (f a -> a) -> (g a -> a) -> f (g s) -> Bool Source #

Traversal0

type Traversal0 s t a b = forall p. Affine p => Optic p s t a b Source #

\( \mathsf{Traversal0}\;S\;A = \exists C, D, S \cong D + C \times A \)

tofrom_traversal0 :: Eq a => Eq s => Traversal0' s a -> s -> a -> Bool Source #

You get back what you put in.

  • sta (sbt a s) ≡ either (Left . const a) Right (sta s)

fromto_traversal0 :: Eq s => Traversal0' s a -> s -> Bool Source #

Putting back what you got doesn't change anything.

  • either id (sbt s) (sta s) ≡ s

idempotent_traversal0 :: Eq s => Traversal0' s a -> s -> a -> a -> Bool Source #

Setting twice is the same as setting once.

  • sbt (sbt s a1) a2 ≡ sbt s a2

Traversal

type Traversal s t a b = forall p. (Affine p, Traversing p) => Optic p s t a b Source #

\( \mathsf{Traversal}\;S\;A = \exists F : \mathsf{Traversable}, S \equiv F\,A \)

id_traversal :: Eq s => Traversal' s a -> s -> Bool Source #

id_traversal1 :: Eq s => Traversal1' s a -> s -> Bool Source #

pure_traversal :: Eq (f s) => Applicative f => ATraversal' f s a -> s -> Bool Source #

compose_traversal :: Eq (f (g s)) => Applicative' f => Applicative' g => Traversal' s a -> (a -> g a) -> (a -> f a) -> s -> Bool Source #

compose_traversal1 :: Eq (f (g s)) => Apply f => Apply g => Traversal1' s a -> (a -> g a) -> (a -> f a) -> s -> Bool Source #

Cotraversal

type Cotraversal s t a b = forall p. (Coaffine p, Cotraversing p) => Optic p s t a b Source #

\( \mathsf{Cotraversal}\;S\;A = \exists F : \mathsf{Distributive}, S \equiv F\,A \)

Setter

type Setter s t a b = forall p. (Affine p, Traversing p, Mapping p) => Optic p s t a b Source #

\( \mathsf{Setter}\;S\;A = \exists F : \mathsf{Functor}, S \equiv F\,A \)

id_setter :: Eq s => Setter' s a -> s -> Bool Source #

  • over o id ≡ id

compose_setter :: Eq s => Setter' s a -> (a -> a) -> (a -> a) -> s -> Bool Source #

  • over o f . over o g ≡ over o (f . g)

idempotent_setter :: Eq s => Setter' s a -> s -> a -> a -> Bool Source #

  • set o y (set o x a) ≡ set o y a