lens-join/list only follows lens laws when views of args don't overlap

[AlexKnauth]

Fixes lens-join/list for #301, by specifying that the joined lens only follows the lens laws if the views of the argument lenses don't overlap.

[codecov]

Codecov Report

Merging #302 into master will increase coverage by <.01%.
The diff coverage is n/a.

@@            Coverage Diff             @@
##           master     #302      +/-   ##
==========================================
+ Coverage   97.98%   97.98%   +<.01%     
==========================================
  Files         100      100              
  Lines        1736     1741       +5     
==========================================
+ Hits         1701     1706       +5     
  Misses         35       35

Impacted Files	Coverage Δ
lens-data/lens/private/list/join-list.rkt	100% <ø> (ø)	⬆️
lens-data/lens/private/string/string.rkt	100% <0%> (ø)	⬆️
lens-data/lens/private/vector/ref.rkt	100% <0%> (ø)	⬆️
lens-data/lens/private/syntax/syntax.rkt	100% <0%> (ø)	⬆️
lens-common/lens/private/compound/if.rkt	90.9% <0%> (+0.16%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1caa237...122dc30. Read the comment docs.

[jackfirth]

FYI: I'm planning to review this and take care of some other lens maintenance this weekend.

[AlexKnauth]

Ping, do you think you’ll have time to review this this weekend?

[jackfirth]

Pong; I ought to have time for lens this weekend. Taking a look at this now.

[jackfirth]

Two high level comments:

1. The proof is helpful, but it's a bit hard to read as comments mixed in with the implementation code. What if it was a separate lens/private/list/join-list-proof text / markdown file?

2. I think the reason this comes up at all is because lens-join conceptually doesn't cooperate with the lens laws. We can't go safely from (Lens a b, Lens a c) to Lens a (b, c) because we first have to prove the b and c parts of a are independent. I'm not so sure it's a good idea to use it at all. But without isomorphisms, prisms, and traversals I can't think of any good alternatives.

What do you think?

[AlexKnauth]

(Re: 1) I wanted it to be in the same file because it should be "discoverable" to people that just want to change that one file.

(Re: 2) A better alternative might look a bit like isomorphism-join in #300, but with lenses, where the extra condition isn't about lenses being independent, but only about a normal constructor/accessor relationship that might be easier to understand. It separates the "lens"-ness from the potential "overlapping"-ness.

[jackfirth]

Alright, sounds reasonable enough to me. Merging.