Achromatic lens

Posted on 2018-03-28 by Oleg Grenrus lens

Russel O'Connor mentionend on #haskell-lens about Guillaume Boisseau's masters thesis, which mentions Achromatic lenses:

oconnor: Guillaume also has a nice derivation of achromatic lenes.

Because the thesis is not online, we have to guess a little (while waiting for https://2018.programmingconference.org/event/bx-2018-papers-understanding-profunctor-optics-a-representation-theorem).

This is post is my short notes on the topic, it's a brain dump (which type-checks though). More Profunctor Optics.

#Operations

roconnor: A lost of the bidirectional programming folks like a variant of lenses that have get, put, and create.

Achromatic lens has the operations of lens:

but additionally it supports

Or so what the type says. Let's try to implement these functions. We can check from the Glassery that we need PointedCartesian instance for Forget a, (->) and Tagged (for view, over and review respectively).

#Upsert

Three characterizing functions is difficult, so we can get away with two: view and

or even better:

implemented using an auxiliary Profunctor:

Another option is to use isomophic type which is product of (->) and Tagged.

Exercise: Prove that in bicartesian closed category:

 B^A \times B \cong B^{A + 1}

#Constructor

We can create a constructor from view and upsert like functions:

#Example

Let's play with cats:

We can define an achromatic lens into name of a cat:

And then we can write use catName as a constructor, getter or setter:

#Laws

Obviously the Lens laws:

Then we can adopt the first prism (or iso) law:

Note: that second prism law dowsn't hold

with a counterexample

so an achromatic lens is not a prism.

Exercise: Formulate laws using view and upsert.

#Default

roconnor phadej: Guillaume's masters thesis suggests an API where the Default class is used for field types for achromatic lenses.

We can rewrite the example achromatic lens with def from Default.

Because instance Default (Maybe a) where def = Nothing, this variant is the same as above where explicit Nothing is used.

You indeed don't need Eq or anything like that. (I was wrong when you check the IRC logs).

#van Laarhoven

Looks like we have to use PointedCartesian also in van Laarhoven formulation (the one lens library uses) of achromatic lens.

We can define catNameVL achromatic lens as in above examples:

And this definition works with lens library out-of-the-box:

#Appendix

Definitions used above, but which are standard profunctor optics stuff.


This work is licensed under a “CC BY SA 4.0” license.

Site proudly generated by Hakyll