diff options
| author | Gregor Kleen <gkleen@yggdrasil.li> | 2018-12-18 13:51:16 +0100 |
|---|---|---|
| committer | Gregor Kleen <gkleen@yggdrasil.li> | 2018-12-18 13:51:16 +0100 |
| commit | 46ae60eaca841b554ba20c6a2b7a15b43c12b4df (patch) | |
| tree | 0bb06127a0e08e75f8be755f5a5dfb1702b627b6 /edit-lens/src/Control/Lens | |
| parent | b0b18979d5ccd109d5a56937396acdeb85c857aa (diff) | |
| download | incremental-dfsts-46ae60eaca841b554ba20c6a2b7a15b43c12b4df.tar incremental-dfsts-46ae60eaca841b554ba20c6a2b7a15b43c12b4df.tar.gz incremental-dfsts-46ae60eaca841b554ba20c6a2b7a15b43c12b4df.tar.bz2 incremental-dfsts-46ae60eaca841b554ba20c6a2b7a15b43c12b4df.tar.xz incremental-dfsts-46ae60eaca841b554ba20c6a2b7a15b43c12b4df.zip | |
Much ado about nothing
Diffstat (limited to 'edit-lens/src/Control/Lens')
| -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. |
