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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen.
Dabei werden wir sowohl 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
-}
\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:
\begin{itemize}
\item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$
\item Mit $\psi(m, c) = (n, c^\prime)$ und $\psi(m^\prime, c^\prime) = (n^\prime, c^{\prime \prime})$:
$$\psi(m m^\prime, c) = (n n^\prime, c^{\prime \prime})$$
\end{itemize}
\begin{code}
-- | A stateful monoid homomorphism
type StateMonoidHom s m n = (s, m) -> (s, n)
\end{code}
\end{defn}
\begin{defn}[edit-lenses]
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:
\begin{itemize}
\item $(\init_M, \ground_C, \init_N) \in K$
\item Für beliebige $m \in \Dom M, n \in \Dom n, \partial m \in \partial M, \partial n \in \partial N, c \in C$ folgt, wenn $m \cdot \partial m$ definiert ist und $\Rrightarrow(c, \partial m) = (c, \partial n)$ gilt:
\begin{itemize}
\item $n \cdot \partial n$ ist ebenfalls definiert
\item $(m \cdot \partial m, c^\prime, n \cdot \partial n) \in K$
\end{itemize}
\item Analog für $\Lleftarrow$
\end{itemize}
Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}.
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):
\begin{code}
data EditLens c m n where
EditLens :: (Module m, Module n) => c -> StateMonoidHom c m n -> StateMonoidHom c n m -> EditLens c m n
class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where
type Complement l :: *
ground :: l -> Complement l
-- ^ A default state from 'Complement l'
propR :: l -> StateMonoidHom (Complement l) m n
-- ^ Map edits of 'm' to changes of 'n', maintaining some state from 'Complement l'
propL :: l -> StateMonoidHom (Complement l) n m
-- ^ Map edits of 'n' to changes of 'm', maintaining some state from 'Complement l'
-- | Inspect the components of an edit lens (e.g. 'EditLens')
instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
type Complement (EditLens c m n) = c
ground (EditLens g _ _) = g
propR (EditLens _ r _) = r
propL (EditLens _ _ l) = l
\end{code}
\end{defn}
\paragraph{Kompatibilität mit bestehenden lens frameworks}
Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt:
\begin{defn}[lenses alá \citeauthor{laarhoven}]
Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur:
$$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$
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.
\end{defn}
Es liegt nun nahe $\nearrow \colon (m \to m) \to (n \to n)$ mit $\Rrightarrow \colon \partial m \to \partial n$ zu identifizieren.
Und in der Tat, eine Funktion $\text{map} \colon (o \to o) \to \partial o$ für $o \in \{ m, n \}$ würde van Laarhoven-lenses in edit-lenses einbetten.
Die charakteristische Eigenschaft der Betrachtung als edit-lens, nämlich die algebraische Struktur von $\partial o$, würde hierbei jedoch notwendigerweise verloren gehen.
Wegen diesem Argument haben wir entschieden keine Komponierbarkeit (durch $\text{id} \colon a \to a$ und $\circ \colon (b \to c) \to (a \to b) \to (a \to c)$, wie in \cite{lens}) von edit-lenses mit van Laarhoven-lenses anzustreben.
|
