Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
where
π
is one ofπ
Profunctor
Iso
Strong
Lens
Choice
Prism
Affine
Modification
(akatraversal0
)Traversing
Traversal
Mapping
Setter
Closed
Grate
Given
o₁ : Optic π₁ A B S T
ando₂ : Optic π₂ S T X Y
, we compose theseo₂ □ 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 ap : Prism S T X Y
would require taking the meet ofChoice P
andStrong P
which isAffine P
. But ideally Lean would display the type asp □ l : Modification A B X Y
.I'm essentially trying to get Lean elaborator to compute the joins on this lattice:
source