\label{chp:classy_deep_embedding}
\begin{chapterabstract}
- The two flavours of DSL embedding are shallow and deep embedding.
+ 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.
Adding semantics is therefore cumbersome while adding constructs is a breeze.
Upgrading the functions to type classes lifts this limitation to a certain extent.
As a result, the language constructs are embedded in the semantics, hence adding new language constructs is laborious where adding semantics is trouble free.
This paper shows that by abstracting the semantics functions in deep embedding to type classes, it is possible to easily add language constructs as well.
- So-called classy deep embedding results in DSLs that are extensible both in language constructs and in semantics while maintaining a concrete abstract syntax tree.
+ So-called classy deep embedding results in \glspl{DSL} that are extensible both in language constructs and in semantics while maintaining a concrete abstract syntax tree.
Additionally, little type-level trickery or complicated boilerplate code is required to achieve this.
\end{chapterabstract}
\section{Introduction}
-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.
+The two flavours of \gls{DSL} embedding are deep and shallow embedding~\citep{boulton_experience_1992}.
+In \gls{FP} 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.
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~\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~\citep{kiselyov_typed_2012}.
+The semantics of the \gls{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.
+However, it is suitable for type system extensions such as \glspl{GADT}.
While this paper is written as a literate
-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{}.
+\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}.}
\section{Deep embedding}
-Pick a DSL, any DSL, pick the language of literal integers and addition.
+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.}.
| Sub_0 Expr_0 Expr_0
\end{lstHaskellLhstex}
-Extending the DSL with language constructs exposes the Achilles' heel of deep embedding.
+Extending the \gls{DSL} with language constructs exposes the Achilles' heel of deep embedding.
Adding a case to the data type means that all semantics functions have become partial and need to be updated to be able to handle this new case.
This does not seem like an insurmountable problem, but it does pose a problem if either the functions or the data type itself are written by others or are contained in a closed library.
\end{lstHaskellLhstex}
\section{Lifting the backends}%
-Let us rethink the deeply embedded DSL design.
+Let us rethink the deeply embedded \gls{DSL} design.
Remember that in shallow embedding, the semantics are embedded in the language construct functions.
Obtaining extensibility both in constructs and semantics was accomplished by abstracting the semantics functions to type classes, making the constructs overloaded in the semantics.
In deep embedding, the constructs are embedded in the semantics functions instead.
e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
\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~\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~\citep[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.
-Generalising the data structure of our DSL is fairly straightforward and to spice things up a bit, we add an equality and boolean not language construct.
-To make the existing DSL constructs more general, we relax the types of those constructors.
+\section{\texorpdfstring{\Acrlongpl{GADT}}{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[Sec.~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 not language construct.
+To make the existing \gls{DSL} constructs more general, we relax the types of those constructors.
For example, operations on integers now work on all numerals instead.
-Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the DSL domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer.
+Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the \gls{DSL} domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer.
Since some optimisations on \haskelllhstexinline{Not_g} remove constructors and therefore use cross-extensional pattern matches, \haskelllhstexinline{Typeable} constraints are added to \haskelllhstexinline{a}.
Furthermore, because the optimisations for \haskelllhstexinline{Add_g} and \haskelllhstexinline{Sub_g} are now more general, they do not only work for \haskelllhstexinline{Int}s but for any type with a \haskelllhstexinline{Num} instance, the \haskelllhstexinline{Eq} constraint is added to these constructors as well.
Finally, not to repeat ourselves too much, we only show the parts that substantially changed.
not_g e = Ext_g gdict (Not_g e)
\end{lstHaskellLhstex}
-Upgrading the semantics type classes to support GADTs is done by an easy textual search and replace.
+Upgrading the semantics type classes to support \glspl{GADT} is done by an easy textual search and replace.
All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskelllhstexinline{a}:
\begin{lstHaskellLhstex}
\section{Related work}%
\label{sec:cde:related}
-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.
+Embedded \gls{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}~\citep{swierstra_data_2008}.
In Swierstra's approach, semantics are lifted to type classes similarly to classy deep embedding.
repositories / phd-thesis.git / blobdiff