Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen.
Dabei werden wir sowohl die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen:

\begin{code}
{-# LANGUAGE TypeFamilies
           , FlexibleContexts
           , FlexibleInstances
           , MultiParamTypeClasses
           , FunctionalDependencies
  #-}
-- Allow more complicated type families
{-# LANGUAGE AllowAmbiguousTypes #-}
-- AmbiguousTypes are useful if we expect functions to be called via TypeApplication
{-# LANGUAGE GADTs #-}
-- For allowing constraints on constructors

module Control.Lens.Edit
  ( Module(..)
  , StateMonoidHom
  , HasEditLens(..)
  , EditLens(..)
  ) where
\end{code}

\begin{defn}[Moduln]
Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur:

\begin{itemize}
  \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$
  \item $\forall m \in \Dom M, (e, e^\prime) \in (\partial M)^2 \colon m \cdot (e e^\prime) = (m \cdot e) \cdot e^\prime$
\end{itemize}

und einem Element $\init_M \in \Dom M$, sodass gilt:

$$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$

Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt.

In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen) führen wir neue, isomorphe, Typen ein (\texttt{newtype}-Wrappern)}.
Eine Repräsentierung als Typklasse bietet sich an:

\begin{code}
class Monoid m => Module m where
  type Domain m :: *
  apply :: Domain m -> m -> Maybe (Domain m)
  -- ^ A partial monoid-action of `m` on `Domain m`
  --
  -- prop> m `apply` mempty = m
  -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e'
  init :: Domain m
  -- ^ 'init @m' (TypeApplication) is the initial element of 'm'
  divInit :: Domain m -> m
  -- ^ Calculate a representation of an element of 'Domain m' in 'Del m'
  --
  -- prop> init `apply` divInit m = m
\end{code}
\end{defn}

Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.

\begin{comment}
\begin{defn}[Modulhomomorphismen]
Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir ein Paar $(f, \phi$) bestehend aus Abbildungen $f \colon \Dom M \to \Dom M^\prime$ und $\phi \colon \partial M \to \partial M^\prime$, sodass gilt:
\begin{itemize}
   \item $\phi$ ist ein Monoidhomomorphismus:

      \begin{itemize}
         \item $\phi(1_{\partial M}) = 1_{\partial M^\prime}$
         \item $\forall (e, e^\prime) \in (\partial M)^2 \colon \phi(e e^\prime) = \phi(e) \phi(e^\prime)$
      \end{itemize}
   \item $f$ erhält das initiale Element:

     $$f(\init_M) = \init_N$$
   \item $f$ und $\phi$ sind \emph{kompatibel}:

     $$\forall m \in \Dom M, e \in \partial M \colon f(m \cdot e) = f(m) \cdot \phi(e)$$
\end{itemize}

\begin{code}
{-
data ModuleHom m n where
  ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n
-}
\end{code}
\end{defn}
\end{comment}

\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
Mit einer Menge von Komplementen $C$ und Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen zustandsbehafteten Monoidhomomorphismus wenn sie den folgenden Ansprüchen genügt:

\begin{itemize}
   \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$
   \item Mit $\psi(m, c) = (n, c^\prime)$ und $\psi(m^\prime, c^\prime) = (n^\prime, c^{\prime \prime})$:

     $$\psi(m m^\prime, c) = (n n^\prime, c^{\prime \prime})$$
\end{itemize}

\begin{code}
-- | A stateful monoid homomorphism
type StateMonoidHom s m n = (s, m) -> (s, n)
\end{code}
\end{defn}

\begin{defn}[edit-lenses]
Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$ aus zwei zustandsbehafteten Monoidhomomorphismen $\Rrightarrow \colon C \times \partial M \to C \times \partial N$ und $\Lleftarrow \colon C \time \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt:

\begin{itemize}
  \item $(\init_M, \ground_C, \init_N) \in K$
  \item Für beliebige $m \in \Dom M, n \in \Dom n, \partial m \in \partial M, \partial n \in \partial N, c \in C$ folgt, wenn $m \cdot \partial m$ definiert ist und $\Rrightarrow(c, \partial m) = (c, \partial n)$ gilt:

    \begin{itemize}
      \item $n \cdot \partial n$ ist ebenfalls definiert
      \item $(m \cdot \partial m, c^\prime, n \cdot \partial n) \in K$
    \end{itemize}
  \item Analog für $\Lleftarrow$
\end{itemize}

Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}.

In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\Rrightarrow$ und $\Lleftarrow$ nur auf konsistente Zustände angewandt werden (und somit auch entweder einen konsistenten Zustand erzeugen oder nichtt definiert sind):

\begin{code}
data EditLens c m n where
  EditLens :: (Module m, Module n) => c -> StateMonoidHom c m n -> StateMonoidHom c n m -> EditLens c m n

class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where
  type Complement l :: *
  ground :: l -> Complement l
  -- ^ A default state from 'Complement l'
  propR :: l -> StateMonoidHom (Complement l) m n
  -- ^ Map edits of 'm' to changes of 'n', maintaining some state from 'Complement l'
  propL :: l -> StateMonoidHom (Complement l) n m
  -- ^ Map edits of 'n' to changes of 'm', maintaining some state from 'Complement l'

-- | Inspect the components of an edit lens (e.g. 'EditLens')
instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
  type Complement (EditLens c m n) = c
  ground (EditLens g _ _) = g
  propR  (EditLens _ r _) = r
  propL  (EditLens _ _ l) = l
\end{code}
\end{defn}

\paragraph{Kompatibilität mit bestehenden lens frameworks}

Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt:

\begin{defn}[lenses alá \citeauthor{laarhoven}]
Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur:

$$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$

Durch geschickte Wahl des Funktors\footnote{\texttt{Const} bzw. \texttt{Identity}} $f$ können dann $\searrow \colon m \to n$ und $\nearrow \colon (m \to m) \to (n \to n)$ rekonstruiert werden oder verwandte Strukturen (folds, traversals, …) konstruiert werden.
\end{defn}

Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren.
Und in der Tat, eine Funktion $\text{map} \colon (o \to o) \to \partial o$ für $o \in \{ m, n \}$ würde van Laarhoven-lenses in edit-lenses einbetten.
Die charakteristische Eigenschaft der Betrachtung als edit-lens, nämlich die algebraische Struktur von $\partial o$, würde hierbei jedoch notwendigerweise verloren gehen.

Wegen diesem Argument haben wir entschieden keine Komponierbarkeit (durch $\text{id} \colon a \to a$ und $\circ \colon (b \to c) \to (a \to b) \to (a \to c)$, wie in \cite{lens}) von edit-lenses mit van Laarhoven-lenses anzustreben.