Refactor

3 files changed, 81 insertions, 77 deletions

diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs
new file mode 100644
index 0000000..7be8db4
--- /dev/null
+++ b/edit-lens/src/Control/Edit.lhs
@@ -0,0 +1,71 @@
+\begin{comment}
+\begin{code}
+module Control.Edit
+  ( Module(..) 
+  ) where
+\end{code}
+\end{comment}
+
+\begin{defn}[Moduln]
+Ein Modul $M$ ist eine \emph{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:
+
+\begin{itemize}
+  \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$
+  \item $\forall m \in \Dom M, (e, e^\prime) \in (\partial M)^2 \colon m \cdot (e e^\prime) = (m \cdot e) \cdot e^\prime$
+\end{itemize}
+
+und einem Element $\init_M \in \Dom M$, sodass gilt:
+
+$$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$
+
+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.
+
+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}-Wrappern)}.
+Eine Repräsentierung als Typklasse bietet sich an:
+
+\begin{code}
+class Monoid m => Module m where
+  type Domain m :: *
+  apply :: Domain m -> m -> Maybe (Domain m)
+  -- ^ A partial monoid-action of `m` on `Domain m`
+  --
+  -- prop> m `apply` mempty = m
+  -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e'
+  init :: Domain m
+  -- ^ 'init @m' (TypeApplication) is the initial element of 'm'
+  divInit :: Domain m -> m
+  -- ^ Calculate a representation of an element of 'Domain m' in 'Del m'
+  --
+  -- prop> init `apply` divInit m = m
+\end{code}
+\end{defn}
+
+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) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.
+
+\begin{comment}
+\begin{defn}[Modulhomomorphismen]
+Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir ein Paar $(f, \phi$) bestehend aus Abbildungen $f \colon \Dom M \to \Dom M^\prime$ und $\phi \colon \partial M \to \partial M^\prime$, sodass gilt:
+\begin{itemize}
+   \item $\phi$ ist ein Monoidhomomorphismus:
+
+      \begin{itemize}
+         \item $\phi(1_{\partial M}) = 1_{\partial M^\prime}$
+         \item $\forall (e, e^\prime) \in (\partial M)^2 \colon \phi(e e^\prime) = \phi(e) \phi(e^\prime)$
+      \end{itemize}
+   \item $f$ erhält das initiale Element:
+
+     $$f(\init_M) = \init_N$$
+   \item $f$ und $\phi$ sind \emph{kompatibel}:
+
+     $$\forall m \in \Dom M, e \in \partial M \colon f(m \cdot e) = f(m) \cdot \phi(e)$$
+\end{itemize}
+
+\begin{code}
+{-
+data ModuleHom m n where
+  ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n
+-}
+\end{code}
+\end{defn}
+\end{comment}
+
diff --git a/edit-lens/src/Control/Edit/Tree.lhs b/edit-lens/src/Control/Edit/Tree.lhs
new file mode 100644
index 0000000..28320c5
--- /dev/null
+++ b/edit-lens/src/Control/Edit/Tree.lhs
@@ -0,0 +1,9 @@
+\begin{comment}
+\begin{code}
+module Control.Edit.Tree
+  (
+  ) where
+
+import Control.Edit
+\end{code}
+\end{comment}
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 7a6cbbe..5a60536 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -1,89 +1,13 @@
-Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen.
-Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen:
-
 \begin{code}
-{-# LANGUAGE TypeFamilies
-           , FlexibleContexts
-           , FlexibleInstances
-           , MultiParamTypeClasses
-           , FunctionalDependencies
-  #-}
--- Allow more complicated type families
-{-# LANGUAGE AllowAmbiguousTypes #-}
--- AmbiguousTypes are useful if we expect functions to be called via TypeApplication
-{-# LANGUAGE GADTs #-}
--- For allowing constraints on constructors
-
 module Control.Lens.Edit
   ( Module(..)
   , StateMonoidHom
   , HasEditLens(..)
   , EditLens(..)
   ) where
-\end{code}
-
-\begin{defn}[Moduln]
-Ein Modul $M$ ist eine \emph{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:
-
-\begin{itemize}
-  \item $\forall m \in \Dom M \colon m \cdot 1_{\partial M} = m$
-  \item $\forall m \in \Dom M, (e, e^\prime) \in (\partial M)^2 \colon m \cdot (e e^\prime) = (m \cdot e) \cdot e^\prime$
-\end{itemize}
-
-und einem Element $\init_M \in \Dom M$, sodass gilt:
-
-$$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \cdot \partial m$$
-
-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.
-
-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}-Wrappern)}.
-Eine Repräsentierung als Typklasse bietet sich an:
-
-\begin{code}
-class Monoid m => Module m where
-  type Domain m :: *
-  apply :: Domain m -> m -> Maybe (Domain m)
-  -- ^ A partial monoid-action of `m` on `Domain m`
-  --
-  -- prop> m `apply` mempty = m
-  -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e'
-  init :: Domain m
-  -- ^ 'init @m' (TypeApplication) is the initial element of 'm'
-  divInit :: Domain m -> m
-  -- ^ Calculate a representation of an element of 'Domain m' in 'Del m'
-  --
-  -- prop> init `apply` divInit m = m
-\end{code}
-\end{defn}
-
-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) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei.
-
-\begin{comment}
-\begin{defn}[Modulhomomorphismen]
-Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir ein Paar $(f, \phi$) bestehend aus Abbildungen $f \colon \Dom M \to \Dom M^\prime$ und $\phi \colon \partial M \to \partial M^\prime$, sodass gilt:
-\begin{itemize}
-   \item $\phi$ ist ein Monoidhomomorphismus:
 
-      \begin{itemize}
-         \item $\phi(1_{\partial M}) = 1_{\partial M^\prime}$
-         \item $\forall (e, e^\prime) \in (\partial M)^2 \colon \phi(e e^\prime) = \phi(e) \phi(e^\prime)$
-      \end{itemize}
-   \item $f$ erhält das initiale Element:
-
-     $$f(\init_M) = \init_N$$
-   \item $f$ und $\phi$ sind \emph{kompatibel}:
-
-     $$\forall m \in \Dom M, e \in \partial M \colon f(m \cdot e) = f(m) \cdot \phi(e)$$
-\end{itemize}
-
-\begin{code}
-{-
-data ModuleHom m n where
-  ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n
--}
+import Control.Edit
 \end{code}
-\end{defn}
-\end{comment}
 
 \begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
 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: