Initial work on central definitions

14 files changed, 278 insertions, 1 deletions

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.gup
index 9eb6cc7..5a6cd9e 100644
--- a/literature.meta.yml
+++ b/literature.meta.yml.gup
@@ -1,5 +1,11 @@
+#!/usr/bin/env zsh
+
+gup -u literature.bibtex
+
+cat >$1 <<EOF
 ---
 lang: de-de
 link-citations: true
 bibliography: literature.bibtex
 ...
+EOF
diff --git a/literature/incremental-parsing.bibtex b/literature/incremental-parsing.bibtex
index e3e5758..5ece4e9 100644
--- a/literature/incremental-parsing.bibtex
+++ b/literature/incremental-parsing.bibtex
@@ -15,4 +15,4 @@
  acmid = {357066},
  publisher = {ACM},
  address = {New York, NY, USA},
-}
\ No newline at end of file
+}
diff --git a/literature/laarhoven.bibtex b/literature/laarhoven.bibtex
new file mode 100644
index 0000000..4a8305f
--- /dev/null
+++ b/literature/laarhoven.bibtex
@@ -0,0 +1,7 @@
+@misc{laarhoven,
+  title={CPS based functional references},
+  year={2009},
+  month={7},
+  author={Twan van Laarhoven},
+  url={https://www.twanvl.nl/blog/haskell/cps-functional-references}
+}
\ No newline at end of file
diff --git a/literature/lens.bibtex b/literature/lens.bibtex
new file mode 100644
index 0000000..ab9481e
--- /dev/null
+++ b/literature/lens.bibtex
@@ -0,0 +1,7 @@
+@manual{lens,
+  title={Lenses, Folds and Traversals},
+  author={Edward A. Kmett},
+  month={8},
+  year={2017},
+  url={https://hackage.haskell.org/package/lens}
+}
\ No newline at end of file
diff --git a/stack.nix b/stack.nix
new file mode 100644
index 0000000..eec431d
--- /dev/null
+++ b/stack.nix
@@ -0,0 +1,11 @@
+{ ghc, nixpkgs ? (import <nixpkgs> {}) }:
+
+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 <<EOF
+---
+lang: de-de
+link-citations: true
+bibliography: literature.bibtex
+title: Iterative Parser als Asymmetrische edit-lenses
+author: Gregor Kleen
+date: \today
+...
+EOF
diff --git a/thesis.tex b/thesis.tex
new file mode 100644
index 0000000..adc6515
--- /dev/null
+++ b/thesis.tex
@@ -0,0 +1 @@
+\input{./edit-lens/src/Control/Lens/Edit.lhs}