Definition.idr

The lenses here are “closed” in the sense of cartesian closure, since they are defined using a single function. Where before we had a dependent lens be defined by two map $fwd:a\to b$ and $bwd:(x:a)\to b^{\prime }(fwdx)\to a^{\prime }x$, closed lenses refactor the common argument and make use of a continuation to obtain the resulting $a^{\prime }x$ value: $(x:a)\to \Sigma (y:b).(b^{\prime }y\to a^{\prime }x)$. Here is the idris implementation:

Definition

A closed lens between containers $(A,\bar{A})$ and $(B,\bar{B})$ is a function $(a:A)\to \Sigma (b:B).\bar{B}(b)\to \bar{A}(a)$

public export
record (=&>)(c1, c2 : Container) where
  constructor (!!)
  fn : (x : c1.req) -> Σ (y : c2.req) | c2.res y -> c1.res x

Just like dependent lenses, closed lenses compose in the way we’d expect. It’s worth noting that the performance characteristic of this type are different since we do not need to recompute the forward part to execute the backward map.

public export
(|&>) : a =&> b -> b =&> c -> a =&> c
(|&>) x y = !! \z => let r : ?
                         r = x.fn z
                         s : ?
                         s = y.fn r.π1
                      in s.π1 ## r.π2 . s.π2

Closed lenses also have an identity.

public export
identity : (0 a : Container) -> a =&> a
identity _ = !! \x => x ## id