summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control/Lens
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens/src/Control/Lens')
-rw-r--r--edit-lens/src/Control/Lens/Edit.lhs10
1 files changed, 6 insertions, 4 deletions
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5a60536..5a106c8 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -1,3 +1,4 @@
1\begin{comment}
1\begin{code} 2\begin{code}
2module Control.Lens.Edit 3module Control.Lens.Edit
3 ( Module(..) 4 ( Module(..)
@@ -8,9 +9,10 @@ module Control.Lens.Edit
8 9
9import Control.Edit 10import Control.Edit
10\end{code} 11\end{code}
12\end{comment}
11 13
12\begin{defn}[Zustandsbehaftete Monoidhomomorphismen] 14\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
13Mit 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: 15Gegeben eine 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:
14 16
15\begin{itemize} 17\begin{itemize}
16 \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)$
@@ -26,7 +28,7 @@ type StateMonoidHom s m n = (s, m) -> (s, n)
26\end{defn} 28\end{defn}
27 29
28\begin{defn}[edit-lenses] 30\begin{defn}[edit-lenses]
29Fü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: 31Fü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$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt:
30 32
31\begin{itemize} 33\begin{itemize}
32 \item $(\init_M, \ground_C, \init_N) \in K$ 34 \item $(\init_M, \ground_C, \init_N) \in K$
@@ -41,7 +43,7 @@ Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$
41 43
42Wir 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}}.
43 45
44In 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): 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):
45 47
46\begin{code} 48\begin{code}
47data EditLens c m n where 49data EditLens c m n where
@@ -74,7 +76,7 @@ Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung
74 76
75$$ \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 )$$
76 78
77Durch 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. 79Durch 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.
78\end{defn} 80\end{defn}
79 81
80Es 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.