Okay, that’s a reasonable ask. In that case, you need the three lens laws (aka. the very well-behaved lens laws): GetPut
, PutGet
, and PutPut
.
-- Suppose there is a lens
get :: s -> a
put :: s -> a -> s
-- satisfying the three laws
GetPut :: forall s. put s (get s) = s
PutGet :: forall s a. get (put s a) = a
PutPut :: forall s a b. put (put s a) b = put s b
Let us recall the definition of the candidate isomorphism:
to :: s -> (a, a -> s)
to s = (get s, put s)
from :: (a, a -> s)
from (a, f) = f a
If we restrict the complement (a -> s)
to exactly the subset of functions that can be obtained by put
, we can show that (to, from)
is an isomorphism. In set comprehension notation:
-- aka. the *image* of put
c = {f :: a -> s | exists s. f = put s}
GetPut
proves the roundtrip from s
to (a, c)
and back.
from (to s) = put s (get s) = s
For the other roundtrip, we start with a pair (a, c)
, where c
is from the image of put
. So we actually start with a pair (a, put s)
.
The from
then to
roundtrip goes:
to (from (a, put s)) = (get (put s a), put (put s a))
The first component simplifies by PutGet
.
get (put s a) = a
The second component simplifies by an eta-reduced reformulation of PutPut
:
put (put s a) = put s
Putting these steps together, the from
-then-to
roundtrip:
to (from (a, put s)) = (a, put s)
Conclusion: to
and from
form an isomorphism between s
and (a, c)
where c = {f :: a -> s | exists s. f = put s}
.
to . from = id
from . to = id
To show that PutPut
is necessary to get an isomorphism, here is a counterexample with a lens that does not satisfy it. Let s
be a type with three elements A | B | C
, and a
be Bool
(two elements).
get :: s -> a
get A = True
get B = False
get C = False
put :: s -> a -> s
put _ True = A
put A False = B
put B False = B
put C False = C
It satisfies GetPut
and PutGet
, but there is no isomorphism between A | B | C
and (Bool, c)
for any c
because 2 does not divide 3.