From afc34d76c845f1be96818addcffb4f70d9d2ea9d Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 24 Nov 2017 17:38:54 +0100 Subject: Work on containers --- edit-lens/src/Control/Edit.lhs | 2 ++ edit-lens/src/Control/Edit/Container.lhs | 50 +++++++++++++++++++++++++++-- edit-lens/src/Control/Lens/Edit.lhs | 5 ++- edit-lens/src/Control/Lens/Edit/Generic.lhs | 41 +++++++++++++++++++++++ 4 files changed, 94 insertions(+), 4 deletions(-) create mode 100644 edit-lens/src/Control/Lens/Edit/Generic.lhs (limited to 'edit-lens/src/Control') 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 \ 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. +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)$. + 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: 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 @@ module Control.Edit.Container ( Container(..), Shape, Content , ContainerEdit(..) + , module Control.Edit ) where import Control.Edit @@ -16,19 +17,48 @@ import Control.Lens \end{code} \end{comment} +\citeauthor{hofmann2012edit} stellen \emph{container} vor—eine systematische Sicht auf Datenstrukturen, die es erlaubt eine generische edit-language zu definieren. + +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: + +\begin{defn}[Container-Typen] +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. + +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}. +\end{defn} + \begin{defn}[Container] +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. + +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})$. + +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. +Polymorphe container können so mit universell quantifizierten Instanzen beschrieben werden. + +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. + \begin{code} class ( Module (ModShape c) , Module (ModContent c) - , Ord (Position c) + , Ord (Position c) -- ^ Neccessary to form 'Set's of 'Position's ) => Container c where + -- | Since we characterise 'Module's by the type of their edits we have to associate that type with @c@. + -- We later introduce a type synonym for @Domain (ModShape c)@ later. type ModShape c :: * + type Position c :: * + type ModContent c :: * + -- ^ Analogous to 'ModShape' + + -- | Compute the live positions of a shape positions :: Shape c -> Set (Position c) + + -- | Convert between the natural representation @c@ and a view as container, that is a 'Shape c' and a value function deconstructed :: Iso' c (Shape c, Position c -> Content c) constructed :: Container c => Iso' (Shape c, Position c -> Content c) c +-- ^ Inverse of 'deconstructed', for convenience constructed = from deconstructed type Shape c = Domain (ModShape c) @@ -36,19 +66,33 @@ type Content c = Domain (ModContent c) \end{code} \end{defn} +\begin{defn}[Klassifikation von edits auf shapes] +Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edits $\partial i \in \partial I$ wie folgt: + +\begin{description} + \item[insertions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \geq i$ + \item[deletions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \leq i$ + \item[rearrangements] $\forall i \in \Dom (\partial i) \colon \size{\text{positions}(i \cdot \partial i)} = \size{\text{positions}(i)}$ +\end{description} +\end{defn} + \begin{defn}[container-edits] + TODO \begin{code} data ContainerEdit c where Fail :: ContainerEdit c ModContent :: Position c -> ModContent c -> ContainerEdit c ModShape :: ModShape c -> (Shape c -> Position c -> Position c) -> ContainerEdit c + +type ContainerEdits c = Seq (ContainerEdit c) \end{code} \end{defn} \begin{defn}[Wirkung von container-edits] + TODO \begin{code} -instance Container c => Module (Seq (ContainerEdit c)) where - type Domain (Seq (ContainerEdit c)) = c +instance Container c => Module (ContainerEdits c) where + type Domain (ContainerEdits c) = c apply fs = over mapped (view constructed) . flip (foldM apply') fs . view deconstructed where 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 @@ +\begin{comment} \begin{code} module Control.Lens.Edit ( Module(..) , StateMonoidHom , HasEditLens(..) , EditLens(..) + , module Control.Edit ) where import Control.Edit \end{code} +\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: @@ -45,7 +48,7 @@ In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\R \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 + EditLens :: 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 :: * 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 @@ +\begin{comment} +\begin{code} +module Control.Lens.Edit.Generic + ( idEL, compEL + ) where + +import Control.Edit +import Control.Lens.Edit + +import Control.Lens +\end{code} +\end{comment} + +Wir übernehmen einige der in \cite{hofmann2012edit} vorgestellten Konstruktionen für generische edit-lenses. + +Zunächst bilden edit-lenses die Morphismen einer Kategorie vermöge folgender Konstruktionen: + +\begin{defn}[Identität von edit-lenses] + Blub % TODO +\begin{code} +idEL :: EditLens () a a +idEL = EditLens () (over _2 id) (over _2 id) +\end{code} +\end{defn} + +\begin{defn}[Komposition von edit-lenses] + Blub % TODO +\begin{code} +compEL :: EditLens c b c -> EditLens c' a b -> EditLens (c, c') a c +compEL (EditLens c1 bc cb) (EditLens c2 ab ba) = EditLens (c1, c2) ac ca + where + ac ((c1, c2), a) = ((c1', c2'), c) + where (c2', b) = ab (c2, a) + (c1', c) = bc (c1, b) + ca ((c1, c2), c) = ((c1', c2'), a) + where (c2', a) = ba (c2, b) + (c1', b) = cb (c1, c) +\end{code} +\end{defn} + +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. -- cgit v1.2.3