Safe Haskell	None
Language	Haskell2010

Data.Profunctor.Optic.Property

Contents

Iso
Prism
Lens
Grate
Traversal0
Traversal & Traversal1
Cotraversal1
Setter

Synopsis

type Iso s t a b = forall p. Profunctor p => Optic p s t a b
fromto_iso :: Eq s => Iso' s a -> s -> Bool
tofrom_iso :: Eq a => Iso' s a -> a -> Bool
type Prism s t a b = forall p. Choice p => Optic p s t a b
tofrom_prism :: Eq s => Prism' s a -> s -> Bool
fromto_prism :: Eq s => Eq a => Prism' s a -> a -> Bool
idempotent_prism :: Eq s => Eq a => Prism' s a -> s -> Bool
type Lens s t a b = forall p. Strong p => Optic p s t a b
tofrom_lens :: Eq s => Lens' s a -> s -> Bool
fromto_lens :: Eq a => Lens' s a -> s -> a -> Bool
idempotent_lens :: Eq s => Lens' s a -> s -> a -> a -> Bool
type Grate s t a b = forall p. Closed p => Optic p s t a b
pure_grate :: Eq s => Grate' s a -> s -> Bool
compose_grate :: Eq s => Grate' s a -> ((((s -> a) -> a) -> a) -> a) -> Bool
type Traversal0 s t a b = forall p. (Strong p, Choice p) => Optic p s t a b
tofrom_traversal0 :: Eq a => Eq s => Traversal0' s a -> s -> a -> Bool
fromto_traversal0 :: Eq s => Traversal0' s a -> s -> Bool
idempotent_traversal0 :: Eq s => Traversal0' s a -> s -> a -> a -> Bool
type Traversal s t a b = forall p. (Choice p, Representable p, Applicative (Rep p)) => Optic p s t a b
pure_traversal :: Eq (f s) => Applicative f => ((a -> f a) -> s -> f s) -> s -> Bool
compose_traversal :: Eq (f (g s)) => Applicative f => Applicative g => (forall f. Applicative f => (a -> f a) -> s -> f s) -> (a -> g a) -> (a -> f a) -> s -> Bool
compose_traversal1 :: Eq (f (g s)) => Apply f => Apply g => (forall f. Apply f => (a -> f a) -> s -> f s) -> (a -> g a) -> (a -> f a) -> s -> Bool
type Cotraversal1 s t a b = forall p. (Closed p, Corepresentable p, Apply (Corep p)) => Optic p s t a b
compose_cotraversal1 :: Eq s => Apply f => Apply g => (forall f. Apply f => (f a -> a) -> f s -> s) -> (g a -> a) -> (f a -> a) -> g (f s) -> Bool
type Setter s t a b = forall p. (Closed p, Choice p, Representable p, Applicative (Rep p), Distributive (Rep p)) => Optic p s t a b
pure_setter :: Eq s => Setter' s a -> s -> Bool
compose_setter :: Eq s => Setter' s a -> (a -> a) -> (a -> a) -> s -> Bool
idempotent_setter :: Eq s => Setter' s a -> s -> a -> a -> Bool

Iso

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

Iso

$ \mathsf{Iso}\;S\;A = S \cong A $

For any valid Iso o we have: o . re o ≡ id re o . o ≡ id view o (review o b) ≡ b review o (view o s) ≡ s

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 #

Prisms access one piece of a sum.

$ \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 #

Lenses access one piece of a product.

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

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 #

Grates access the codomain of a function.

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

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

```
sabt ($ s) ≡ s
```

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

sabt (k -> h (k . sabt)) ≡ sabt (k -> h ($ k))

Traversal0

type Traversal0 s t a b = forall p. (Strong p, Choice p) => Optic p s t a b Source #

A Traversal0 processes at most one part of the whole, with no interactions.

$ \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 & Traversal1

type Traversal s t a b = forall p. (Choice p, Representable p, Applicative (Rep p)) => Optic p s t a b Source #

A Traversal processes 0 or more parts of the whole, with Applicative interactions.

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

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

A Traversal is a valid Setter with the following additional laws:

```
abst pure ≡ pure
```

fmap (abst f) . abst g ≡ getCompose . abst (Compose . fmap f . g)

These can be restated in terms of withTraversal:

withTraversal abst (Identity . f) ≡  Identity . fmap f

Compose . fmap (withTraversal abst f) . withTraversal abst g == withTraversal abst (Compose . fmap f . g)

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

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

Cotraversal1

type Cotraversal1 s t a b = forall p. (Closed p, Corepresentable p, Apply (Corep p)) => Optic p s t a b Source #

compose_cotraversal1 :: Eq s => Apply f => Apply g => (forall f. Apply f => (f a -> a) -> f s -> s) -> (g a -> a) -> (f a -> a) -> g (f s) -> Bool Source #

A Cotraversal1 is a valid Resetter with the following additional law:

abst f . fmap (abst g) ≡ abst (f . fmap g . getCompose) . Compose

These can be restated in terms of cowithTraversal1:

cowithTraversal1 abst (f . runIdentity) ≡  fmap f . runIdentity

cowithTraversal1 abst f . fmap (cowithTraversal1 abst g) . getCompose == cowithTraversal1 abst (f . fmap g . getCompose)

Setter

type Setter s t a b = forall p. (Closed p, Choice p, Representable p, Applicative (Rep p), Distributive (Rep p)) => Optic p s t a b Source #

A Setter modifies part of a structure.

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

pure_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
```