diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2019-06-07 09:08:42 +0200 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2019-06-07 09:08:42 +0200 |
commit | a29cce747f3717e32231c9a92b40be12832037b6 (patch) | |
tree | 70f399682dec8657719eae4358e87cdc24bbf42f /edit-lens/src/Control/Edit.lhs | |
parent | 9a02751c1e588a5bbb83bb7e543c26486d3079d5 (diff) | |
download | incremental-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/Edit.lhs')
-rw-r--r-- | edit-lens/src/Control/Edit.lhs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs index 80c143a..98fa8c4 100644 --- a/edit-lens/src/Control/Edit.lhs +++ b/edit-lens/src/Control/Edit.lhs | |||
@@ -6,10 +6,10 @@ module Control.Edit | |||
6 | \end{code} | 6 | \end{code} |
7 | \end{comment} | 7 | \end{comment} |
8 | 8 | ||
9 | Um das intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen formalisieren wir sie als \emph{Moduln}: | 9 | Um das intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen, formalisieren wir sie als \emph{Moduln}: |
10 | 10 | ||
11 | \begin{defn}[Moduln] | 11 | \begin{defn}[Moduln] |
12 | Ein \emph{Modul} $M$ ist eine partielle Monoidwirkung zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: | 12 | Ein \emph{Modul} $M$ ist eine partielle Monoidwirkung zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger. D.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom M$, die \emph{kompatibel} ist mit der Monoid-Struktur: |
13 | 13 | ||
14 | \begin{itemize} | 14 | \begin{itemize} |
15 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ | 15 | \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$ |
@@ -22,7 +22,7 @@ $$\forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \c | |||
22 | 22 | ||
23 | Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt. | 23 | Wir führen außerdem eine Abbildung $(\init_M \cdot)^{-1} \colon \Dom M \to \partial m$ ein, die ein $m$ auf ein arbiträr gewähltes $\partial m$ abbildet für das $\init_M \cdot \partial m = m$ gilt. |
24 | 24 | ||
25 | In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen) führen wir neue, isomorphe Typen ein (\texttt{newtype}-Wrapper)}. | 25 | In Haskell charakterisieren wir Moduln über ihren Monoid, d.h. die Wahl des Monoiden \texttt{m} legt den Träger \texttt{Domain m}, die Wirkung \texttt{apply}, das initiale Element \texttt{init} und $(\init_M \cdot)^{-1}$ eindeutig fest\footnote{Betrachten wir mehrere Moduln über dem selben Träger (oder mit verschiedenen Wirkungen), führen wir neue, isomorphe Typen ein (\texttt{newtype}-Wrapper)}. |
26 | Eine Repräsentierung als Typklasse bietet sich an: | 26 | Eine Repräsentierung als Typklasse bietet sich an: |
27 | 27 | ||
28 | \begin{code} | 28 | \begin{code} |
@@ -50,7 +50,7 @@ apply' md e = flip apply e =<< md | |||
50 | \end{code} | 50 | \end{code} |
51 | \end{defn} | 51 | \end{defn} |
52 | 52 | ||
53 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv\footnote{$(\init_M \cdot)^{-1}$}) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei. | 53 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} ab, indem wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv\footnote{$(\init_M \cdot)^{-1}$}) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei. |
54 | 54 | ||
55 | \begin{comment} | 55 | \begin{comment} |
56 | \begin{defn}[Modulhomomorphismen] | 56 | \begin{defn}[Modulhomomorphismen] |