Deeply embedded languages represent their language constructs as data and the semantics are functions on it.
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.
+ This chapter 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 \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}
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.
+This chapter 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 \glspl{GADT}.
-While this paper is written as a literate
+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}.}
\section{Deep embedding}
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.}.
+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.}.
\begin{lstHaskellLhstex}
data Expr_0
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}.
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.
+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.
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 \gls{DSL} domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer.
\Citet{loh_open_2006} 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.
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.
+In contrast, this chapter 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 \citet{najd_trees_2017} to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form.
For example to decorate the abstract syntax tree of a compiler differently for each phase of the compiler.
& \CIRCLE{}\tnote{3}\\
Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
- & \LEFTcircle{}\tnote{4}\\
+ & \textcolor{gray}{\CIRCLE{}}\tnote{4}\\
Little boilerplate & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
- & \LEFTcircle{}\tnote{4}\\
+ & \textcolor{gray}{\CIRCLE{}}\tnote{4}\\
\bottomrule
\end{tabular}
\begin{tablenotes}
repositories / phd-thesis.git / blobdiff