1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
\begin{comment}
\begin{code}
module Control.Lens.Edit
( Module(..)
, StateMonoidHom
, HasEditLens(..)
, EditLens(..)
) where
import Control.Edit
\end{code}
\end{comment}
\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
Gegeben eine Menge $C$ von \emph{Komplementen} und zwei 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 \times \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C \in 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 nicht 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}
\subsection{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á 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)$ 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.
|
