While this chapter is written as a literate
\Gls{HASKELL} \citep{peyton_jones_haskell_2003} program using some minor extensions provided by \gls{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}.}
+with Class'': TFP 2022.\ Zenodo.\ \url{https://doi.org/10.5281/zenodo.6650880}.}
\section{Deep embedding}
-Pick a \gls{DSL}, any \gls{DSL}, pick the language of literal integers and addition.
+Pick the language of literal integers and addition \citep{bender_benderrule_2019}\todo{nodig? grappig?}.
+%Pick a \gls{DSL}, any \gls{DSL}, pick the language of literal integers and addition.
In deep embedding, terms in the language are represented by data in the host language.
Hence, defining the constructs is as simple as creating the following algebraic data type\footnote{All data types and functions are subscripted to indicate the evolution. When definitions are omitted for version $n$, version $n-1$ is assumed.}.
sub_t (E_t e1) (E_t e2) = E_t (e1 - e2)
\end{lstHaskellLhstex}
-Finally, adding semantics such as a printer over the language is achieved by providing a data type representing the semantics accompanied by instances for the language constructs.
+Finally, adding semantics such as a printer for the language is achieved by providing a data type representing the semantics accompanied by instances for the language constructs.
\begin{lstHaskellLhstex}
newtype Printer_t = P_t String
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.
+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 \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.
\end{lstHaskellLhstex}
The \haskelllhstexinline{d} type variable is inhabited by an explicit dictionary for the semantics, i.e.\ a witness to the class instance.
-Therefore, for all semantics type classes, a data type is made that contains the semantics function for the given semantics.
+Therefore, for all semantics type classes, a data type is defined which contains the semantics function for the given semantics.
This means that for \haskelllhstexinline{Eval_3}, a dictionary with the function \haskelllhstexinline{EvalDict_3} is defined, a type class \haskelllhstexinline{HasEval_3} for retrieving the function from the dictionary and an instance for \haskelllhstexinline{HasEval_3} for \haskelllhstexinline{EvalDict_3}.
\begin{lstHaskellLhstex}
sub_3 e1 e2 = Ext_3 gdict (Sub_3 e1 e2)
\end{lstHaskellLhstex}
-Finally, we reached the end goal, orthogonal extension of both language constructs as shown by adding subtraction to the language and in language semantics.
+Finally, we reached the end goal, orthogonal extension of both language constructs as shown by adding subtraction to the language, and in language semantics.
Adding the printer can now be done without touching the original code as follows.
First the printer type class, dictionaries and instances for \haskelllhstexinline{GDict} are defined.
Dependent language functionality often does not need to span extensions, i.e.\ it is possible to group them in the same data type.
\subsection{Chaining semantics}
-Now that the data types are parametrised by the semantics a final problem needs to be overcome.
+Now that the data types are parametrised by the semantics, a final problem needs to be overcome.
The data type is parametrised by the semantics, thus, using multiple semantics, such as evaluation after optimising is not straightforwardly possible.
Luckily, a solution is readily at hand: introduce an ad-hoc combination semantics.
\section{Generalised algebraic data types}%
\Glspl{GADT} 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 \glspl{GADT}, deeply embedded \glspl{DSL} can be made statically type safe even when different value types are supported.
-Even when \glspl{GADT} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types \citep[\citesection{2.2}]{cheney_lightweight_2002}.
+Still when \glspl{GADT} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types \citep[\citesection{2.2}]{cheney_lightweight_2002}.
Where some solutions to the expression problem do not easily generalise to \glspl{GADT} (see \cref{sec:cde:related}), classy deep embedding does.
Generalising the data structure of our \gls{DSL} is fairly straightforward and to spice things up a bit, we add an equality and boolean negation language construct.
To make the existing \gls{DSL} constructs more general, we relax the types of those constructors.
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}
-No \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requirements programmers have.
+No single \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requirements 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.
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.
+Minimal boilerplate denotes the amount of scaffolding and boilerplate required.
For example, hybrid embedding requires a transcoding step between the deep syntax and the shallow core language.
\begin{table}
Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
& \textcolor{gray}{\CIRCLE{}}\tnote{4}\\
- Little boilerplate & \CIRCLE{} & \CIRCLE{} & \Circle{}
+ Minimal boilerplate & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
& \textcolor{gray}{\CIRCLE{}}\tnote{4}\\
\bottomrule
\begin{subappendices}
\section{Reprise: reducing boilerplate}%
\label{sec:classy_reprise}
-One of the unique selling points of this novel \gls{DSL} embedding technique is that it, in its basic form, does not require advanced type system extensions nor a lot of boilerplate.
+One of the unique selling points of classy deep embedding is that it, in its basic form, does not require advanced type system extensions nor a lot of boilerplate.
However, generalising the technique to \glspl{GADT} arguably unleashes a cesspool of \emph{unsafe} compiler extensions.
If we are willing to work with extensions, almost all the boilerplate can be inferred or generated.
\section{Data types and definitions}%
\label{sec:cde:appendix}
-This appendix collects all definitions omitted for brevity.
+This appendix contains all definitions omitted for brevity.
\lstset{basicstyle=\tt\footnotesize}
\begin{lstHaskellLhstex}[caption={Data type definitions.}]
repositories / phd-thesis.git / blobdiff