feat: profunctor optics

[EdAyers]

trafficstars

A port of some of https://hackage.haskell.org/package/profunctor-optics-0.0.2/docs/Data-Profunctor-Optic-Traversal.html

Just for fun.

How should composition work?

If anyone has a good idea for how to get optic composition to work smoothly I'd love to hear it!

Currently all optics have the form

def Optic π A B S T := ∀ ⦃P⦄ [c : π P], P A B → P S T

where π is one of

π	optic
Profunctor	Iso
Strong	Lens
Choice	Prism
Affine	Modification (aka traversal0)
Traversing	Traversal
Mapping	Setter
Closed	Grate

Given o₁ : Optic π₁ A B S T and o₂ : Optic π₂ S T X Y, we compose these o₂ □ o₁ : Optic (π₁ ⊓ π₂) A B X Y. Where the meet operation ⊓ is the tricky part that I don't know how to define nicely.

So for example composing a l : Lens A B S T and a p : Prism S T X Y would require taking the meet of Choice P and Strong P which is Affine P. But ideally Lean would display the type as p □ l : Modification A B X Y.

I'm essentially trying to get Lean elaborator to compute the joins on this lattice: source

[bollu]

It's cool to see that optics have a place in mathlib4. Could I have some context for what need they fulfil in the library?

[EdAyers]

They are just interesting on their own really. I was hoping to prove some stuff about lawful optics eventually. I don't know if we are still treating mathlib4 is a monorepo with all lean code in like mathlib3. I guess it could be its own package.