diff options
Diffstat (limited to 'edit-lens/src/Control/Lens/Edit.lhs')
-rw-r--r-- | edit-lens/src/Control/Lens/Edit.lhs | 10 |
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} |
2 | module Control.Lens.Edit | 3 | module Control.Lens.Edit |
3 | ( Module(..) | 4 | ( Module(..) |
@@ -8,9 +9,10 @@ module Control.Lens.Edit | |||
8 | 9 | ||
9 | import Control.Edit | 10 | import Control.Edit |
10 | \end{code} | 11 | \end{code} |
12 | \end{comment} | ||
11 | 13 | ||
12 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] | 14 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] |
13 | 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: | 15 | Gegeben 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] |
29 | 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: | 31 | 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$ 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 | ||
42 | Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. | 44 | Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. |
43 | 45 | ||
44 | 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): | 46 | 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): |
45 | 47 | ||
46 | \begin{code} | 48 | \begin{code} |
47 | data EditLens c m n where | 49 | data 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 | ||
77 | 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. | 79 | 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. |
78 | \end{defn} | 80 | \end{defn} |
79 | 81 | ||
80 | Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. | 82 | Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren. |