diff options
Diffstat (limited to 'edit-lens/src/Control/Edit.lhs')
-rw-r--r-- | edit-lens/src/Control/Edit.lhs | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs index 7be8db4..11f2c12 100644 --- a/edit-lens/src/Control/Edit.lhs +++ b/edit-lens/src/Control/Edit.lhs | |||
@@ -2,6 +2,7 @@ | |||
2 | \begin{code} | 2 | \begin{code} |
3 | module Control.Edit | 3 | module Control.Edit |
4 | ( Module(..) | 4 | ( Module(..) |
5 | , ModuleHom | ||
5 | ) where | 6 | ) where |
6 | \end{code} | 7 | \end{code} |
7 | \end{comment} | 8 | \end{comment} |
@@ -26,12 +27,12 @@ Eine Repräsentierung als Typklasse bietet sich an: | |||
26 | \begin{code} | 27 | \begin{code} |
27 | class Monoid m => Module m where | 28 | class Monoid m => Module m where |
28 | type Domain m :: * | 29 | type Domain m :: * |
29 | apply :: Domain m -> m -> Maybe (Domain m) | 30 | apply :: m -> Domain m -> Maybe (Domain m) |
30 | -- ^ A partial monoid-action of `m` on `Domain m` | 31 | -- ^ A partial monoid-action of `m` on `Domain m` |
31 | -- | 32 | -- |
32 | -- prop> m `apply` mempty = m | 33 | -- prop> m `apply` mempty = m |
33 | -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e' | 34 | -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e' |
34 | init :: Domain m | 35 | initial :: Domain m |
35 | -- ^ 'init @m' (TypeApplication) is the initial element of 'm' | 36 | -- ^ 'init @m' (TypeApplication) is the initial element of 'm' |
36 | divInit :: Domain m -> m | 37 | divInit :: Domain m -> m |
37 | -- ^ Calculate a representation of an element of 'Domain m' in 'Del m' | 38 | -- ^ Calculate a representation of an element of 'Domain m' in 'Del m' |
@@ -42,7 +43,6 @@ class Monoid m => Module m where | |||
42 | 43 | ||
43 | 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. | 44 | 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. |
44 | 45 | ||
45 | \begin{comment} | ||
46 | \begin{defn}[Modulhomomorphismen] | 46 | \begin{defn}[Modulhomomorphismen] |
47 | 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: | 47 | 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: |
48 | \begin{itemize} | 48 | \begin{itemize} |
@@ -61,11 +61,9 @@ Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir | |||
61 | \end{itemize} | 61 | \end{itemize} |
62 | 62 | ||
63 | \begin{code} | 63 | \begin{code} |
64 | {- | 64 | -- | A homomorphism between 'Module's |
65 | data ModuleHom m n where | 65 | data ModuleHom m n where |
66 | ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n | 66 | ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n |
67 | -} | ||
68 | \end{code} | 67 | \end{code} |
69 | \end{defn} | 68 | \end{defn} |
70 | \end{comment} | ||
71 | 69 | ||