Oleg's gists — Archive

Glassery

Posted on 2017-04-18 by Oleg Grenrus

After I have improved the raw performance of optika – a JavaScript optics library, it's time to make the library (feature-)complete and sound. Gathering and classifying all possible optic types, gives us a reference point to guide the implementation. In this post I systematically introduce various optic types, using programming language Haskell. In fact, this literal Haskell file could be turned into a library with some work. The primary goal of this post is to clarify my own thoughts; but I hope it may be useful for others too.

As some of the previous posts ( Compiling lenses, Affine Traversal, Why there is no AGetter? ), this is a literate Haskell file, but this time we don't depend on profunctors (but as it seems, on everything else).

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
module Glassery where
import Control.Monad.Trans.State (State, evalState, state)
import Data.Distributive (Distributive (..), cotraverse)
import Data.Foldable (traverse_)
import Data.Functor.Apply (Apply (..))
import Data.Functor.Const (Const (..))
import Data.Functor.Identity (Identity (..))
import Data.Functor.Rep hiding (tabulated)
import Data.Monoid (Endo (..))
import Data.Pointed (Pointed (..))
import Data.Proxy (Proxy (..))
import Data.Semigroup (Semigroup (..))
import Data.Semigroup.Foldable (Foldable1 (..), traverse1_)
import Data.Semigroup.Traversable (Traversable1 (..))
import Data.Tuple (swap)
import GHC.Proof ((===), (=/=))
import Linear (V2 (..))

cc-by-sa This work is licensed under a “CC BY SA 4.0” license.

Introduction

Profunctor formulation of optics is elegant:

type Optic c s t a b = forall p. c p => p a b -> p s t

Depending of the constraint c, we get different kind of optics, e.g. with c = Strong we get a Lens. There are not many type classes for * -> * -> * kinded types: Profunctor, Strong, Choice, Bifunctor and few less known ones: Traversing1, Traversing, Mapping and Bicontravariant (and Closed). The subset lattice of class sets exposes an optics hierarchy:

Each color represents different class added into the mix. Iso is restricted only by Profunctor; imposing additional Strong (blue) constraint we get Lens; adding Traversing1 (green) turns a Lens into a Traversal1. Other colors are for Choice (red), Bicontravariant (orange), Bifunctor (purple), and Mapping (gray). There is no color for Traversing as it's (almost) the combination of Traversing1 and Choice.

If the implementation is concrete-representation based, this graph is an inheritance graph of optic classes (good example of multiple inheritance!). With the van Laarhoven encoding of lenses, you get the same hierarchy; but it's not as easy to see, as the type Optic is more complicated. See the documentation for Control.Lens.Type module.

The Strong part of the graph can also be indexed: IndexedLens, IndexedTraversal etc. Indexed optics provide also the index of a smaller value inside the bigger one.

Major part of the content of this post is based on the haddock documentation of Edward Kmett's lens and profunctors packages. The "Profunctor Optics: Modular Data Accessors" by Matthew Pickering et al is also one reference, even it doesn't discuss all the possible (known) optics. The Typeclassopedia has influenced the format.

Edit: There are older posts about profunctor optics: in r6research: Mainline Profunctor Heirarchy for Optics and bennofs' lpaste.

We can summarize the contents of this post as a table (of contents). For each optic type there is a constructor and characterizing operations (analogous to introduction and elimination rules in logic!), as well as closely related type classes and profunctors. Some operations occur more than once in the table. This is because I try to make table complete, for example lens-operations view and set are operations of Lens sub-classes: Getter and Setter, but they are enough to describe a Lens l:

lens (view l) (set l) ≡ l
      view (lens g s) ≡ g
       set (lens g s) ≡ s

Compare that to the local soundness and completeness of conjunction:

pair (fst p) (snd p) ≡ p  -- complete
      fst (pair x y) ≡ x  -- sound 1
      snd (pair x y) ≡ y  -- sound 2

Optic	Constructor	Operations	Type class	Profunctor
Equality	`id`, `simple`			`Identical`
Iso	`iso`	`view`, `review`	`Profunctor`
Prism	`prism`	`previewE`, `review`	`Choice`	`ForgetE`
Review	`upto`	`review`	`Bifunctor`	`Tagged`
Getter	`to`	`view`	`Bicontravariant`
Lens	`lens`	`view`, `set`	`Strong`
Affine Traversal	`affine`	`previewE`, `set`	`Choice`, `Strong`
Traversal1	`traversing1`	`traverse1Of`	`Traversing1`	`Star`
Traversal	`traversing`	`traverseOf`	`Traversing`	`Star`
Affine Fold	`afolding`	`preview`		`ForgetM`
Fold1	`folding1`	`foldMap1Of`		`Forget`
Fold	`folding`	`foldMapOf`		`Forget`
Setter	`setting`	`over`	`Mapping`	`(->)`

Each optic section follows the same internal structure:

I define the optic using profunctor framework
then informally describe it,
state its laws,
introduce related type class (if any),
show how its constructor and operations can be defined
state the completeness and soundness properties of them, and
define a data type used to implement the operations.

After the bulk of the text, there are sections about Indexed optics, concrete optics, re-operation, Closed type class and the optic it induces: Grate.

Practical Optic

Though formulation presented in the introduction would work, it's not practical in Haskell as we'd need to enable UndecidableSuperClasses to write

class CTop1 a
instance CTop1 a

class (f a, g a) => (f :/\: g) a
instance (f a, g a) => (f :/\: g) a

So instead we'll define different type alias:

type Optic p s t a b = p a b -> p s t

and universally qualify over p in the particular optic type definition. After this small technicality we can continue to the first concrete optic: Equality.

Equality

The root of the optics hierarchy is an Equality.

type Equality s t a b = forall p. Optic p s t a b

It's a witness that both pairs of types: (a ~ s) and (b ~ t) are equal. I "borrowed" the diagrams from the paper by Matthew Pickering et al.. They nicely illustrate what various optics do. In the Equality case we can go back and forth between s and a as well as between t and b.

Types like Equality are used to witness equality in Haskell without GADTs (eq package), in PureScript purescript-leibniz, or in Scala scalaz: Leibniz. PrimGetter and PrimReview have similar "two-in-one" property, as we will see in respective sections.

data type: Identical

The :~: type from Data.Type.Equality is another type for propositional equality, it arguably more directly encodes the equality:

data a :~: b where
    Refl :: a :~: a -- or a ~ b => a :~: b

It however encodes only single equality. Encoding two at the same time isn't difficult

data Identical a b s t where
    Identical :: Identical a b a b

We can convert freely between pair of :~: and Equality, using Identical. In fact, the id is the only (non-bottom) constructor for Equality:

toEquality :: a :~: s -> b :~: t -> Equality s t a b
toEquality Refl Refl = id

fromEquality :: Equality s t a b -> (a :~: s, b :~: t)
fromEquality l = case (l Identical) of
    Identical -> (Refl, Refl)

constructor: simple

The simple is occasionally useful to constraint excessive polymorphism, e.g turn Optic into simple Optic'.

type Simple o s a = o s s a a
type Optic' p s a = Optic p s s a a -- Simple (Optic p) s a
type As a = Simple Equality a a

-- | @foo . (simple :: As Int) . bar@.
simple :: As a
simple = id

Iso

The relaxed version of equality is an isomorphism, Iso.

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

We restrict Equality so we can go only from s to a and from b to t. In simple, monomorphic case we get a bijection between s and a. The type system doesn't prevent us from encoding two arbitrary functions (which aren't inverses of each other) as an Iso, but then that value won't be a lawful Iso.

laws

Since every Iso is both a valid Lens and a valid Prism the laws for those types imply the following laws for an Iso o:

viewP o (reviewP o b) ≡ b
reviewP o (viewP o s) ≡ s

Or even more powerfully using re:

o . re o ≡ id
re o . o ≡ id

Intuitively re "rotates" the optic diagram 180 degrees, turning Iso s t a b into Iso b a t s, Review t b into Getter b t and back.

Note: re in the Haskell lens only turns a Review into a Getter, as the asymmetry of van Laarhoven encoding prevents making more general re. Therefore we have from to invert Iso.

Note: re doesn't turn Lens into Prism (or vice versa), that's discussed later.

type class: Profunctor

Intuitively Profunctor is a bifunctor where the first argument is contravariant and the second argument is covariant.

Other way to see it is a generalization of function, which can be pre- and post-composed with other functions but not with itself.

class Profunctor p where
    dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
    dimap f g = lmap f . rmap g

    lmap :: (a -> b) -> p b c -> p a c
    lmap f = dimap f id

    rmap :: (b -> c) -> p a b -> p a c
    rmap = dimap id

    {-# MINIMAL dimap | (lmap , rmap) #-}

Note: here and later we won't state the laws of the type classes. Also note that optics and Profunctor laws aren't connected, we can construct and use incorrect optics using lawful Profunctors. The next (after 5.2) release of profunctors library will contain laws in the haddock documentation. This post will be later updated to contain links to the Hackage documentation.

constructor: iso

iso builds an isomorphism from a pair of inverse functions.

iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso = dimap

soundness and completeness

The describing operations of Iso are viewP (of Getter) and reviewP (of Review). Using those we can state completeness equation for Iso:

iso_complete :: Iso s t a b -> Iso s t a b
iso_complete o = iso (viewP o) (reviewP o)

If compiler would be smart enough, it can simplify that definition to iso_complete p = p. Unfortunately it isn't, so we cannot use ghc-proofs (blog post) by Joachim Breitner for completeness proofs. Luckily, soundness proofs are simpler, so we can prove them, we only have to eta-expand the functions (which would make HLint unhappy).

iso_sound1_proof :: ()
iso_sound1_proof =
    (\getter setter s -> viewP (iso getter setter) s)
    ===
    (\getter _setter s -> getter s)

iso_sound2_proof :: ()
iso_sound2_proof =
    (\getter setter b -> reviewP (iso getter setter) b)
    ===
    (\_getter setter b -> setter b)

Prism

A prism is a first-class pattern. Prisms are to sum data types as lenses are to product data types.

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

laws

First, if I review a value with a Prism and then preview, I will get it back:
```
preview l (review l b) ≡ Just b
```
If you can extract a value a using a Prism l from a value s, then the value s is completely described by l and a:
```
preview l s ≡ Just a ⇒ review l a ≡ s
```

type class: Choice

The generalization of Costar of Functor that is strong with respect to Either.

class Profunctor p => Choice p where
    left' :: p a b -> p (Either a c) (Either b c)
    left' =  dimap swapE swapE . right'

    right' :: p a b -> p (Either c a) (Either c b)
    right' = dimap swapE swapE. left'

    {-# MINIMAL left' | right' #-}

swapE :: Either a b -> Either b a
swapE = either Right Left

Note: that left' and right' are Prisms, called _Left and _Right in Haskell's lens.

λ> :t left' :: Prism (Either a c) (Either b c) a b
left' :: Prism (Either a c) (Either b c) a b
  :: Choice p => Optic p (Either a c) (Either b c) a b

λ> :t right' :: Prism (Either c a) (Either c b) a b
right' :: Prism (Either c a) (Either c b) a b
  :: Choice p => Optic p (Either c a) (Either c b) a b

constructor: prism

prism builds a Prism from build (which is a setter) and match (which is a getter) functions:

prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
prism setter getter = dimap getter (either id setter) . right'

Note: That's how they will be defined in purescript-profunctor-lenses, and are in mezzolens.

There the right' is a foundational operation letting us to focus on the smaller part of the sum (Either). dimap preprocesses the input, recall it witnesses an isomorphism, in this case Iso s t (Either t a) (Either t b). But that's not an isomorphism! The more theoretically correct definition would be to use some (existential) type:

eprism :: (Either e b -> t) -> (s -> Either e a) -> Prism s t a b
eprism build match = dimap match build . right'

The existential definition is an insight I learned from Edward Kmett; similar approach applies to Lens. In practice (think about any bigger sum type), this is not good way to do things, as we don't have way to say "SumOfThree which isn't constructed with FirstOfThree".

operation: previewE

Describing operations are preview (see Affine Fold) and review (see Review). Yet, careful reader may notice that type of preview is s -> Maybe a, which would only allow us to define a monomorphic constructor:

prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' setter getter = prism setter (\s -> maybe (Left s) Right (getter s))

-- previewE :: Prism s t a b -> s -> Either t a
previewE :: Optic (ForgetE a) s t a b -> s -> Either t a
previewE o = runForgetE (o (ForgetE Right))

soundness and completeness

previewE together with reviewP completely describe Prism:

prism_complete :: Prism s t a b -> Prism s t a b
prism_complete p = prism (reviewP p) (previewE p)

The soundness properties are obvious:

prism_sound1_proof :: ()
prism_sound1_proof =
    (\getter setter s -> previewE (prism setter getter) s)
    ===
    (\getter _setter s -> getter s)

prism_sound2_proof :: ()
prism_sound2_proof =
    (\getter setter b -> reviewP (prism setter getter) b)
    ===
    (\_getter setter b -> setter b)

data type: ForgetE

ForgetE is the first profunctor we see from family of Forget profunctors. It's the one which isn't an instance of Traversing1.

newtype ForgetE r a b = ForgetE { runForgetE :: a -> Either b r }

Instance definitions are in the appendix.

Review

A Review describes how to construct a single value. It's a dual of Getter.

type PrimReview s t a b = forall p. Bifunctor p => Optic p s t a b
type Review t b = forall p. (Bifunctor p, Choice p) => Optic' p t b

Unlike a Prism a Review is write-only. Since a Review cannot be used to read back there are no laws that can be applied to it. In fact, it is isomorphic to an arbitrary function from (b -> t) as witnessed by upto and review. Similarly, there are no laws for Getter either.

Note that Review isn't Simple PrimReview, by using both Bifunctor and Profunctor constraint we say that the first argument of a bifunctor is phantom. That how we remove the first rail from the diagram.

In practice we don't need two-in-one PrimReview (or PrimGetter), so there is little reason to define it in the libraries.

type class: Bifunctor

Bifunctor class is a bifunctor where both arguments are covariant, unlike Profunctor which is contravariant in the first argument. Bifunctor is in the base library since version 4.8.0.0. Many Prelude types are Bifunctors, e.g. Either and (,).

class Bifunctor p where
    bimap :: (a -> b) -> (c -> d) -> p a c -> p b d
    bimap f g = first f . second g

    first :: (a -> b) -> p a c -> p b c
    first f = bimap f id

    second :: (b -> c) -> p a b -> p a c
    second = bimap id

    {-# MINIMAL bimap | (first, second) #-}

constructor: upto

You can generate a Review by using unto. You can also use any Prism or Iso directly as a Review.

upto :: (b -> t) -> Review t b
upto f = bimap f f

uptoP :: (a -> s) -> (b -> t) -> PrimReview s t a b
uptoP = bimap

There is another way to define upto, only using the function argument once. As the first argument of a profunctor is phantom, we can freely change it:

firstPhantom :: (Bifunctor p, Profunctor p) => p a c -> p b c
firstPhantom p = lmap (const ()) (first (const ()) p)

upto' :: (b -> t) -> Review t b
upto' f = firstPhantom . rmap f

operation: review

This can be used to turn an Iso or Prism around and view a value through it the other way.

review :: Optic' Tagged t b -> b -> t
review o b = unTagged (o (Tagged b))

reviewP :: Optic Tagged s t a b -> b -> t
reviewP o b = unTagged (o (Tagged b))

soundness and completeness

Soundness and completeness of review and upto is trivial to show:

review_complete :: Review t b -> Review t b
review_complete o = upto (review o)

review_sound_proof :: ()
review_sound_proof =
    (\build b -> review (upto build) b)
    ===
    (\build b -> build b)

data type: Tagged

A Tagged a b value is a value b with an attached phantom type a.

Thus it's Profunctor and Bifunctor.

newtype Tagged a b = Tagged { unTagged :: b }

Instance definitions are in the appendix.

Getter

A Getter describes how to retrieve a single value in a way that can be composed with other optics. It's a dual of Review.

type PrimGetter s t a b = forall p. Bicontravariant p => Optic p s t a b
type Getter s a = forall p. (Bicontravariant p, Strong p) => Optic' p s a

Unlike a Lens a Getter is read-only. Since a Getter cannot be used to write back there are no Lens laws that can be applied to it. In fact, it is isomorphic to an arbitrary function from (s -> a).

type class: Bicontravariant

Bicontravariant as a bifunctor contravariant in both arguments. It's a dual of Bifunctor. AFAIK none widely used package defines this type class.

class Bicontravariant p where
    cimap :: (b -> a) -> (d -> c) -> p a c -> p b d
    cimap f g = cofirst f . cosecond g

    cofirst :: (b -> a) -> p a c -> p b c
    cofirst f = cimap f id

    cosecond :: (c -> b) -> p a b -> p a c
    cosecond = cimap id

    {-# MINIMAL cimap | (cofirst, cosecond) #-}

constructor: to

We can use to construct a Getter. Unsurprisingly, it's definition is similar to the definition of upto:

to :: (s -> a) -> Getter s a
to f = cimap f f

toP :: (s -> a) -> (t -> b) -> PrimGetter s t a b
toP = cimap

operation: view

Definition of view is more complicated than for review. We start with a function a -> a (wrapped as Forget a a a), where the result type is fixed; and transform it into s -> a using the optic.

view :: Optic' (Forget a) s a -> s -> a
view o = runForget (o (Forget id))

viewP :: Optic (Forget a) s t a b -> s -> a
viewP o = runForget (o (Forget id))

Note: view, as defined above, accepts also other optics than Lens, but in any case it returns only single a.

soundness and completeness

Soundness and completeness of to and view is trivial to show, similarly to `Review.

getter_complete :: Getter s a -> Getter s a
getter_complete o = to (view o)

getter_sound_proof :: ()
getter_sound_proof =
    (\getter b -> view (to getter) b)
    ===
    (\getter b -> getter b)

data type: Forget

Forget is a bifunctor contravariant in the first argument, and phantom in the second. It's used to implement operations on all optics containing Bicontravariant constraint, i.e. Getter and the folds.

newtype Forget r a b = Forget { runForget :: a -> r }

Note: Forget r is isomorphic to Star (Const r).

Instance definitions are in the appendix.

Lens

A Lens s t a b is a purely functional reference.

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

laws

You get back what you put in:
```
view l (set l v s)  ≡ v
```
Putting back what you got doesn't change anything:
```
set l (view l s) s  ≡ s
```
Setting twice is the same as setting once:
```
set l v' (set l v s) ≡ set l v' s
```

type class: Strong

Generalizing Star of a strong Functor.

class Profunctor p => Strong p where
  first' :: p a b  -> p (a, c) (b, c)
  first' = dimap swap swap . second'

  second' :: p a b -> p (c, a) (c, b)
  second' = dimap swap swap . first'

  {-# MINIMAL first' | second' #-}

Note:: first' and second' are lenses, however they aren't _1 and _2 as latter have more general type in Kmett's lens.

constructor: lens

lens builds a Lens from getter and setter.

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens getter setter pab = dimap
     (\s -> (getter s, s))
     (\(b, s) -> setter s b)
     (first' pab)

Note: There is an issue in profunctors whether this method should be in Strong (similarly as prism in Choice).

soundness and completeness

viewP (from Getter) andset(fromSetter) completely describe aLens`:

lens_complete :: Lens s t a b -> Lens s t a b
lens_complete o = lens (viewP o) (set o)

And the operations are obviously sound:

lens_sound1_proof :: ()
lens_sound1_proof =
    (\getter setter s -> viewP (lens getter setter) s)
    ===
    (\getter _setter s -> getter s)

lens_sound2_proof :: ()
lens_sound2_proof =
    (\getter setter s b -> set (lens getter setter) s b)
    ===
    (\_getter setter s b -> setter s b)

Affine Traversal

Affine Traversal is an optic that has 0 or 1 target. A bit like Prism, but unlike it (and like Lens) you cannot use it to construct the value, only change the inner part.

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

If Iso combines the both good properties of Lens and Prism, AffineTraversal combines both bad ones: it what you get when you compose Lens with Prism (or Prism with Lens):

laws

As with Iso we can deduce Affine Traversal laws from Lens and Prism laws:

You get back what you put in:

preview l (set l v s)  ≡ v <$ preview l s

If you can extract a value, and put it back, that doesn't change anything.
```
preview l s ≡ Just a => set l s a ≡ s
```
If you get nothing when extracting a value, then whatever you put in, the operation is no-op.
```
preview l s ≡ Nothing => set l s a ≡ s
```
Setting twice is the same as setting once:
```
set l v' (set l v s) ≡ set l v' s
```

constructor: affine

affineTraversal :: (s -> Either t a)
                -> (s -> b -> t)
                -> AffineTraversal s t a b
affineTraversal getter setter pab = dimap
    (\s -> (getter s, s))
    (\(bt, s) -> either id (setter s) bt)
    (first' (right' pab))

soundness and completeness

The describing operations of AffineTraversal are previewE and set. Using those we can state completeness equation for Affine Traversal:

affine_traversal_complete ::
    AffineTraversal s t a b -> AffineTraversal s t a b
affine_traversal_complete o = affineTraversal (previewE o) (set o)

The soundness proofs:

affine_traversal_sound1_proof :: ()
affine_traversal_sound1_proof =
    (\getter setter s -> previewE (affineTraversal getter setter) s)
    ===
    (\getter _setter s -> getter s)

affine_traversal_sound2_proof :: ()
affine_traversal_sound2_proof =
    (\getter setter s b -> set (affineTraversal getter setter) s b)
    =/=
    (\_getter setter s b -> setter s b)

ghc-proofs fails to prove the second one when trying to unify:

\getter setter s b ->
    case getter s of
        Left x -> x
        Right y -> setter s b
\getter setter s b ->
    setter s b

Here we need to use the third law of Affine Traversal to proceed. In the Left x clause, x and setter s b are equivalent; as we get nothing from the getter (the x is s), setting the value is a no-op.

Traversal1

A Traversal s t a b (Traversal1 s t a b) is a generalization of traverse (traverse1) from Traversable (Traversable1). It allows you to traverse over a structure and change out its contents with monadic or Applicative (Apply) side-effects.

type Traversal1 s t a b = forall p. Traversing1 p => Optic p s t a b

laws

The laws of Traversal can be stated for Traversal1 too.

Identity
```
traverse1Of t (Id . f) ≡  Id (fmap f)
```

Composition

Compose . fmap (traverse1Of t f) . traverse1Of t g ≡
traverse1Of t (Compose . fmap f . g)

type class: Traversing1

class (Strong p) => Traversing1 p where
    traverse1' :: Traversable1 f => p a b -> p (f a) (f b)
    traverse1' = wander1 traverse1

    wander1 :: (forall f. Apply f => (a -> f b) -> s -> f t)
            -> p a b -> p s t

traverse1' can be defined using wander1, but the implemenation is not very insightful, the Traversable Baz1 type is the key:

newtype Baz1 t b a
    = Baz1 { runBaz :: forall f. Apply f => (a -> f b) -> f t }

See profunctors source for the details.

Note: Traversing1 determines Strong:

firstTraversing1 :: Traversing1 p => p a b -> p (a, c) (b, c)
firstTraversing1 = dimap swap swap . traverse1'

secondTraversing1 :: Traversing1 p => p a b -> p (c, a) (c, b)
secondTraversing1 = traverse1'

constructor: traversing1

As Traversing1 is cleverly defined class, the constructor of a Traversal1 is just a new name for wander1.

traversing1 :: (forall f. Apply f => (a -> f b) -> s -> f t)
            -> Traversal1 s t a b
traversing1 = wander1

operation: traverse1Of

Map each element of a structure targeted by a Lens or Traversal1, evaluate these actions from left to right, and collect the results.

-- traverse1Of :: Traversal1 s t a b
--             -> (forall f. Apply f => (a -> f b) -> s -> f t)
traverse1Of :: Apply f
            => Optic (Star f) s t a b
            -> (a -> f b) -> s -> f t
traverse1Of o f = runStar (o (Star f))

Note: the Apply f constraint is redundant, but it will be needed to satisfy Traversing1 (Star f)! It makes sense to define:

withStar :: Optic (Star f) s t a b
         -> (a -> f b) -> s -> f t
withStar o f  = runStar (o (Star f))

Note: In van Laarhoven encoding, implementation of traverse1Of (and traverseOf) is simply an id (with less general type). In profunctor encoding the over operation is id!

data type: Star

Star is isomorphic to Kleisli from base. It lifts a Functor into a Profunctor (forwards).

newtype Star f a b = Star { runStar :: a -> f b }

Instance definitions are in the appendix.

Traversal

A Traversal s t a b (Traversal1 s t a b) is a generalization of traverse (traverse1) from Traversable (Traversable1). It allows you to traverse over a structure and change out its contents with monadic or Applicative (Apply) side-effects.

type Traversal s t a b = forall p. Traversing p => Optic p s t a b

laws

The laws for a Traversal t follow from the laws for Traversable as stated in "The Essence of the Iterator Pattern".

Identity
```
traverseOf t (Id . f) ≡  Id (fmap f)
```

Composition

Compose . fmap (traverseOf t f) . traverseOf t g ≡
traverseOf t (Compose . fmap f . g)

type class: Traversing

Note: Definitions in terms of 'wander' are much more efficient! Note: traverse' can be defined in terms of wander.

class (Choice p, Traversing1 p) => Traversing p where
  traverse' :: Traversable f => p a b -> p (f a) (f b)
  traverse' = wander traverse

  wander :: (forall f. Applicative f => (a -> f b) -> s -> f t)
         -> p a b -> p s t

Traversing fully determines Choice:

leftTraversing :: Traversing p => p a b -> p (Either a c) (Either b c)
leftTraversing = dimap swapE swapE . traverse'

rightTraversing :: Traversing p => p a b -> p (Either c a) (Either c b)
rightTraversing = traverse'

The Traversing class is needed as Choice and Traversing1 doesn't necessarily agree with Traversing. Intuitively Choice can be used to check whether a container is empty or not, and if not then we could use Traversing1. If the classes are internal to the optics library, Traversing is still useful to provide more efficient wander. The situation similar to Applicative ⊂ Apply and Pointed situation, superset because there are extra interaction laws.

constructor: traversing

Similarly as traversing1 is an alias to wander1, traversing is an alias to wander.

traversing :: (forall f. Applicative f => (a -> f b) -> s -> f t)
           -> Traversal s t a b
traversing = wander

operation: traverseOf

Map each element of a structure targeted by a Lens, Traversal1 or Traversal, evaluate these actions from left to right, and collect the results.

-- traverseOf :: Traversal1 s t a b
--            -> (forall f. Applicative f => (a -> f b) -> s -> f t)
traverseOf :: Applicative f
           => Optic (Star f) s t a b
           -> (a -> f b) -> s -> f t
traverseOf = withStar

Note the definition is same as of traverse1Of, the context differs. Star is Traversing only if f is Applicative; and Traversing1 if f is Apply.

operation: partsOf

You may ask: How Traversal s t a b is different from Lens s t [a] [b]? The difference is the same as between AffineTraversal and Lens. Traversal don't let you to remove the elements. We can however write a conversion function

partsOf :: Traversal s s a a -> Lens s s [a] [a]
partsOf o = lens getter setter
  where
    getter s = foldMapOf o (:[]) s
    setter s xs = evalState (traverseOf o (state . fill) s) xs
    fill a []     = (a, [])
    fill _ (a:as) = (a, as)

The note in partsOf documentation in lens package says:

You should really try to maintain the invariant of the number of children in the list.

The implementation will do it for us too, we cannot remove or add elements using partsOf: it will either use old if not given enough or drop excess ones. That is the reason why we can work only with a type-preserving Traversal (in fact we can write a version for Traveral s t a a, but there are still a a, not a b).

λ> view (partsOf traverse') [1,2,3]
[1,2,3]
λ> set (partsOf traverse') [1,2,3] [4,5]
[4,5,3]
λ> set (partsOf traverse') [1,2,3] [4,5,6,7]
[4,5,6]

Fold, Fold1, and Affine Fold

A Fold s a is a generalization of something Foldable. It allows you to extract multiple results from a container.

Fold1 extract at least one result, AffineFold at most one. (Getter exactly one.) Since folds are read-only, there are now laws.

type AffineFold s a
    = forall p. (Strong p, Choice p, Bicontravariant p) => Optic' p s a
type Fold1 s a
    = forall p. (Traversing1 p, Bicontravariant p) => Optic' p s a
type Fold s a
    = forall p. (Traversing p, Bicontravariant p) => Optic' p s a

operation: foldMapOf

foldMapOf :: Optic' (Forget r) s a -> (a -> r) -> s -> r
foldMapOf o f = runForget (o (Forget f))

operation: toListOf

Using foldMapOf is easy to define various folds, toListOf is useful at least for examples:

toListOf :: Optic' (Forget (Endo [a])) s a -> s ->  [a]
toListOf o s = appEndo (foldMapOf o (Endo . (:)) s) []

Note: we use Endo as a difference list, [a] would do it too, but less efficiently.

operation: foldMap1Of

The definition of foldMap1Of is exactly the same as of foldMapOf. If passed in optic uses only Traversing1 constraint, then only the Semigroup r would be required on r in Forget.

operation: preview

preview :: Optic' (ForgetM a) s a -> s -> Maybe a
preview o = runForgetM (o (ForgetM Just))

constructor: folding

folding :: Foldable f => (s -> f a) -> Fold s a
folding f = cimap f (const ()) . wander traverse_

soundness and completeness

Completeness is not as obvious as previously, as here we have to pick some Foldable. List is a safe choice (DList would be more efficient).

fold_complete :: Fold s a -> Fold s a
fold_complete o = folding (toListOf o)

The soundness proof is also complicated. First GHC wants us to annotate the types to resolve ambiguous Foldable and Monoid.

fold_sound_proof :: ()
fold_sound_proof =
    (\(f :: Int -> [Int]) (s :: [Int]) -> foldMapOf (folding id) f s)
    =/=
    (\f s -> foldMap f s)

The proof failed with the following obligation left:

    Simplified LHS
        (\ (f :: Int -> [Int]) (s :: [Int]) ->
           foldr
             @ Int
             @ (Const [Int] ())
             ((\ (x :: Int) -> ++ @ Int (f x)) `cast` ...)
             (([] @ Int) `cast` ...)
             s)
        `cast` ...
    Simplified RHS:
        \ (f :: Int -> [Int]) (s :: [Int]) ->
          foldr
            @ Int
            @ [Int]
            (\ (x :: Int) -> ++ @ Int (f x))
            ([] @ Int)
            s

It's easy to see that the expressions are same, except for the casts. Possibly ghc-proof could erase types (and casts) and compare expressions after that.

constructor: folding1

Similar to folding:

folding1 :: Foldable1 f => (s -> f a) -> Fold1 s a
folding1 f = cimap f (const ()) . wander1 traverse1_

constructor: afolding

Because there isn't a Foldable variant for at most one element containers, we'll use Maybe:

afolding :: (s -> Maybe a) -> AffineFold s a
afolding f = cimap (\s -> maybe (Left s) Right (f s)) Left . right'

Note: we don't use Strong constraint here.

We can freely convert between AffineFold s a and Getter s (Maybe a):

getterToAF, getterToAF' :: Getter s (Maybe a) -> AffineFold s a
getterToAF o = afolding (view o)
getterToAF' o = o . _Just

afToGetter :: AffineFold s a -> Getter s (Maybe a)
afToGetter o = to (preview o)

data type: ForgetM

ForgetM is a variant of Forget with a value wrapped in Maybe. It's used to implement preview.

newtype ForgetM r a b = ForgetM { runForgetM :: a -> Maybe r }

Instance definitions are in the appendix.

Setter

Another top class of an optics hierarchy is a Setter. It's a generalization of fmap from Functor.

type Setter s t a b = forall p. Mapping p => Optic p s t a b

laws

The only Lens law that can apply to a Setter l is that

set l y (set l x a) ≡ set l y a

You can't view a Setter in general, so the other two lens laws are irrelevant.

However, two Functor laws apply to a Setter:

over l id ≡ id
over l f . over l g ≡ over l (f . g)

type class: Mapping

The third in series of Traversable1, Traversable, Functor type classes: is Mapping.

class (Traversing p, Closed p) => Mapping p where
    map' :: Functor f => p a b -> p (f a) (f b)
    map' = roam collect

    roam :: (forall f. (Applicative f,  Distributive f)
         => (a -> f b) -> s -> f t)
         -> p a b -> p s t
    roam = roamMap' map'

    {-# MINIMAL map' | roam #-}

Originally I defined roam using Representable constraint, because I didn't know how to implement setting without it. Turns out, it's possible by using map' as shown in a post in r6research blog.

Applicative constraint isn't strictly necessary, but is required to implement wanderMapping as mentioned in profunctors #50 pull request. Also roamMap' implementation is from that pull request. On the other hand, there is a distributive issue to add Applicative constraint to Distributive anyway.

constructor: setting

setting builds a Setter from a map like function. In my original try, I had to use Representable constraint, as I used index and tabulate. However, r6research shows how to define setting using Context (PStore in the post), without relying on the Representable.

setting :: ((a -> b) -> s -> t) -> Setter s t a b
setting f = dimap (Context id) (\(Context g s) -> f g s) . map'

data Context a b t = Context (b -> t) a deriving Functor

λ> over (setting fmap) (+1) [1,2,3]
[2,3,4]

Context is the indexed store can be used to characterize a Lens, and seems the Setter.

The definition using Representable:

setting :: ((a -> b) -> s -> t) -> Setter s t a b
setting f = roam $ \g s -> tabulate $ \idx ->
    f (flip index idx . g) s

The useful Setter is mapped:

mapped :: Functor f => Setter (f a) (f b) a b
mapped = setting fmap

constructor: collecting

collecting is another name for roam. Name would suggest we'd require only Distributive, but that won't be enough, because of the way we defined Mapping.

collecting
    :: (forall f. (Applicative f, Distributive f) => (a -> f b) -> s -> f t)
    -> Setter s t a b
collecting = roam

operation: over

Modify all targets of the optic with a function. over is specific version of id.

over :: Optic (->) s t a b -> (a -> b) -> s -> t
over = id

operation: set

set :: Optic (->) s t a b -> s -> b -> t
set o s b = over o (const b) s

operation: collectOf

We can also make multiple copies at once. We should be OK with just Distributive, but it's simpler to require Representable.

collectOf :: (Applicative f, Distributive f)
          => Optic (Star (WrappedApplicative f)) s t a b
          -> (a -> f b) -> s -> f t
collectOf o f = unwrapApplicative . runStar (o (Star (WrapApplicative . f)))

soundness and completeness

setter_complete :: Setter s t a b -> Setter s t a b
setter_complete = setting . over

In soundness proof, we have to eta-expand g:

setter_sound_proof :: ()
setter_sound_proof =
    (\f g s -> over (setting f) g s)
    ===
    (\f g s -> f (\x -> g x) s)

Another way is to say that collectOf and collecting are the basic operations:

setter_complete_2 :: Setter s t a b -> Setter s t a b
setter_complete_2 o = collecting (collectOf o)

Stating soundness property is quite complicated (as with traversals), so we omit it.

Indexed optics

Indexed optics are possible in the profunctor encoding. The first step is to notice is that the index is an additional information we extract from the bigger value, so we can encode indexed optics as Optic p s t (i, a) b.

purescript-profunctor-lenses uses a newtype, so will we too:

newtype Indexed p i a b = Indexed { runIndexed :: p (i, a) b }

type IndexedOptic p i s t a b = Indexed p i a b -> p s t
type IndexedOptic' p i s a = IndexedOptic p i s s a a

Instances and simple operations are easy to define:

itraversing :: Traversing p
            => (forall f. Applicative f => (i -> a -> f b) -> s -> f t)
            -> IndexedOptic p i s t a b
itraversing itr (Indexed pab) = wander (\f s -> itr (curry f) s) pab

ifoldMapOf :: IndexedOptic' (Forget r) i s a -> (i -> a -> r) -> s -> r
ifoldMapOf o f = runForget (o (Indexed (Forget (uncurry f))))

The problematic part is the indexed optic composition: icompose (<.> clashes with the Apply operation). Conceptually the operation is simple, second optic should just pass the first index through:

Writing the actual definition is simple (only?) if you know the right type:

icompose :: Profunctor p
         => (i -> j -> k)
         -> (Indexed p i u v -> p s t)
         -> (Indexed (Indexed p i) j a b -> Indexed p i u v)
         -> (Indexed p k a b -> p s t)
icompose ijk stuv uvab ab = icompose' ijk
    (stuv . Indexed)
    (runIndexed . uvab . Indexed . Indexed)
    (runIndexed ab)

icompose' :: Profunctor p
          => (i -> j -> k)
          -> (p (i, u) v -> p s t)
          -> (p (i, (j, a)) b -> p (i, u) v)
          -> (p (k, a) b -> p s t)
icompose' ijk stuv uvab ab = stuv (uvab (lmap f ab))
  where
    f (i, (j, a)) = (ijk i j, a)

I conclude this section by showing an example, with an indexed list traversal:

itraverseList :: Applicative f => (Int -> a -> f b) -> [a] -> f [b]
itraverseList f = go 0
  where
    go _ []     = pure []
    go i (a:as) = (:) <$> f i a <*> go (i + 1) as

itraversedList :: Traversing p => IndexedOptic p Int [a] [b] a b
itraversedList = itraversing itraverseList

we can extract indexes in nested lists too:

λ> let xss = [[1,2],[3,4,5]]
λ> let o = icompose (,) itraversedList itraversedList
λ> ifoldMapOf o (\ij a -> [(ij, a)]) xss
[((0,0),1),((0,1),2),((1,0),3),((1,1),4),((1,2),5)]

A concrete optic

The operations presented here take optics applied to a concrete Profunctor. For example the Lens operations:

viewP :: Optic (Forget a) s t a b -> s -> a
set   :: Optic (->)       s t a b -> s -> b -> t

(->) is a concrete profunctor for Setter, and Forget for the Getter. What does the concrete Lens looks like? Let's take the lens operations, and put them into the record:

data Shop a b s t = Shop
    { shopGetter :: s -> a
    , shopSetter :: s -> b -> t
    }

Note that the argument pairs are flipped. Shop is a Strong profunctor (instances). Recall that profunctor optics transform profunctors: p a b -> p s t. If p is Shop a b, then an optic will transform Shop a b a b into Shop a b s t, from which we can extract lens operations!

type ALens s t a b = Optic (Shop a b) s t a b

cloneLens :: ALens s t a b -> Lens s t a b
cloneLens o = lens getter setter where
    Shop getter setter = o (Shop id (\_ -> id))

Note: cloneLens is a Rank1Type variant of lens_complete function. Here we get both Lens operations in one go.

But why is ALens useful? In Haskell we cannot put Lens directly into a container (we'd need impredicative types); we'll need either wrap Lens into a newtype or alternatively we can use ALens variant. Neither variant is composable, but ALens approach is simple, as we don't need to explicitly wrap the optic:

afirst :: ALens (a, c) (b, c) a b
afirst = first'

As JavaScript is dynamic language, there is no need for an optic, as we can put whatever values in whatever container. However, in a static typed language they are often needed.

operation: re

The re operation turns or rotates optics.

re :: Optic (Re p a b) s t a b -> Optic p b a t s
re o = runRe (o (Re id))

The Re type, and its instances witness the symmetry of Profunctor and the relation between Bifunctor and Bicontravariant:

newtype Re p s t a b = Re { runRe :: p b a -> p t s }

instance Profunctor p => Profunctor (Re p s t) where
    dimap f g (Re p) = Re (p . dimap g f)

instance Bifunctor p => Bicontravariant (Re p s t) where
    cimap f g (Re p) = Re (p . bimap g f)

instance Bicontravariant p => Bifunctor (Re p s t) where
    bimap f g (Re p) = Re (p . cimap g f)

However there Choice and Strong aren't related in the same way as Bifunctor and Bicontravariant. If you rotate Prism, you don't get Lens:

To make Review and Getter invertible (not only Prim variants), we need two new type classes:

class Profunctor p => Costrong p where
    unfirst :: p (a, d) (b, d) -> p a b
    unfirst = unsecond . dimap swap swap

    unsecond :: p (d, a) (d, b) -> p a b
    unsecond = unfirst . dimap swap swap

class Profunctor p => Cochoice p where
    unleft :: p (Either a d) (Either b d) -> p a b
    unleft = unright . dimap swapE swapE

    unright :: p (Either d a) (Either d b) -> p a b
    unright = unleft . dimap swapE swapE

The instances are in the appendix.

We can prove per optic type and operation that re . re = id.

rere_id_lens_set_proof :: ()
rere_id_lens_set_proof =
    (\getter setter s b -> set (lens getter setter) s b)
    ===
    (\getter setter s b -> set (re (re (lens getter setter))) s b)

Interesting question arises: what is Cotraversing? I don't know.

Inverting Prism

After noting the reset in the bennofs' lpaste, I realised we can try to rotate Prism into Lens:

rePrism :: Prism s t a b -> Lens b a t s
rePrism o = lens (reviewP o) (reset o)

reset :: Optic (Re (->) a b) s t a b -> b -> s -> a
reset = set . re

reover :: Optic (Re (->) a b) s t a b -> (t -> s) -> (b -> a)
reover = over . re

but there's a gotcha:

λ> :t set (rePrism right')
set (rePrism right') :: s -> Either c t -> t

if we try to set rePrism right' with Left value, it will loop. Converting Lens to Prism is similarly problematic,

type class: Closed

The profunctor library defines Closed type class. And it seems to be useful in the optics context too: http://r6research.livejournal.com/28050.html. The support for Grate was recently added to purescript-profunctor-optics.

A strong profunctor allows the monoidal structure to pass through.

A closed profunctor allows the closed structure to pass through.

class Profunctor p => Closed p where
    closed :: p a b -> p (x -> a) (x -> b)
    closed = grate f
      where
        f :: (((x -> a) -> a) -> b) -> x -> b
        f g x = g ($ x)

    grate :: (((s -> a) -> b) -> t) -> p a b -> p s t
    grate f = dimap (flip ($)) f . closed

    {-# MINIMAL closed | grate #-}

Using Closed we can define a new optic, Grate:

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

On way to understand where it's useful, is through associated container class: Distributive.

To be distributive a container will need to have a way to consistently zip a potentially infinite number of copies of itself. This effectively means that the holes in all values of that type, must have the same cardinality, fixed sized vectors, infinite streams, functions, etc. and no extra information to try to merge together.

The actual constructor are either grate or closed, yet we can define some helpful constructors:

cotraversed :: Distributive f => Grate (f a) (f b) a b
cotraversed = grate $ \f -> cotraverse f id

represented :: Representable f => Grate (f a) (f b) a b
represented = dimap index tabulate . closed

One way to use Grate is to review them, for example:

_V2 :: Grate (V2 a) (V2 b) a b
_V2 = represented

λ> review (_V2 . right' . _V2) 1 :: V2 (Either Bool (V2 Int))
V2 (Right (V2 1 1)) (Right (V2 1 1))

λ> over _V2 (+1) (V2 1 2) :: V2 Int
V2 2 3

data type: Zipping

Another use is to zip containers, using Zipping (which is Costar V2, except we can define more instances).

newtype Zipping a b = Zipping { runZipping :: a -> a -> b }

operation: zipWithOf

zipWithOf :: Optic Zipping s t a b -> (a -> a -> b) -> s -> s -> t
zipWithOf o f = runZipping (o (Zipping f))

Zipping is also Choice and Strong, so we can zip inside structures:

λ> let as = V2 (Left ())     (Right (1,2))
λ> let bs = V2 (Right (3,4)) (Right (5,6))
λ> zipWithOf (_V2 . right' . first') (,) as bs
V2 (Left ()) (Right ((1,5),2))

With Prism, non-matching elements are taking from the first argument. In Lens case "left-over" part is also taken from the first argument.

Note: we can zipWithOf only containers with the same element type. And of the same size, so it's combination of zipWith and alignWith (from these package).

Note: I think it's possible to implement both variants: common zipWithOf and alignWithOf using Traversal, using State trick as in partsOf: Pick the shorter or longer container and zip/align into it. That won't work with infinite structures.

type class: Monoidal

There is at least one more, not well know profunctor class Monoidal. It's used in opaleye (as ProductProfunctor, author seems want to remove empty and ***!, yet I do want to use them).

class Profunctor p => Semigroupal p where
    mult :: p a b -> p c d -> p (a, c) (b, d)

class Semigroupal p => Monoidal p where
    unit :: p () ()

We can define a variant of _V2 using Semigroupal (I have a strong tempation to call an optic using Monoidal, a Monocle; yet the Stereographic (glasses) is conceptually more correct).

v2 :: Semigroupal p => Optic p (V2 a) (V2 b) a b
v2 p = dimap (\(V2 x y) -> (x, y)) (\(x, y) -> V2 x y) (mult p p)

With new v2 the examples in Closed section work, both review

λ> review (v2 . right' . _V2) 1 :: V2 (Either Bool (V2 Int))
V2 (Right (V2 1 1)) (Right (V2 1 1))

and zipWithOf:

λ> let as = V2 (Left ())     (Right (1,2))
λ> let bs = V2 (Right (3,4)) (Right (5,6))
λ> zipWithOf (v2 . right' . first') (,) as bs
V2 (Left ()) (Right ((1,5),2))

But also traverseOf:

λ> let f x = state (\s -> (x + s, s +1))
λ> evalState (traverseOf v2 f (V2 5 7)) 1
V2 6 9

and toListOf:

λ> toListOf (v2 . v2) (V2 (V2 1 2) (V2 3 4))
[1,2,3,4]

In the "Modular Data Access" Monoidal is used to implement Traversal; yet it's not enough alone: you have to add Choice (which is called Cocartesian there) to deal with not Representable containers (we have to check whether it's empty or not). as well as Strong to let extra content information pass through. This is OK for Traversal, but not ok for Traversal1, which is Choiceless optic.

As I don't understood Grate or Monoidal, I don't know where to put them in the graph. If we look at the instances:

One way to see the subtle difference between Monoidal + Strong + Choice and Traversing is try to define a traversedList (without relying on Choice):

traversedList :: (Strong p, Monoidal p)
              => Optic p [a] [b] a b
traversedList pab = _

It should be possible, but is far from straight forward: Strong is required there, hint:

Yet, I don't see any practical benefit: every Choice in the table below is also a Monoidal, we don't get anything by not requiring Choice for Traversing like operation.

	`Forget`	`Star`	`Tagged`	`Zipping`
`Bifunctor`	no	no	yes	no
`Bicontravariant`	yes	no	no	no
`Choice`	yes	yes	yes	yes
`Strong`	yes	yes	no	yes
`Closed`	yes	no	yes	yes
`Monoidal`	yes	yes	yes	yes

van Laarhoven encoding

There're another ways to encode optics using type-classes, other than profunctor one presented in this post. van Laarhoven style lenses give rise to two ways to encode optics: Profunctor + Functor = OpticEK used in Edward Kmett's lens and Functor + Functor = OpticVL as showed in r6reseach blog post:

type OpticP  c   s t a b  =
    forall p.    c p        => p a b        -> p s t
type OpticEK c c' s t a b =
    forall p f. (c p, c' f) => p a (f b)    -> p s (f t)
type OpticVL c c' s t a b =
    forall f g. (c f, c' g) => (g a -> f b) -> g s -> f t

The OpticEK variant is expressive and well understood, lens library is an emperical evidence. The encoding is practical: in the Strong part of the hierarchy p is a function arrow (->). Therefore Strong optics are of the form forall f. c f => (a - > f b) -> s -> f t, as a consequence lenses (c = Functor) and traversals (c = Applicative) can be defined in the libraries without dependency on the lens library. In additon, indexed optics are there as well, in more ergonomic way (Profunctor variant needs Indexable analogue to be able to talk about p and Indexed p i in an uniform way, when you don't care). See Edwards reply for more info.

The another variant, OpticVL looks suspicious (and I'm not familiar with it at all), but it seems you can do about anything with it as well. Let's explore the IsoVL and PrismVL. First we define a bit different (but practical) alias:

type OpticVL g f s t a b = (g a -> f b) -> g s -> f t

IsoVL

To form an isomorphism we require that f and g to be Functors:

type IsoVL s t a b =
    forall f g. (Functor g, Functor f) => OpticVL g f s t a b

The constructor definition is guided by the types:

isoVL :: (s -> a) -> (b -> t) -> IsoVL s t a b
isoVL getter setter gafb gs = setter <$> gafb (getter <$> gs)

To viewVL and reviewVL we instantiate the functor arguments with Identity and Const (and vice versa). The definitions are elegantly symmetric:

viewVL :: OpticVL Identity (Const a) s t a b -> s -> a
viewVL o s = getConst (o (Const . runIdentity) (Identity s))

reviewVL :: OpticVL (Const b) Identity s t a b -> b -> t
reviewVL o b = runIdentity (o (Identity . getConst) (Const b))

As before, we can state completeness and soundness equations for these operations:

isoVL_complete :: IsoVL s t a b -> IsoVL s t a b
isoVL_complete o = isoVL (viewVL o) (reviewVL o)

and GHC proves some of them for us:

isoVL_sound1_proof :: ()
isoVL_sound1_proof =
    (\getter setter s -> viewVL (isoVL getter setter) s)
    ===
    (\getter _setter s -> getter s)

isoVL_sound2_proof :: ()
isoVL_sound2_proof =
    (\getter setter b -> reviewVL (isoVL getter setter) b)
    ===
    (\_getter setter b -> setter b)

PrismVL

The encoding of Prism in two Functor form is not trivial:

type PrismVL s t a b =
    forall f g. (CostrongSum g, Functor f, Pointed f) => OpticVL g f s t a b

Pointed f is not a surprise (if you read my post about affine traversal); the CostrongSum might be. It's a type inspired by another r6research blog post (haskell-cafe post, and Gershom B. reply). which let's us to undo StrongSum's distRight (i.e. point from Pointed).

class Functor f => CostrongSum f where
    codistRight :: f (Either a b) -> Either a (f b)

instance CostrongSum (Const r) where
    codistRight (Const r) = Right (Const r)

instance CostrongSum Identity where
    codistRight = either Left (Right . Identity) . runIdentity

Now we have the right tools to define the prismVL constructor:

prismVL :: (b -> t) -> (s -> Either t a) -> PrismVL s t a b
prismVL setter getter gafb gs =
     either point (fmap setter . gafb) (codistRight (getter <$> gs))

The second of PrismVL operations is previewVL:

previewEVL :: OpticVL Identity (Either a) s t a b -> s -> Either t a
previewEVL o s = swapE (o (Left . runIdentity) (Identity s))

And again we can write completeness and soundness expressions:

prismVL_complete :: PrismVL s t a b -> PrismVL s t a b
prismVL_complete p = prismVL (reviewVL p) (previewEVL p)

prismVL_sound1_proof :: ()
prismVL_sound1_proof =
    (\getter setter s -> previewEVL (prismVL setter getter) s)
    ===
    (\getter _setter s -> getter s)

prismVL_sound2_proof :: ()
prismVL_sound2_proof =
    (\getter setter b -> reviewVL (prismVL setter getter) b)
    ===
    (\_getter setter b -> setter b)

I can conclude with a bare definition of LensVL, leaving implementing lensVL as an exercise for the reader:

type LensVL s t a b =
    forall f g. (CostrongProduct g, Functor f) => OpticVL g f s t a b

where yet another new non-standard class is:

class Functor f => CostrongProduct f where
    distPair :: f (a, b) -> (a, f b)

or you can just use g ~ Identity.

Appendix: Some optics

_Just :: Prism (Maybe a) (Maybe b) a b
_Just = dimap (maybe (Left ()) Right) (either (const Nothing) Just) . right'

Appendix: Instances

Tagged

instance Profunctor Tagged where
    dimap _ g (Tagged b) = Tagged (g b)

instance Choice Tagged where
    right' (Tagged b) = Tagged (Right b)

instance Bifunctor Tagged where
    bimap _ g (Tagged b) = Tagged (g b)

instance Closed Tagged where
    closed (Tagged b) = Tagged (const b)

instance Semigroupal Tagged where
    mult (Tagged a) (Tagged b) = Tagged (a, b)

instance Monoidal Tagged where
    unit = Tagged ()

Function, (->)

instance Profunctor (->) where
    dimap f g p = g . p . f

instance Choice (->) where
    right' f = either Left (Right . f)

instance Strong (->) where
    first' f (a, c) = (f a, c)

instance Closed (->) where
    closed f xa x = f (xa x)

instance Traversing1 (->) where
    wander1 f g s = runIdentity (f (Identity . g) s)

instance Traversing (->) where
    wander f g s = runIdentity (f (Identity . g) s)

instance Mapping (->) where
    roam f g s = runIdentity (f (Identity . g) s)

instance Semigroupal (->) where
    mult = bimap

instance Monoidal (->) where
    unit = id

instance Cochoice (->) where
    unright f = go . Right where go = either (go . Left) id . f

instance Costrong (->) where
    unfirst f a = b where (b, d) = f (a, d)

Star

instance Functor f => Profunctor (Star f) where
    dimap f g (Star p) = Star (fmap g . p . f)

-- | definition using firstTraversing would require Apply constraint
instance Functor f => Strong (Star f) where
    first' (Star p) = Star $ (\(a,c) -> fmap (,c) (p a))

instance (Functor f, Pointed f) => Choice (Star f) where
    right' (Star p) = Star (either (point . Left) (fmap Right . p))

instance Apply f => Traversing1 (Star f) where
    wander1 f (Star p) = Star (f p)

instance (Applicative f, Apply f, Pointed f) => Traversing (Star f) where
    wander f (Star p) = Star (f p)

instance Distributive f => Closed (Star f) where
    closed (Star afb) = Star (\xa -> distribute (\x -> afb (xa x)))

-- | We /could/ define `StarCo f a b = StarCo (a -> Co f b)`
-- to use only `Representable` constraint
instance (Apply f, Pointed f, Applicative f, Distributive f) => Mapping (Star f) where
    roam f (Star p) = Star (f p)

instance Apply f => Semigroupal (Star f) where
    mult (Star f) (Star g) = Star (\(x, y) -> (,) <$> f x <.> g y)

instance (Apply f, Applicative f) => Monoidal (Star f) where
    unit = Star (\_ -> pure ())

Forget

instance Profunctor (Forget r) where
    dimap f _ (Forget p) = Forget (p . f)

instance Strong (Forget r) where
    first' (Forget p) = Forget (p . fst)

instance Bicontravariant (Forget r) where
    cimap f _ (Forget p) = Forget (p . f)

-- | We could use `Default` with `def` here
-- Then we should require that if `r` is `Monoid`, then `def = mempty`.
instance Monoid r => Choice (Forget r) where
    right' (Forget p) =  Forget (either (const mempty) p)

instance Semigroup r => Traversing1 (Forget r) where
    wander1 f (Forget p) = Forget (getConst . f (Const . p))

instance (Semigroup r, Monoid r) => Traversing (Forget r) where
    wander f (Forget p) = Forget (getConst . f (Const . p))

instance Semigroup r => Semigroupal (Forget r) where
    mult (Forget p) (Forget q) = Forget (\(x, y) -> p x <> q y)

instance (Semigroup r, Monoid r) => Monoidal (Forget r) where
    unit = Forget (\_ -> mempty)

ForgetM

instance Profunctor (ForgetM r) where
    dimap f _ (ForgetM p) = ForgetM (p . f)

instance Bicontravariant (ForgetM r) where
    cimap f _ (ForgetM p) = ForgetM (p . f)

instance Choice (ForgetM r) where
    right' (ForgetM p) = ForgetM (either (const Nothing) p)

instance Strong (ForgetM r) where
    first' (ForgetM p) = ForgetM (p . fst)

ForgetE

is a Strong Choice.

instance Profunctor (ForgetE r) where
    dimap f g (ForgetE p) = ForgetE (first g . p . f)

instance Choice (ForgetE r) where
    right' (ForgetE p) = ForgetE (unassocE . fmap p)

unassocE :: Either a (Either b c) -> Either (Either a b) c
unassocE (Left a)          = Left (Left a)
unassocE (Right (Left b))  = Left (Right b)
unassocE (Right (Right c)) = Right c

instance Strong (ForgetE r) where
    first' (ForgetE p) = ForgetE (\(a,c) -> first (,c) (p a))

instance Costrong (ForgetE r) where
    unfirst (ForgetE f) =
       ForgetE (first fst . f . (, error "Costrong ForgetE"))

Either and pair

instance Bifunctor Either where
    bimap f _ (Left x)  = Left (f x)
    bimap _ g (Right y) = Right (g y)

instance Bifunctor (,) where
    bimap f g (x, y) = (f x, g y)

Re

instance Cochoice p => Choice (Re p s t) where
    right' (Re p) = Re (p . unright)

instance Costrong p => Strong (Re p s t) where
    first' (Re p) = Re (p . unfirst)

instance Choice p => Cochoice (Re p s t) where
    unright (Re p) = Re (p . right')

instance Strong p => Costrong (Re p s t) where
    unfirst (Re p) = Re (p . first')

Indexed

instance Profunctor p => Profunctor (Indexed p i) where
    dimap f g (Indexed p) = Indexed (dimap (fmap f) g p)

instance Strong p => Strong (Indexed p i) where
    first' (Indexed p) = Indexed (lmap unassoc (first' p))

unassoc :: (a,(b,c)) -> ((a,b),c)
unassoc (a,(b,c)) = ((a,b),c)

instance Choice p => Choice (Indexed p i) where
    left' (Indexed p) = Indexed $
        lmap (\(i, e) -> first (i,) e) (left' p)

instance Traversing1 p => Traversing1 (Indexed p i) where
    wander1 f (Indexed p) = Indexed $
         wander1 (\g (i, s) -> f (curry g i) s) p

instance Traversing p => Traversing (Indexed p i) where
    wander f (Indexed p) = Indexed $
         wander (\g (i, s) -> f (curry g i) s) p

Zipping

instance Profunctor Zipping where
    dimap f g (Zipping p) = Zipping (\x y -> g (p (f x) (f y)))

instance Closed Zipping where
    closed (Zipping p) = Zipping (\f g x -> p (f x) (g x))

instance Choice Zipping where
    right' (Zipping p) = Zipping (\x y -> p <$> x <*> y)

instance Strong Zipping where
    first' (Zipping p) = Zipping (\(x, c) (y, _) -> (p x y, c))

instance Semigroupal Zipping where
    mult (Zipping p) (Zipping q) = Zipping (\(a,b) (c,d) -> (p a c, q b d))

instance Monoidal Zipping where
    unit = Zipping (\_ _ -> ())

Shop

instance Profunctor (Shop x y) where
    dimap f g (Shop getter setter) = Shop
        { shopGetter = getter . f
        , shopSetter = \a y -> g (setter (f a) y)
        }

instance Strong (Shop x y) where
    first' (Shop getter setter) = Shop
        { shopGetter = getter . fst
        , shopSetter = \(a, c) y -> (setter a y, c)
        }

Orphans

instance Pointed V2 where
    point = pure

instance Representable f => Pointed (Co f) where
    point x = Co (tabulate (const x))

Appendix: Auxiliary functions and types

roamMap'

Implementation by David Feuer from profunctors #50.

roamMap' :: Profunctor p
         => (forall f. Functor f => p a b -> p (f a) (f b))  -- ^ map'
         -> (forall f. (Distributive f, Applicative f)
                     => (a -> f b) -> s -> f t)
         -> p a b -> p s t
roamMap' m f = dimap (\s -> Bar $ \afb -> f afb s) lent . m
  where
    lent :: Bar t a a -> t
    lent m = runIdentity (runBar m Identity)

newtype Bar t b a = Bar
   { runBar :: forall f. (Distributive f, Applicative f)
            => (a -> f b) -> f t
   }
   deriving Functor

WrappedApplicative

Used to implement collectOf without Pointed and Apply constraints.

newtype WrappedApplicative f a =
    WrapApplicative { unwrapApplicative :: f a }
    deriving Functor

instance Applicative f => Pointed (WrappedApplicative f) where
    point = WrapApplicative . pure

instance Applicative f => Apply (WrappedApplicative f) where
    WrapApplicative f <.> WrapApplicative x = WrapApplicative (f <*> x)

instance Applicative f => Applicative (WrappedApplicative f) where
    pure = point
    (<*>) = (<.>)

instance Distributive f => Distributive (WrappedApplicative f) where
    collect f = WrapApplicative . collect (unwrapApplicative . f)

Appendix: Changes

2017-04-19: Reimplemented setting using a version from Mainline Profunctor Heirarchy for Optics.
2017-04-19: Added van Laarhoven encoding section.
2017-04-19: Added Inverting Prism section.

Leave comments in /r/haskell thread

You can run this file with

stack --resolver=nightly-2017-03-01 ghci --ghci-options='-pgmL markdown-unlit'
λ> :l glassery.lhs

fetch the source from https://gist.github.com/phadej/c32503efd3274e83196d549eaae28a1a

twitter github email linkedin stackoverflow strava

Site proudly generated by Hakyll

Introduction

Contents

Practical Optic

Equality

data type: Identical

constructor: simple

Iso

laws

type class: Profunctor

constructor: iso

soundness and completeness

Prism

laws

type class: Choice

constructor: prism

operation: previewE

soundness and completeness

data type: ForgetE

Review

type class: Bifunctor

constructor: upto

operation: review

soundness and completeness

data type: Tagged

Getter

type class: Bicontravariant

constructor: to

operation: view

soundness and completeness

data type: Forget

Lens

laws

type class: Strong

constructor: lens

soundness and completeness

Affine Traversal

laws

constructor: affine

soundness and completeness

Traversal1

laws

type class: Traversing1

constructor: traversing1

operation: traverse1Of

data type: Star

Traversal

laws

type class: Traversing

constructor: traversing

operation: traverseOf

operation: partsOf

Fold, Fold1, and Affine Fold

operation: foldMapOf

operation: toListOf

operation: foldMap1Of

operation: preview

constructor: folding

soundness and completeness

constructor: folding1

constructor: afolding

data type: ForgetM

Setter

laws

type class: Mapping

constructor: setting

constructor: collecting

operation: over

operation: set

operation: collectOf

soundness and completeness

Indexed optics

A concrete optic

operation: re

Inverting Prism

type class: Closed

data type: Zipping

operation: zipWithOf

type class: Monoidal

van Laarhoven encoding

IsoVL