\chapter{Deep embedding with class}%
\label{chp:classy_deep_embedding}
-\begin{quote}
+\begin{chapterabstract}
The two flavours of 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.
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.
Additionally, little type-level trickery or complicated boilerplate code is required to achieve this.
-\end{quote}
+\end{chapterabstract}
\section{Introduction}%
The two flavours of DSL embedding are deep and shallow embedding~\cite{boulton_experience_1992}.
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 \haskellinline{(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
+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.
\subsection{Tagless-final embedding}
Semantics become data types\footnotemark{} implementing these type classes, resulting in the following instance for the evaluator.
\footnotetext{%
- In this case \haskelllhstexinline{newtype}s are used instead of regular \haskellinline{data} declarations.
+ In this case \haskelllhstexinline{newtype}s are used instead of regular \haskelllhstexinline{data} declarations.
A \haskelllhstexinline{newtype} is a special data type with a single constructor containing a single value only to which it is isomorphic.
It allows the programmer to define separate class instances that the instances of the isomorphic type without any overhead.
During compilation the constructor is completely removed~\cite[Sec.~4.2.3]{peyton_jones_haskell_2003}.
\end{lstHaskellLhstex}
\section{Lifting the backends}%
-
Let us rethink the deeply embedded 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.
The astute reader might have noticed that we have dissociated ourselves from the original data type.
It is only possible to create an expression with a subtraction on the top level.
-The recursive knot is left untied and as a result, \haskelllhstexinline{Sub_1} can never be reached from an \haskellinline{Expr_1}.
+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.
\subsection{Unbraiding the semantics from the data}
This approach does reveal a minor problem.
Namely, that all semantics type classes are braided into our datatypes via the \haskelllhstexinline{Ext_2} constructor.
-Say if we add the printer again, the \haskelllhstexinline{Ext_2} constructor has to be modified to contain the printer type class constraint as well\footnote{Resulting in the following constructor: \haskellinline{forall x.(Eval_2 x, Print_2 x) => Ext_2 x}.}. %chktex 36
+Say if we add the printer again, the \haskelllhstexinline{Ext_2} constructor has to be modified to contain the printer type class constraint as well\footnote{Resulting in the following constructor: \haskelllhstexinline{forall x.(Eval_2 x, Print_2 x) => Ext_2 x}.}. %chktex 36
Thus, if we add semantics, the main data type's type class constraints in the \haskelllhstexinline{Ext_2} constructor need to be updated.
To avoid this, the type classes can be bundled in a type class alias or type class collection as follows.
data Expr_3 d = Lit_3 Int
| Add_3 (Expr_3 d) (Expr_3 d)
| forall x. Ext_3 (d x) x
-\end{lstHaskellLhstex}
-\begin{lstHaskellLhstex}
data Sub_3 d = Sub_3 (Expr_3 d) (Expr_3 d)
\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.
-This means that for \haskelllhstexinline{Eval_3}, a dictionary with the function \haskellinline{EvalDict_3} is defined, a type class \haskellinline{HasEval_3} for retrieving the function from the dictionary and an instance for \haskellinline{HasEval_3} for \haskellinline{EvalDict_3}.
+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}
newtype EvalDict_3 v = EvalDict_3 (v -> Int)
\end{lstHaskellLhstex}
The instances for the type classes change as well according to the change in the datatype.
-Given that there is a \haskelllhstexinline{HasEval_3} instance for the witness type \haskellinline{d}, we can provide an implementation of \haskellinline{Eval_3} for \haskellinline{Expr_3 d}.
+Given that there is a \haskelllhstexinline{HasEval_3} instance for the witness type \haskelllhstexinline{d}, we can provide an implementation of \haskelllhstexinline{Eval_3} for \haskelllhstexinline{Expr_3 d}.
\begin{lstHaskellLhstex}
instance HasEval_3 d => Eval_3 (Expr_3 d) where
eval_3 (Sub_3 e1 e2) = eval_3 e1 - eval_3 e2
\end{lstHaskellLhstex}
-Because the \haskelllhstexinline{Ext_3} constructor from \haskellinline{Expr_3} now contains a value of type \haskellinline{d}, the smart constructor for \haskellinline{Sub_3} must somehow come up with this value.
+Because the \haskelllhstexinline{Ext_3} constructor from \haskelllhstexinline{Expr_3} now contains a value of type \haskelllhstexinline{d}, the smart constructor for \haskelllhstexinline{Sub_3} must somehow come up with this value.
To achieve this, a type class is introduced that allows the generation of such a dictionary.
\begin{lstHaskellLhstex}
opt_3 (Ext_3 d x) = Ext_3 d (getOpt_3 d x)
\end{lstHaskellLhstex}
-Replicating this for the \haskelllhstexinline{Opt_3} instance of \haskellinline{Sub_3} seems a clear-cut task at first glance.
+Replicating this for the \haskelllhstexinline{Opt_3} instance of \haskelllhstexinline{Sub_3} seems a clear-cut task at first glance.
\begin{lstHaskellLhstex}
instance HasOpt_3 d => Opt_3 (Sub_3 d) where
\subsection{Convolution}%
-Adding a loopback case or convolution constructor to \haskelllhstexinline{Sub_3} allows the removal of the \haskellinline{Sub_3} constructor while remaining the \haskellinline{Sub_3} type.
+Adding a loopback case or convolution constructor to \haskelllhstexinline{Sub_3} allows the removal of the \haskelllhstexinline{Sub_3} constructor while remaining the \haskelllhstexinline{Sub_3} type.
It should be noted that a loopback case is \emph{only} required if the transformation actually removes tags.
This changes the \haskelllhstexinline{Sub_3} data type as follows.
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 \haskellinline{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.
-As a result, the \haskelllhstexinline{Typeable} type class constraints are added to the quantified type variable \haskellinline{x} of the \haskellinline{Ext_4} constructor and to \haskellinline{d}s in the smart constructors.
+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.
+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}
data Expr_4 d = Lit_4 Int
\begin{lstHaskellLhstex}
instance (Typeable d, GDict (d (Neg_4 d)), HasOpt_4 d) => Opt_4 (Neg_4 d) where
- opt_4 (Neg_4 (Add_4 e1 e2)) = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2)))
- opt_4 (Neg_4 (Ext_4 d x)) = case fromDynamic (toDyn (getOpt_4 d x)) of
- Just (Neg_4 e) -> NegLoop_4 e
- _ -> Neg_4 (Ext_4 d (getOpt_4 d x))
- opt_4 (Neg_4 e) = Neg_4 (opt_4 e)
- opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e)
+ opt_4 (Neg_4 (Add_4 e1 e2))
+ = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2)))
+ opt_4 (Neg_4 (Ext_4 d x))
+ = case fromDynamic (toDyn (getOpt_4 d x)) of
+ Just (Neg_4 e) -> NegLoop_4 e
+ _ -> Neg_4 (Ext_4 d (getOpt_4 d x))
+ opt_4 (Neg_4 e) = Neg_4 (opt_4 e)
+ opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e)
\end{lstHaskellLhstex}
Loopback cases do make cross-extensional pattern matching less modular in general.
-For example, \haskelllhstexinline{Ext_4 d (SubLoop_4 (Lit_4 0))} is equivalent to \haskellinline{Lit_4 0} in the optimisation semantics and would require an extra pattern match.
+For example, \haskelllhstexinline{Ext_4 d (SubLoop_4 (Lit_4 0))} is equivalent to \haskelllhstexinline{Lit_4 0} in the optimisation semantics and would require an extra pattern match.
Fortunately, this problem can be mitigated---if required---by just introducing an additional optimisation semantics that removes loopback cases.
Luckily, one does not need to resort to these arguably blunt matters often.
Dependent language functionality often does not need to span extensions, i.e.\ it is possible to group them in the same data type.
gdict = OPD_4 gdict gdict
\end{lstHaskellLhstex}
-And this allows us to write \haskelllhstexinline{print_4 (opt_4 e1)} resulting in \verb|"((~42)+(~38))"| when \haskellinline{e1} represents $(\sim(42+38))-0$ and is thus defined as follows.
+And this allows us to write \haskelllhstexinline{print_4 (opt_4 e1)} resulting in \verb|"((~42)+(~38))"| when \haskelllhstexinline{e1} represents $(\sim(42+38))-0$ and is thus defined as follows.
\begin{lstHaskellLhstex}
e1 :: Expr_4 OptPrintDict_4
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.
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 \haskellinline{Show} instance, required for the printer.
-Since some optimisations on \haskelllhstexinline{Not_g} remove constructors and therefore use cross-extensional pattern matches, \haskellinline{Typeable} constraints are added to \haskellinline{a}.
-Furthermore, because the optimisations for \haskelllhstexinline{Add_g} and \haskellinline{Sub_g} are now more general, they do not only work for \haskellinline{Int}s but for any type with a \haskellinline{Num} instance, the \haskellinline{Eq} constraint is added to these constructors as well.
+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.
+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.
The omitted definitions and implementation can be found in \cref{sec:cde:appendix}.
NotLoop_g :: Expr_g d a -> Not_g d a
\end{lstHaskellLhstex}
-The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskellinline{d} type variable for it to be usable in the \haskellinline{Ext_g} constructor as can be seen in the smart constructor for \haskellinline{Neg_g}:
+The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskelllhstexinline{d} type variable for it to be usable in the \haskelllhstexinline{Ext_g} constructor as can be seen in the smart constructor for \haskelllhstexinline{Neg_g}:
\begin{lstHaskellLhstex}
-neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) => Expr_g d a -> Expr_g d a
+neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) =>
+ Expr_g d a -> Expr_g d a
neg_g e = Ext_g gdict (Neg_g e)
-not_g :: (Typeable d, GDict (d (Not_g d))) => Expr_g d Bool -> Expr_g d Bool
+not_g :: (Typeable d, GDict (d (Not_g d))) =>
+ Expr_g d Bool -> Expr_g d Bool
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.
-All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskellinline{a}:
+All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskelllhstexinline{a}:
\begin{lstHaskellLhstex}
class Eval_g v where
\end{lstHaskellLhstex}
The \haskelllhstexinline{GDict} type class is general enough, so the instances can remain the same.
-The \haskelllhstexinline{Eval_g} instance of \haskellinline{GDict} looks as follows:
+The \haskelllhstexinline{Eval_g} instance of \haskelllhstexinline{GDict} looks as follows:
\begin{lstHaskellLhstex}
instance Eval_g v => GDict (EvalDict_g v) where
\begin{lstHaskellLhstex}
instance (Typeable d, GDict (d (Not_g d)), HasOpt_g d) => Opt_g (Not_g d) where
- opt_g (Not_g (Ext_g d x)) = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of
+ opt_g (Not_g (Ext_g d x))
+ = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of
Just (Not_g e) -> NotLoop_g e
_ -> Not_g (Ext_g d (getOpt_g d x))
- opt_g (Not_g e) = Not_g (opt_g e)
- opt_g (NotLoop_g e) = NotLoop_g (opt_g e)
+ opt_g (Not_g e) = Not_g (opt_g e)
+ opt_g (NotLoop_g e) = NotLoop_g (opt_g e)
\end{lstHaskellLhstex}
\section{Conclusion}%
opt_g (SubLoop_g e) = SubLoop_g (opt_g e)
instance (Typeable d, GDict (d (Neg_g d)), HasOpt_g d) => Opt_g (Neg_g d) where
- opt_g (Neg_g (Add_g e1 e2)) = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2)))
- opt_g (Neg_g (Ext_g d x)) = case fromDynamic (toDyn (getOpt_g d x)) of
+ opt_g (Neg_g (Add_g e1 e2))
+ = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2)))
+ opt_g (Neg_g (Ext_g d x))
+ = case fromDynamic (toDyn (getOpt_g d x)) of
Just (Neg_g e) -> NegLoop_g e
_ -> Neg_g (Ext_g d (getOpt_g d x))
opt_g (Neg_g e) = Neg_g (opt_g e)
repositories / phd-thesis.git / blobdiff