summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control/Lens
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2019-06-07 09:08:42 +0200
committerGregor Kleen <gkleen@yggdrasil.li>2019-06-07 09:08:42 +0200
commita29cce747f3717e32231c9a92b40be12832037b6 (patch)
tree70f399682dec8657719eae4358e87cdc24bbf42f /edit-lens/src/Control/Lens
parent9a02751c1e588a5bbb83bb7e543c26486d3079d5 (diff)
downloadincremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.gz
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.bz2
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.xz
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.zip
Finish for submission
Diffstat (limited to 'edit-lens/src/Control/Lens')
-rw-r--r--edit-lens/src/Control/Lens/Edit.lhs12
1 files changed, 6 insertions, 6 deletions
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5cf8662..84216bd 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -12,7 +12,7 @@ import Control.Edit
12\end{comment} 12\end{comment}
13 13
14\begin{defn}[Zustandsbehaftete Monoidhomomorphismen] 14\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
15Gegeben 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 \emph{zustandsbehafteten Monoidhomomorphismus} wenn sie den folgenden Ansprüchen genügt: 15Gegeben 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 \emph{zustandsbehafteten Monoidhomomorphismus}, wenn sie den folgenden Ansprüchen genügt:
16 16
17\begin{itemize} 17\begin{itemize}
18 \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$ 18 \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$
@@ -28,7 +28,7 @@ type StateMonoidHom s m n = (s, m) -> (s, n)
28\end{defn} 28\end{defn}
29 29
30\begin{defn}[edit-lenses] 30\begin{defn}[edit-lenses]
31Für Moduln $M$ und $N$ besteht eine \emph{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: 31Für Moduln $M$ und $N$ besteht eine \emph{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:
32 32
33\begin{itemize} 33\begin{itemize}
34 \item $(\init_M, \ground_C, \init_N) \in K$ 34 \item $(\init_M, \ground_C, \init_N) \in K$
@@ -43,7 +43,7 @@ Für Moduln $M$ und $N$ besteht eine \emph{symmetrische edit-lens} zwischen $M$
43 43
44Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. 44Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}.
45 45
46In 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): 46In 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):
47 47
48\begin{code} 48\begin{code}
49data EditLens c m n where 49data EditLens c m n where
@@ -67,12 +67,12 @@ instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
67\end{code} 67\end{code}
68\end{defn} 68\end{defn}
69 69
70\subsection{Kompatibilität mit bestehenden lens frameworks} 70\subsection{Kompatibilität mit bestehenden lens Frameworks}
71 71
72Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen à la \citeauthor{laarhoven} wie folgt: 72Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen à la \citeauthor{laarhoven} wie folgt:
73 73
74\begin{defn}[lenses à la Laarhoven] 74\begin{defn}[lenses à la Laarhoven]
75Fü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: 75Fü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:
76 76
77$$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$ 77$$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$
78 78
@@ -80,7 +80,7 @@ Durch geschickte Wahl des Funktors\footnote{\texttt{Const m} bzw. \texttt{Identi
80\end{defn} 80\end{defn}
81 81
82Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. 82Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren.
83Und 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. 83In 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.
84Die charakteristische Eigenschaft der Betrachtung als edit-lens, nämlich die algebraische Struktur von $\partial o$, würde hierbei jedoch notwendigerweise verloren gehen. 84Die charakteristische Eigenschaft der Betrachtung als edit-lens, nämlich die algebraische Struktur von $\partial o$, würde hierbei jedoch notwendigerweise verloren gehen.
85 85
86Wegen 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. 86Wegen 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.