diff options
-rw-r--r-- | edit-lens/package.yaml | 1 | ||||
-rw-r--r-- | edit-lens/src/Control/Edit.lhs | 2 | ||||
-rw-r--r-- | edit-lens/src/Control/Edit/Container.lhs | 50 | ||||
-rw-r--r-- | edit-lens/src/Control/Lens/Edit.lhs | 5 | ||||
-rw-r--r-- | edit-lens/src/Control/Lens/Edit/Generic.lhs | 41 | ||||
-rwxr-xr-x | gup/literature.bibtex.gup | 7 | ||||
-rw-r--r-- | literature/base.bibtex | 6 | ||||
-rwxr-xr-x | thesis.pdf.gup | 6 | ||||
-rw-r--r-- | thesis.tex | 11 |
9 files changed, 117 insertions, 12 deletions
diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml index 5737fb4..61d1285 100644 --- a/edit-lens/package.yaml +++ b/edit-lens/package.yaml | |||
@@ -30,4 +30,5 @@ library: | |||
30 | - Control.Edit | 30 | - Control.Edit |
31 | - Control.Edit.Container | 31 | - Control.Edit.Container |
32 | - Control.Lens.Edit | 32 | - Control.Lens.Edit |
33 | - Control.Lens.Edit.Generic | ||
33 | 34 | ||
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 | ||
22 | 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. | 22 | 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. |
23 | 23 | ||
24 | Fü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 | |||
24 | 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)}. | 26 | 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)}. |
25 | Eine Repräsentierung als Typklasse bietet sich an: | 27 | Eine 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 @@ | |||
3 | module Control.Edit.Container | 3 | module 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 | ||
8 | import Control.Edit | 9 | import 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 | |||
22 | Intuitiv 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] | ||
25 | Ein 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 | |||
27 | Wir 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] |
31 | Ein 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 | |||
33 | In 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 | |||
35 | Hierfü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. | ||
36 | Polymorphe container können so mit universell quantifizierten Instanzen beschrieben werden. | ||
37 | |||
38 | Wir 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} |
21 | class ( Module (ModShape c) | 41 | class ( 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 | ||
31 | constructed :: Container c => Iso' (Shape c, Position c -> Content c) c | 60 | constructed :: Container c => Iso' (Shape c, Position c -> Content c) c |
61 | -- ^ Inverse of 'deconstructed', for convenience | ||
32 | constructed = from deconstructed | 62 | constructed = from deconstructed |
33 | 63 | ||
34 | type Shape c = Domain (ModShape c) | 64 | type 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] | ||
70 | Fü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} |
41 | data ContainerEdit c where | 82 | data 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 | |||
87 | type 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} |
50 | instance Container c => Module (Seq (ContainerEdit c)) where | 94 | instance 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} |
2 | module Control.Lens.Edit | 3 | module 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 | ||
9 | import Control.Edit | 11 | import Control.Edit |
10 | \end{code} | 12 | \end{code} |
13 | \end{comment} | ||
11 | 14 | ||
12 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] | 15 | \begin{defn}[Zustandsbehaftete Monoidhomomorphismen] |
13 | 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: | 16 | 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: |
@@ -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} |
47 | data EditLens c m n where | 50 | data 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 | ||
50 | class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where | 53 | class (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} | ||
3 | module Control.Lens.Edit.Generic | ||
4 | ( idEL, compEL | ||
5 | ) where | ||
6 | |||
7 | import Control.Edit | ||
8 | import Control.Lens.Edit | ||
9 | |||
10 | import Control.Lens | ||
11 | \end{code} | ||
12 | \end{comment} | ||
13 | |||
14 | Wir übernehmen einige der in \cite{hofmann2012edit} vorgestellten Konstruktionen für generische edit-lenses. | ||
15 | |||
16 | Zunä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} | ||
21 | idEL :: EditLens () a a | ||
22 | idEL = 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} | ||
29 | compEL :: EditLens c b c -> EditLens c' a b -> EditLens (c, c') a c | ||
30 | compEL (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 | |||
41 | Es 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. | ||
diff --git a/gup/literature.bibtex.gup b/gup/literature.bibtex.gup index cabebc3..ebbf8fb 100755 --- a/gup/literature.bibtex.gup +++ b/gup/literature.bibtex.gup | |||
@@ -1,9 +1,8 @@ | |||
1 | #!/usr/bin/env zsh | 1 | #!/usr/bin/env zsh |
2 | 2 | ||
3 | gup --always | ||
4 | |||
3 | typeset -a bibFiles | 5 | typeset -a bibFiles |
4 | bibFiles=(literature/**/*.bibtex) | 6 | bibFiles=(literature/**/*.bibtex) |
5 | 7 | ||
6 | gup --contents <<<${bibFiles} | 8 | cat ${bibFiles} >$1 |
7 | gup -u ${bibFiles} | ||
8 | |||
9 | cat ${bibFiles} >$1 \ No newline at end of file | ||
diff --git a/literature/base.bibtex b/literature/base.bibtex new file mode 100644 index 0000000..d5e3db5 --- /dev/null +++ b/literature/base.bibtex | |||
@@ -0,0 +1,6 @@ | |||
1 | @manual{base, | ||
2 | title={Basic Libraries}, | ||
3 | month={7}, | ||
4 | year={2017}, | ||
5 | url={https://hackage.haskell.org/package/base} | ||
6 | } \ No newline at end of file | ||
diff --git a/thesis.pdf.gup b/thesis.pdf.gup index 2167f7b..43a34e5 100755 --- a/thesis.pdf.gup +++ b/thesis.pdf.gup | |||
@@ -1,10 +1,10 @@ | |||
1 | #!/usr/bin/env zsh | 1 | #!/usr/bin/env zsh |
2 | 2 | ||
3 | gup -u edit-lens/src/Control/Lens/Edit.lhs | 3 | find edit-lens/src/ -name '*.lhs' -print0 | xargs -0 -- gup -u |
4 | gup -u edit-lens/src/Control/Lens/Edit/Compose.lhs | 4 | find edit-lens/src/ -name '*.lhs' -print0 | gup --contents |
5 | 5 | ||
6 | bDir=$(pwd) | 6 | bDir=$(pwd) |
7 | 7 | ||
8 | cd .. | 8 | cd .. |
9 | 9 | ||
10 | exec gup/pdf.gup $1 ${bDir}/$2 \ No newline at end of file | 10 | exec gup/pdf.gup $1 ${bDir}/$2 |
@@ -1,6 +1,15 @@ | |||
1 | \section{Edits und edit-lenses} | ||
2 | |||
1 | Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. | 3 | Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. |
2 | Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: | 4 | Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: |
3 | 5 | ||
4 | \input{./edit-lens/src/Control/Edit.lhs} | 6 | \input{./edit-lens/src/Control/Edit.lhs} |
7 | |||
5 | \input{./edit-lens/src/Control/Lens/Edit.lhs} | 8 | \input{./edit-lens/src/Control/Lens/Edit.lhs} |
6 | \input{./edit-lens/src/Control/Edit/Tree.lhs} | 9 | |
10 | \paragraph{Generische Konstruktionen für edit-lenses} | ||
11 | \input{./edit-lens/src/Control/Lens/Edit/Generic.lhs} | ||
12 | |||
13 | \section{Edit-lenses für container} | ||
14 | |||
15 | \input{./edit-lens/src/Control/Edit/Container.lhs} | ||