From b9eaf43c5da941b8e7c37c4ac950c8f2a7e618cd Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Mon, 13 Nov 2017 17:05:24 +0100 Subject: Initial work on central definitions --- .gitignore | 3 + edit-lens/ChangeLog.md | 5 ++ edit-lens/LICENSE | 30 +++++++ edit-lens/Setup.hs | 2 + edit-lens/edit-lens.cabal | 26 ++++++ edit-lens/src/Control/Lens/Edit.lhs | 158 ++++++++++++++++++++++++++++++++++ literature.meta.yml | 5 -- literature.meta.yml.gup | 11 +++ literature/incremental-parsing.bibtex | 2 +- literature/laarhoven.bibtex | 7 ++ literature/lens.bibtex | 7 ++ stack.nix | 11 +++ stack.yaml | 7 ++ thesis.meta.yml.gup | 14 +++ thesis.tex | 1 + 15 files changed, 283 insertions(+), 6 deletions(-) create mode 100644 edit-lens/ChangeLog.md create mode 100644 edit-lens/LICENSE create mode 100644 edit-lens/Setup.hs create mode 100644 edit-lens/edit-lens.cabal create mode 100644 edit-lens/src/Control/Lens/Edit.lhs delete mode 100644 literature.meta.yml create mode 100644 literature.meta.yml.gup create mode 100644 literature/laarhoven.bibtex create mode 100644 literature/lens.bibtex create mode 100644 stack.nix create mode 100644 stack.yaml create mode 100644 thesis.meta.yml.gup create mode 100644 thesis.tex diff --git a/.gitignore b/.gitignore index fb55372..8d2d346 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ literature.pdf **/.gup /literature.bibtex +**/.stack-work +/thesis.meta.yml +/thesis.pdf diff --git a/edit-lens/ChangeLog.md b/edit-lens/ChangeLog.md new file mode 100644 index 0000000..8bae309 --- /dev/null +++ b/edit-lens/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for edit-lens + +## 0.0.0.0 + +* First version. diff --git a/edit-lens/LICENSE b/edit-lens/LICENSE new file mode 100644 index 0000000..4522849 --- /dev/null +++ b/edit-lens/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017, Gregor Kleen + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Gregor Kleen nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/edit-lens/Setup.hs b/edit-lens/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/edit-lens/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/edit-lens/edit-lens.cabal b/edit-lens/edit-lens.cabal new file mode 100644 index 0000000..72c08c7 --- /dev/null +++ b/edit-lens/edit-lens.cabal @@ -0,0 +1,26 @@ +-- Initial edit-lens.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: edit-lens +version: 0.0.0.0 +-- synopsis: +-- description: +license: BSD3 +license-file: LICENSE +author: Gregor Kleen +maintainer: aethoago@141.li +-- copyright: +category: Control +build-type: Simple +extra-source-files: ChangeLog.md +cabal-version: >=1.10 + +library + exposed-modules: Control.Lens.Edit + -- other-modules: + -- other-extensions: + build-depends: base >=4.9 && <4.10 + , lens + , data-default + hs-source-dirs: src + default-language: Haskell2010 diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs new file mode 100644 index 0000000..69a6f7f --- /dev/null +++ b/edit-lens/src/Control/Lens/Edit.lhs @@ -0,0 +1,158 @@ +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 + , KindSignatures + , FlexibleContexts + , FlexibleInstances + , MultiParamTypeClasses + , FunctionalDependencies + , AllowAmbiguousTypes + , GADTs + #-} + +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 initialen Element (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 m^\prime $$ + +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 -> Del 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 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 HasEditLens (EditLens c 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. diff --git a/literature.meta.yml b/literature.meta.yml deleted file mode 100644 index 9eb6cc7..0000000 --- a/literature.meta.yml +++ /dev/null @@ -1,5 +0,0 @@ ---- -lang: de-de -link-citations: true -bibliography: literature.bibtex -... diff --git a/literature.meta.yml.gup b/literature.meta.yml.gup new file mode 100644 index 0000000..5a6cd9e --- /dev/null +++ b/literature.meta.yml.gup @@ -0,0 +1,11 @@ +#!/usr/bin/env zsh + +gup -u literature.bibtex + +cat >$1 < {}) }: + +let + inherit (nixpkgs) haskell pkgs; +in haskell.lib.buildStackProject { + inherit ghc; + name = "stackenv"; + buildInputs = with pkgs; + [ zlib + ]; +} diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..125d9fb --- /dev/null +++ b/stack.yaml @@ -0,0 +1,7 @@ +resolver: lts-9.9 +packages: + - edit-lens +nix: + packages: [] + pure: false + shell-file: ./stack.nix diff --git a/thesis.meta.yml.gup b/thesis.meta.yml.gup new file mode 100644 index 0000000..de9e5ac --- /dev/null +++ b/thesis.meta.yml.gup @@ -0,0 +1,14 @@ +#!/usr/bin/env zsh + +gup -u literature.bibtex + +cat >$1 <