From aca24d6f4a2a2780881bd24a5b26fdf74d17326a Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Thu, 23 Nov 2017 15:59:10 +0100 Subject: Refactor --- edit-lens/edit-lens.cabal | 35 ----------------- edit-lens/package.yaml | 4 +- edit-lens/src/Control/Edit.lhs | 71 +++++++++++++++++++++++++++++++++ edit-lens/src/Control/Edit/Tree.lhs | 9 +++++ edit-lens/src/Control/Lens/Edit.lhs | 78 +------------------------------------ thesis.pdf.gup | 10 +++++ thesis.tex | 5 +++ 7 files changed, 98 insertions(+), 114 deletions(-) delete mode 100644 edit-lens/edit-lens.cabal create mode 100644 edit-lens/src/Control/Edit.lhs create mode 100644 edit-lens/src/Control/Edit/Tree.lhs create mode 100755 thesis.pdf.gup diff --git a/edit-lens/edit-lens.cabal b/edit-lens/edit-lens.cabal deleted file mode 100644 index ab4c575..0000000 --- a/edit-lens/edit-lens.cabal +++ /dev/null @@ -1,35 +0,0 @@ --- This file has been generated from package.yaml by hpack version 0.19.3. --- --- see: https://github.com/sol/hpack - -name: edit-lens -version: 0.0.0.0 -category: Control -author: Gregor Kleen -license: BSD3 -license-file: LICENSE -build-type: Simple -cabal-version: >= 1.10 - -extra-source-files: - ChangeLog.md - -source-repository head - type: git - location: https://git.yggdrasil.li/gkleen/pub/bachelor-thesis - -library - hs-source-dirs: - src - default-extensions: TypeFamilies FlexibleContexts FlexibleInstances MultiParamTypeClasses FunctionDependencies AllowAmbiguousTypes TypeApplication GADTs - build-depends: - base - , lens - exposed-modules: - Control.Edit - Control.Edit.Tree - Control.Lens.Edit - other-modules: - Control.Lens.Edit.Compose - Paths_edit_lens - default-language: Haskell2010 diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml index 01b83fa..db1f021 100644 --- a/edit-lens/package.yaml +++ b/edit-lens/package.yaml @@ -15,9 +15,9 @@ library: - FlexibleContexts - FlexibleInstances - MultiParamTypeClasses - - FunctionDependencies + - FunctionalDependencies - AllowAmbiguousTypes - - TypeApplication + - TypeApplications - GADTs source-dirs: src dependencies: diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs new file mode 100644 index 0000000..7be8db4 --- /dev/null +++ b/edit-lens/src/Control/Edit.lhs @@ -0,0 +1,71 @@ +\begin{comment} +\begin{code} +module Control.Edit + ( Module(..) + ) where +\end{code} +\end{comment} + +\begin{defn}[Moduln] +Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (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 \partial 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. + +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 -> 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 schwach-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} + diff --git a/edit-lens/src/Control/Edit/Tree.lhs b/edit-lens/src/Control/Edit/Tree.lhs new file mode 100644 index 0000000..28320c5 --- /dev/null +++ b/edit-lens/src/Control/Edit/Tree.lhs @@ -0,0 +1,9 @@ +\begin{comment} +\begin{code} +module Control.Edit.Tree + ( + ) where + +import Control.Edit +\end{code} +\end{comment} diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs index 7a6cbbe..5a60536 100644 --- a/edit-lens/src/Control/Lens/Edit.lhs +++ b/edit-lens/src/Control/Lens/Edit.lhs @@ -1,89 +1,13 @@ -Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. -Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: - \begin{code} -{-# LANGUAGE TypeFamilies - , FlexibleContexts - , FlexibleInstances - , MultiParamTypeClasses - , FunctionalDependencies - #-} --- Allow more complicated type families -{-# LANGUAGE AllowAmbiguousTypes #-} --- AmbiguousTypes are useful if we expect functions to be called via TypeApplication -{-# LANGUAGE GADTs #-} --- For allowing constraints on constructors - 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 schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (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 \partial 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. - -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 -> 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 schwach-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 --} +import Control.Edit \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: diff --git a/thesis.pdf.gup b/thesis.pdf.gup new file mode 100755 index 0000000..2167f7b --- /dev/null +++ b/thesis.pdf.gup @@ -0,0 +1,10 @@ +#!/usr/bin/env zsh + +gup -u edit-lens/src/Control/Lens/Edit.lhs +gup -u edit-lens/src/Control/Lens/Edit/Compose.lhs + +bDir=$(pwd) + +cd .. + +exec gup/pdf.gup $1 ${bDir}/$2 \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index adc6515..f975ba7 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1 +1,6 @@ +Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. +Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: + +\input{./edit-lens/src/Control/Edit.lhs} \input{./edit-lens/src/Control/Lens/Edit.lhs} +\input{./edit-lens/src/Control/Edit/Tree.lhs} -- cgit v1.2.3