1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
\begin{comment}
\begin{code}
module Control.Edit
( Module(..)
, ModuleHom
) 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 :: m -> Domain 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'
initial :: 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{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}
-- | A homomorphism between 'Module's
data ModuleHom m n where
ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n
\end{code}
\end{defn}
|
