\end{chapterabstract}
\section{Introduction}%
-The two flavours of DSL embedding are deep and shallow embedding~\cite{boulton_experience_1992}.
+The two flavours of DSL embedding are deep and shallow embedding~\citep{boulton_experience_1992}.
In functional programming languages, shallow embedding models language constructs as functions in the host language.
As a result, adding new language constructs---extra functions---is easy.
However, the semantics of the language is embedded in these functions, making it troublesome to add semantics since it requires updating all existing language constructs.
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~\cite{reynolds_user-defined_1978} and discussed by many others~\cite{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler~\cite{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 Wadler~\citep{wadler_expression_1998}:
\begin{quote}
The \emph{expression problem} is a new name for an old problem.
\end{quote}
In shallow embedding, abstracting the functions to type classes disentangles the language constructs from the semantics, allowing extension both ways.
-This technique is dubbed tagless-final embedding~\cite{carette_finally_2009}, nonetheless it is no silver bullet.
+This technique is dubbed tagless-final embedding~\citep{carette_finally_2009}, nonetheless it is no silver bullet.
Some semantics that require an intensional analysis of the syntax tree, such as transformation and optimisations, are difficult to implement in shallow embedding due to the lack of an explicit data structure representing the abstract syntax tree.
-The semantics of the DSL have to be combined and must hold some kind of state or context, so that structural information is not lost~\cite{kiselyov_typed_2012}.
+The semantics of the DSL have to be combined and must hold some kind of state or context, so that structural information is not lost~\citep{kiselyov_typed_2012}.
\subsection{Research contribution}
This paper shows how to apply the technique observed in tagless-final embedding to deep embedding.
The presented basic technique, christened \emph{classy deep embedding}, does not require advanced type system extensions to be used.
However, it is suitable for type system extensions such as generalised algebraic data types.
While this paper is written as a literate
-Haskell~\cite{peyton_jones_haskell_2003} program using some minor extensions provided by GHC~\cite{ghc_team_ghc_2021}, the idea is applicable to other languages as well\footnotemark{}.
+Haskell~\citep{peyton_jones_haskell_2003} program using some minor extensions provided by GHC~\citep{ghc_team_ghc_2021}, the idea is applicable to other languages as well\footnotemark{}.
\footnotetext{Lubbers, M. (2021): Literate Haskell/lhs2\TeX{} source code of the paper ``Deep Embedding
with Class'': TFP 2022.\ DANS.\ \url{https://doi.org/10.5281/zenodo.5081386}.}
Adding semantics on the other hand---e.g.\ a printer---is not that simple because the semantics are part of the functions representing the language constructs.
One way to add semantics is to change all functions to execute both semantics at the same time.
In our case this means changing the type of \haskelllhstexinline{Sem_s} to be \haskelllhstexinline{(Int, String)} so that all functions operate on a tuple containing the result of the evaluator and the printed representation at the same time. %chktex 36
-Alternatively, a single semantics can be defined that represents a fold over the language constructs~\cite{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied.
+Alternatively, a single semantics can be defined that represents a fold over the language constructs~\citep{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied.
\subsection{Tagless-final embedding}
Tagless-final embedding overcomes the limitations of standard shallow embedding.
The recursive knot is left untied and as a result, \haskelllhstexinline{Sub_1} can never be reached from an \haskelllhstexinline{Expr_1}.
Luckily, we can reconnect them by adding a special constructor to the \haskelllhstexinline{Expr_1} data type for housing extensions.
-It contains an existentially quantified~\cite{mitchell_abstract_1988} type with type class constraints~\cite{laufer_combining_1994,laufer_type_1996} for all semantics type classes~\cite[Chp.~6.4.6]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.
+It contains an existentially quantified~\citep{mitchell_abstract_1988} type with type class constraints~\citep{laufer_combining_1994,laufer_type_1996} for all semantics type classes~\cite[Chp.~6.4.6]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.
\begin{lstHaskellLhstex}
data Expr_2 = Lit_2 Int
The class alias removes the need for the programmer to visit the main data type when adding additional semantics.
Unfortunately, the compiler does need to visit the main data type again.
Some may argue that adding semantics happens less frequently than adding language constructs but in reality it means that we have to concede that the language is not as easily extensible in semantics as in language constructs.
-More exotic type system extensions such as constraint kinds~\cite{bolingbroke_constraint_2011,yorgey_giving_2012} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
+More exotic type system extensions such as constraint kinds~\citep{bolingbroke_constraint_2011,yorgey_giving_2012} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
However, by adding some boilerplate, even without this extension, the language constructs can be parametrised by the semantics by putting the semantics functions in a data type.
First the data types for the language constructs are parametrised by the type variable \haskelllhstexinline{d} as follows.
Pattern matching within datatypes and from an extension to the main data type works out of the box.
Cross-extensional pattern matching on the other hand---matching on a particular extension---is something that requires a bit of extra care.
Take for example negation propagation and double negation elimination.
-Pattern matching on values with an existential type is not possible without leveraging dynamic typing~\cite{abadi_dynamic_1991,baars_typing_2002}.
-To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic}~\cite{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions.
+Pattern matching on values with an existential type is not possible without leveraging dynamic typing~\citep{abadi_dynamic_1991,baars_typing_2002}.
+To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic}~\citep{ghc_team_datadynamic_2021} is added to the list of constraints in all places where we need to pattern match across extensions.
As a result, the \haskelllhstexinline{Typeable} type class constraints are added to the quantified type variable \haskelllhstexinline{x} of the \haskelllhstexinline{Ext_4} constructor and to \haskelllhstexinline{d}s in the smart constructors.
\begin{lstHaskellLhstex}
\end{lstHaskellLhstex}
\section{Generalised algebraic data types}%
-Generalised algebraic data types (GADTs) are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\cite{cheney_first-class_2003,hinze_fun_2003}.
+Generalised algebraic data types (GADTs) are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\citep{cheney_first-class_2003,hinze_fun_2003}.
Leveraging GADTs, deeply embedded DSLs can be made statically type safe even when different value types are supported.
Even when GADTs are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types~\cite[Sec.~2.2]{cheney_lightweight_2002}.
Where some solutions to the expression problem do not easily generalise to GADTs (see \cref{sec:cde:related}), classy deep embedding does.
Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
The introduced type variable \haskelllhstexinline{a} is not an argument to the type class, so it should not be an argument to the dictionary data type.
-To represent this type class function, a rank-2 polymorphic function is needed~\cite[Chp.~6.4.15]{ghc_team_ghc_2021}\cite{odersky_putting_1996}.
+To represent this type class function, a rank-2 polymorphic function is needed~\cite[Chp.~6.4.15]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
Concretely, for the evaluatior this results in the following definitions:
\begin{lstHaskellLhstex}
Embedded DSL techniques in functional languages have been a topic of research for many years, thus we do not claim a complete overview of related work.
-Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a la Carte}~\cite{swierstra_data_2008}.
+Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a la Carte}~\citep{swierstra_data_2008}.
In Swierstra's approach, semantics are lifted to type classes similarly to classy deep embedding.
Each language construct is their own datatype parametrised by a type parameter.
This parameter contains some type level representation of language constructs that are in use.
In return, pattern matching is easier and does not require dynamic typing.
Classy deep embedding only strains the programmer with writing the extension case for the main data type and the occasional loopback constructor.
-L\"oh and Hinze proposed a language extension that allows open data types and open functions, i.e.\ functions and data types that can be extended with more cases later on~\cite{loh_open_2006}.
+L\"oh and Hinze proposed a language extension that allows open data types and open functions, i.e.\ functions and data types that can be extended with more cases later on~\citep{loh_open_2006}.
They hinted at the possibility of using type classes for open functions but had serious concerns that pattern matching would be crippled because constructors are becoming types, thus ultimately becoming impossible to type.
In contrast, this paper shows that pattern matching is easily attainable---albeit using dynamic types---and that the terms can be typed without complicated type system extensions.
-A technique similar to classy deep embedding was proposed by Najd and Peyton~Jones to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form~\cite{najd_trees_2017}.
+A technique similar to classy deep embedding was proposed by Najd and Peyton~Jones to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form~\citep{najd_trees_2017}.
For example to decorate the abstract syntax tree of a compiler differently for each phase of the compiler.
They propose to add an extension descriptor as a type variable to a data type and a type family that can be used to decorate constructors with extra information and add additional constructors to the data type using an extension constructor.
Classy deep embedding works similarly but uses existentially quantified type variables to describe possible extensions instead of type variables and type families.
In classy deep embedding, the extensions do not need to be encoded in the type system and less boilerplate is required.
Furthermore, pattern matching on extensions becomes a bit more complicated but in return it allows for multiple extensions to be added orthogonally and avoids the necessity for type system extensions.
-Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding~\cite{carette_finally_2009}.
+Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding~\citep{carette_finally_2009}.
Classy deep embedding was organically grown from observing the evolution of tagless-final embedding.
The main difference between tagless-final embedding and classy deep embedding---and in general between shallow and deep embedding---is that intensional analyses of the abstract syntax tree is more difficult because there is no tangible abstract syntax tree data structure.
In classy deep embedding, it is possible to define transformations even across extensions.
Hybrid approaches between deep and shallow embedding exist as well.
-For example, Svenningson et al.\ show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well~\cite{svenningsson_combining_2013}.
+For example, Svenningson et al.\ show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well~\citep{svenningsson_combining_2013}.
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.
\section*{Acknowledgements}
repositories / phd-thesis.git / blobdiff