summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens/src/Control')
-rw-r--r--edit-lens/src/Control/Edit.lhs2
-rw-r--r--edit-lens/src/Control/Edit/Container.lhs50
-rw-r--r--edit-lens/src/Control/Lens/Edit.lhs5
-rw-r--r--edit-lens/src/Control/Lens/Edit/Generic.lhs41
4 files changed, 94 insertions, 4 deletions
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs
index 11f2c12..6d9b14c 100644
--- a/edit-lens/src/Control/Edit.lhs
+++ b/edit-lens/src/Control/Edit.lhs
@@ -21,6 +21,8 @@ $$ \forall m \in \Dom M \ \exists \partial m \in \partial M \colon m = \init_M \
21 21
22Wir 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. 22Wir 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 23
24Für ein $\partial m \in \partial M$ schreiben wir für die Menge aller $m \in \Dom M$, sodass $m \cdot \partial m$ definiert ist auch $\Dom (\partial m)$.
25
24In 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)}. 26In 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)}.
25Eine Repräsentierung als Typklasse bietet sich an: 27Eine Repräsentierung als Typklasse bietet sich an:
26 28
diff --git a/edit-lens/src/Control/Edit/Container.lhs b/edit-lens/src/Control/Edit/Container.lhs
index 7d0d57c..32ec479 100644
--- a/edit-lens/src/Control/Edit/Container.lhs
+++ b/edit-lens/src/Control/Edit/Container.lhs
@@ -3,6 +3,7 @@
3module Control.Edit.Container 3module Control.Edit.Container
4 ( Container(..), Shape, Content 4 ( Container(..), Shape, Content
5 , ContainerEdit(..) 5 , ContainerEdit(..)
6 , module Control.Edit
6 ) where 7 ) where
7 8
8import Control.Edit 9import Control.Edit
@@ -16,19 +17,48 @@ import Control.Lens
16\end{code} 17\end{code}
17\end{comment} 18\end{comment}
18 19
20\citeauthor{hofmann2012edit} stellen \emph{container} vor—eine systematische Sicht auf Datenstrukturen, die es erlaubt eine generische edit-language zu definieren.
21
22Intuitiv zerlegt die Darstellung als container eine polymorphe Datenstruktur in ihre \emph{Form} (\emph{shape}), ordnet der Form eine Menge von \emph{Positionen} zu und belegt jede Position mit einem Wert:
23
24\begin{defn}[Container-Typen]
25Ein container-type ist ein Tupel $(I, P, \text{positions})$ aus einem Modul von \emph{shapes} mit partiell geordnetem Träger $\Dom I$, einer Menge von \emph{Positionen} $P$, und einer Abbildung\footnote{In \cite{hofmann2012edit} genannt $\text{live}$} $\text{positions} \colon \Dom I \to \powerset(P)$, die jeder Form eine Menge von Positionen zuordnet, die in einem container jener Form belegt sind.
26
27Wir forden zudem, dass $\text{positions}$ monoton sein soll bzgl. der partiellen Ordnung auf $\Dom I$ und $\subseteq$ auf $\powerset P$\footnote{$\text{positions}$ ist ein Funktor von der Kategorie gegeben durch die Partielle Ordnung auf $\Dom I$ in die Kategorie von Teilmengen von $\powerset(P)$ mit Injektionen als Morphismen}.
28\end{defn}
29
19\begin{defn}[Container] 30\begin{defn}[Container]
31Ein container vom Typ $(I, P, \text{positions})$ mit Werten in $X$ ist ein Tupel $(i, c)$ aus einer Form $i \in \Dom I$ und einer Funktion $c \colon \text{positions}(i) \to X$, die jeder in $i$ vorkommenden Position einen Wert aus $X$ zuweist.
32
33In Haskell sagen wir ein Typ \texttt{c} sei ein container gdw. wir einen Isomorphismus\footnote{Wir verwenden den Typ für Isomorphismen aus \cite[\texttt{Control.Lens.Iso}]{lens}, dessen genau Definition unerheblich ist für diese Arbeit} angeben können zwischen \texttt{c} und Tupeln $(i, c)$ für einen container-typ $(I, P, \text{positions})$.
34
35Hierfür unterdrücken wir den inheränten Polymorphismus von containern zunächst und ordnen stattdessen jedem monomorph instanziierten container-typ \texttt{c} einen Typ \texttt{Content c} zu.
36Polymorphe container können so mit universell quantifizierten Instanzen beschrieben werden.
37
38Wir beschränken uns zudem auf monomorphe container deren Werte-Typ der Träger eines Moduls ist, da dies, als unglückliche Folge unserer charakterisierung von Moduln durch den Typ ihrer edits, für die spätere Definition von container-edits notwendig ist.
39
20\begin{code} 40\begin{code}
21class ( Module (ModShape c) 41class ( Module (ModShape c)
22 , Module (ModContent c) 42 , Module (ModContent c)
23 , Ord (Position c) 43 , Ord (Position c) -- ^ Neccessary to form 'Set's of 'Position's
24 ) => Container c where 44 ) => Container c where
45 -- | Since we characterise 'Module's by the type of their edits we have to associate that type with @c@.
46 -- We later introduce a type synonym for @Domain (ModShape c)@ later.
25 type ModShape c :: * 47 type ModShape c :: *
48
26 type Position c :: * 49 type Position c :: *
50
27 type ModContent c :: * 51 type ModContent c :: *
52 -- ^ Analogous to 'ModShape'
53
54 -- | Compute the live positions of a shape
28 positions :: Shape c -> Set (Position c) 55 positions :: Shape c -> Set (Position c)
56
57 -- | Convert between the natural representation @c@ and a view as container, that is a 'Shape c' and a value function
29 deconstructed :: Iso' c (Shape c, Position c -> Content c) 58 deconstructed :: Iso' c (Shape c, Position c -> Content c)
30 59
31constructed :: Container c => Iso' (Shape c, Position c -> Content c) c 60constructed :: Container c => Iso' (Shape c, Position c -> Content c) c
61-- ^ Inverse of 'deconstructed', for convenience
32constructed = from deconstructed 62constructed = from deconstructed
33 63
34type Shape c = Domain (ModShape c) 64type Shape c = Domain (ModShape c)
@@ -36,19 +66,33 @@ type Content c = Domain (ModContent c)
36\end{code} 66\end{code}
37\end{defn} 67\end{defn}
38 68
69\begin{defn}[Klassifikation von edits auf shapes]
70Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edits $\partial i \in \partial I$ wie folgt:
71
72\begin{description}
73 \item[insertions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \geq i$
74 \item[deletions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \leq i$
75 \item[rearrangements] $\forall i \in \Dom (\partial i) \colon \size{\text{positions}(i \cdot \partial i)} = \size{\text{positions}(i)}$
76\end{description}
77\end{defn}
78
39\begin{defn}[container-edits] 79\begin{defn}[container-edits]
80 TODO
40\begin{code} 81\begin{code}
41data ContainerEdit c where 82data ContainerEdit c where
42 Fail :: ContainerEdit c 83 Fail :: ContainerEdit c
43 ModContent :: Position c -> ModContent c -> ContainerEdit c 84 ModContent :: Position c -> ModContent c -> ContainerEdit c
44 ModShape :: ModShape c -> (Shape c -> Position c -> Position c) -> ContainerEdit c 85 ModShape :: ModShape c -> (Shape c -> Position c -> Position c) -> ContainerEdit c
86
87type ContainerEdits c = Seq (ContainerEdit c)
45\end{code} 88\end{code}
46\end{defn} 89\end{defn}
47 90
48\begin{defn}[Wirkung von container-edits] 91\begin{defn}[Wirkung von container-edits]
92 TODO
49\begin{code} 93\begin{code}
50instance Container c => Module (Seq (ContainerEdit c)) where 94instance Container c => Module (ContainerEdits c) where
51 type Domain (Seq (ContainerEdit c)) = c 95 type Domain (ContainerEdits c) = c
52 apply fs = over mapped (view constructed) . flip (foldM apply') fs . view deconstructed 96 apply fs = over mapped (view constructed) . flip (foldM apply') fs . view deconstructed
53 where 97 where
54 apply' :: Container c 98 apply' :: Container c
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5a60536..0a679cb 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -1,13 +1,16 @@
1\begin{comment}
1\begin{code} 2\begin{code}
2module Control.Lens.Edit 3module Control.Lens.Edit
3 ( Module(..) 4 ( Module(..)
4 , StateMonoidHom 5 , StateMonoidHom
5 , HasEditLens(..) 6 , HasEditLens(..)
6 , EditLens(..) 7 , EditLens(..)
8 , module Control.Edit
7 ) where 9 ) where
8 10
9import Control.Edit 11import Control.Edit
10\end{code} 12\end{code}
13\end{comment}
11 14
12\begin{defn}[Zustandsbehaftete Monoidhomomorphismen] 15\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
13Mit 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: 16Mit 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:
@@ -45,7 +48,7 @@ In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\R
45 48
46\begin{code} 49\begin{code}
47data EditLens c m n where 50data EditLens c m n where
48 EditLens :: (Module m, Module n) => c -> StateMonoidHom c m n -> StateMonoidHom c n m -> EditLens c m n 51 EditLens :: c -> StateMonoidHom c m n -> StateMonoidHom c n m -> EditLens c m n
49 52
50class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where 53class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where
51 type Complement l :: * 54 type Complement l :: *
diff --git a/edit-lens/src/Control/Lens/Edit/Generic.lhs b/edit-lens/src/Control/Lens/Edit/Generic.lhs
new file mode 100644
index 0000000..9dd1b78
--- /dev/null
+++ b/edit-lens/src/Control/Lens/Edit/Generic.lhs
@@ -0,0 +1,41 @@
1\begin{comment}
2\begin{code}
3module Control.Lens.Edit.Generic
4 ( idEL, compEL
5 ) where
6
7import Control.Edit
8import Control.Lens.Edit
9
10import Control.Lens
11\end{code}
12\end{comment}
13
14Wir übernehmen einige der in \cite{hofmann2012edit} vorgestellten Konstruktionen für generische edit-lenses.
15
16Zunächst bilden edit-lenses die Morphismen einer Kategorie vermöge folgender Konstruktionen:
17
18\begin{defn}[Identität von edit-lenses]
19 Blub % TODO
20\begin{code}
21idEL :: EditLens () a a
22idEL = EditLens () (over _2 id) (over _2 id)
23\end{code}
24\end{defn}
25
26\begin{defn}[Komposition von edit-lenses]
27 Blub % TODO
28\begin{code}
29compEL :: EditLens c b c -> EditLens c' a b -> EditLens (c, c') a c
30compEL (EditLens c1 bc cb) (EditLens c2 ab ba) = EditLens (c1, c2) ac ca
31 where
32 ac ((c1, c2), a) = ((c1', c2'), c)
33 where (c2', b) = ab (c2, a)
34 (c1', c) = bc (c1, b)
35 ca ((c1, c2), c) = ((c1', c2'), a)
36 where (c2', a) = ba (c2, b)
37 (c1', b) = cb (c1, c)
38\end{code}
39\end{defn}
40
41Es ist leider nicht möglich eine Instanz für die Kategorien-Typeklasse der Haskell-Standardlibrary \cite[\texttt{Control.Category}]{base} zu definieren, da sich die Typklasse \texttt{Category} auf Typen vom Kind $\ast \to \ast \to \ast$ einschränkt, \texttt{EditLens} jedoch notwendigerweise den Typ seines Komplements mit sich trägt.