\input{subfilepreamble}
+\setcounter{chapter}{0}
+
\begin{document}
+\input{subfileprefix}
\chapter{Deep embedding with class}%
\label{chp:classy_deep_embedding}
-
-\input{subfileprefix}
-
\begin{chapterabstract}
The two flavours of \gls{DSL} embedding are shallow and deep embedding.
In functional languages, shallow embedding models the language constructs as functions in which the semantics are embedded.
It can be stated that the language constructs are embedded in the functions that form a semantics.
If one wants to add a language construct, all semantics functions must be revisited and revised to avoid ending up with partial functions.
-This juxtaposition has been known for many years \citep{reynolds_user-defined_1978} and discussed by many others \citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler \citep{wadler_expression_1998}:
+This juxtaposition has been known for many years \citep{reynolds_user-defined_1978} and discussed by many others \citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by \citet{wadler_expression_1998}:
\begin{quote}
The \emph{expression problem} is a new name for an old problem.
opt_g (NotLoop_g e) = NotLoop_g (opt_g e)
\end{lstHaskellLhstex}
-\section{Conclusion}%
-
-Classy deep embedding is a novel organically grown embedding technique that alleviates deep embedding from the extensibility problem in most cases.
-
-By abstracting the semantics functions to type classes they become overloaded in the language constructs.
-Thus, making it possible to add new language constructs in a separate type.
-These extensions are brought together in a special extension constructor residing in the main data type.
-This extension case is overloaded by the language construct using a data type containing the class dictionary.
-As a result, orthogonal extension is possible for language constructs and semantics using only little syntactic overhead or type annotations.
-The basic technique only requires---well established through history and relatively standard---existential data types.
-However, if needed, the technique generalises to \glspl{GADT} as well, adding rank-2 types to the list of type system requirements as well.
-Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
-
-Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
-\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.
-
\section{Related work}%
\label{sec:cde:related}
Hybrid approaches between deep and shallow embedding exist as well.
For example, \citet{svenningsson_combining_2013} show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well.
-This paper differs from those approaches in the sense that it does not require a core language in which all extensions need to be expressible.
+Classy deep embedding differs from the hybrid approaches in the sense that it does not require the language extensions to be expressible in the core language.
\subsection{Comparison}
-\todo[inline]{text moet beter}
-No \gls{DSL} embedding technique is the silver bullet.
+No \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requiremens programmers have.
\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two stated in the expression problem.
\Cref{tbl:dsl_comparison_brief} shows a variant of their comparison table.
-The first two rows describe the two axes of the original expression problem and the third row describes theadded axis of modular dependency handling as stated by \citeauthor{sun_compositional_2022}.
+The first two rows describe the two axes of the original expression problem and the third row describes the added axis of modular dependency handling as stated by \citeauthor{sun_compositional_2022}.
The \emph{poly.} style of embedding---including tagless-final---falls short of this requirement.
Intensional analysis is an umbrella term for pattern matching and transformations.
In shallow embedding, intensional analysis is more complex and requires stateful views describing context but it is possible to implement though.
-Simple type system describes the whether it is possible to encode this embedding technique with many type system extensions.
+Simple type system describes the whether it is possible to encode this embedding technique without many type system extensions.
In classy deep embedding, there is either a bit more scaffolding and boilerplate required or advanced type system extensions need to be used.
Little boilerplate denotes the amount of scaffolding and boilerplate required.
& \CIRCLE{}\\
Intensional analysis & \LEFTcircle{}\tnote{2} & \CIRCLE{} & \CIRCLE{}
& \LEFTcircle{}\tnote{2} & \LEFTcircle{}\tnote{2} & \CIRCLE{}
- & \LEFTcircle{}\tnote{3}\\
+ & \CIRCLE{}\tnote{3}\\
Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
& \LEFTcircle{}\tnote{4}\\
\end{threeparttable}
\end{table}
+\section{Conclusion}%
+Classy deep embedding is a novel organically grown embedding technique that alleviates deep embedding from the extensibility problem in most cases.
+
+By abstracting the semantics functions to type classes they become overloaded in the language constructs.
+Thus, making it possible to add new language constructs in a separate type.
+These extensions are brought together in a special extension constructor residing in the main data type.
+This extension case is overloaded by the language construct using a data type containing the class dictionary.
+As a result, orthogonal extension is possible for language constructs and semantics using only little syntactic overhead or type annotations.
+The basic technique only requires---well established through history and relatively standard---existential data types.
+However, if needed, the technique generalises to \glspl{GADT} as well, adding rank-2 types to the list of type system requirements as well.
+Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
+
+Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
+\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.
+
\section*{Acknowledgements}
This research is partly funded by the Royal Netherlands Navy.
Furthermore, I would like to thank Pieter and Rinus for the fruitful discussions, Ralf for inspiring me to write a functional pearl, and the anonymous reviewers for their valuable and honest comments.
In classy deep embedding, the \gls{DSL} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
When using multiple interpretations, these need to be bundled in a data type.
Using the \gls{GHC}'s \GHCmod{ConstraintKind} extension, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
-Furthermore, this constraint does not necessarily has to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead.
+Furthermore, this constraint does not necessarily has to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead \citep{yorgey_giving_2012}.
The data type for this list of witnesses is \haskelllhstexinline{Record} as shown in \cref{lst_cbde:record_type}.
This \gls{GADT} is parametrised by two type variables.
The first type variable (\haskelllhstexinline{dt}) is the type or type constructor on which the constraints can be applied and the second type variable (\haskelllhstexinline{clist}) is the list of constraints constructors itself.
\end{lstHaskellLhstex}
Furthermore, we define a type class (\haskelllhstexinline{In}) that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
-Since the constraints become available as soon as the \haskelllhstexinline{Cons} constructor is matched, the implementation is a trivial type-level list traversal.
+Since the constraints become available as soon as the \haskelllhstexinline{Cons} constructor is matched, the implementation is a type-level list traversal.
\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
class c `In` cs where
e1 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
\end{lstHaskellLhstex}
-Finally, using the \GHCmod{TypeFamilies} extension, type families can be created for bundling \haskelllhstexinline{`In`} constraints (\haskelllhstexinline{UsingExt}) and \haskelllhstexinline{CreateRecord} constraints (\haskelllhstexinline{DependsOn}), making the syntax even more descriptive.
-E.g.\ \haskelllhstexinline{UsingExt '[A, B, C] c} expands to \haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)} and \haskelllhstexinline{DependsOn '[A, B, C] s} expands to \haskelllhstexinline{(A `In` s, B `In` s, C `In` s)}.
+Finally, using the \GHCmod{TypeFamilies} extension, type families can be created for bundling \haskelllhstexinline{`In`} constraints (\haskelllhstexinline{UsingExt}) and \haskelllhstexinline{CreateRecord} constraints \mbox{(\haskelllhstexinline{DependsOn})}, making the syntax even more descriptive.
+E.g.\ \mbox{\haskelllhstexinline{UsingExt '[A, B, C] c}} expands to\newline\haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)}.
+Similarly, \haskelllhstexinline{DependsOn '[A, B, C] s} expands to \haskelllhstexinline{(A `In` s, B `In` s, C `In` s)}.
\begin{lstHaskellLhstex}
type family UsingExt cs c :: Constraint where
With these enhancements, there is hardly any boilerplate required to use classy deep embedding.
The \haskelllhstexinline{Record} data type; the \haskelllhstexinline{CreateRecord} type class; and the \haskelllhstexinline{UsingExt} and \haskelllhstexinline{DependsOn} type families can be provided as a library only requiring the programmer to create the extension constructors with their respective implementations and smart constructors for language construct extensions.
-The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.
+The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.\footnote{Lubbers, M. (2022): Library and examples for enhanced classy deep embedding.\ Zenodo.\ \href{https://doi.org/10.5281/zenodo.7277498}{10.5281/zenodo.7277498}.}
+It contains examples for expressions, expressions using \glspl{GADT}, detection of sharing in expressions (modelled after \citet{kiselyov_implementing_2011}), a \gls{GADT} version of sharing detection, and a region \gls{DSL} (modelled after \citet{sun_compositional_2022}).
\section{Data types and definitions}%
\label{sec:cde:appendix}
+This appendix collects all definitions omitted for brevity.
+
\lstset{basicstyle=\tt\footnotesize}
\begin{lstHaskellLhstex}[caption={Data type definitions.}]
data Sub_g d a where
repositories / phd-thesis.git / blobdiff