\documentclass[../thesis.tex]{subfiles}
-\begin{document}
-\ifSubfilesClassLoaded{
- \pagenumbering{arabic}
-}{}
+\include{subfilepreamble}
+\begin{document}
\chapter{Deep embedding with class}%
\label{chp:classy_deep_embedding}
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~\citep{gibbons_folding_2014}, delaying the selection of semantics to the moment the fold is applied.
-\subsection{Tagless-final embedding}
+\subsection{Tagless-final embedding}\label{sec:tagless-final_embedding}
Tagless-final embedding overcomes the limitations of standard shallow embedding.
To upgrade to this embedding technique, the language constructs are changed from functions to type classes.
For our language this results in the following type class definition.
e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
\end{lstHaskellLhstex}
-\section{\texorpdfstring{\Acrlongpl{GADT}}{Generalised algebraic data types}}%
+\section{\texorpdfstring{\Glsxtrlongpl{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[\citesection{2.2}]{cheney_lightweight_2002}.
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.
+In \citeauthor{swierstra_data_2008}'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 classy deep embedding, extensions only have to be enumerated at the type level when the term is required to be overloaded, in all other cases they are captured in the extension case.
For example, \citet{svenningsson_combining_2013} show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well.
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.
+\subsection{Comparison}
+\todo[inline]{text moet beter}
+There is no silver bullet to embedding \glspl{DSL}.
+\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two statet in the expression problem.
+
+\Cref{tbl:dsl_comparison_brief} shows a variant of their comparison table.
+The first two rows describe the two axes of the original expression problem and the third row describes theadded axis of modular dependency handling as stated by \citeauthor{sun_compositional_2022}.
+The \emph{poly.} style of embedding---including tagless-final---falls short of this requirement.
+
+Intensional analysis is an umbrella term for pattern matching and transformations.
+In shallow embedding, intensional analysis is more complex and requires stateful views describing context but it is possible to implement though.
+
+Simple type system describes the whether it is possible to encode this embedding technique with 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.
+For example, hybrid embedding requires a transcoding step between the deep syntax and the shallow core language.
+
+\begin{table}[ht]
+ \begin{threeparttable}[b]
+ \small
+ \caption{Comparison of embedding techniques, extended from \citet[\citesection{3.6}]{sun_compositional_2022}.}%
+ \label{tbl:dsl_comparison_brief}
+ \begin{tabular}{llllllll}
+ \toprule
+ & Shallow & Deep & Hybrid
+ & Poly. & Comp. & \`a la
+ & Classy\\
+ \midrule
+ Extend constructs & \CIRCLE{} & \Circle{} & \LEFTcircle{}\tnote{1}
+ & \CIRCLE{} & \CIRCLE{} & \CIRCLE{}
+ & \CIRCLE{}\\
+ Extend views & \Circle{} & \CIRCLE{} & \CIRCLE{}
+ & \CIRCLE{} & \CIRCLE{} & \CIRCLE{}
+ & \CIRCLE{}\\
+ Modular dependencies & \Circle{} & \CIRCLE{} & \CIRCLE{}
+ & \Circle{} & \CIRCLE{} & \CIRCLE{}
+ & \CIRCLE{}\\
+ Intensional analysis & \LEFTcircle{}\tnote{2} & \CIRCLE{} & \CIRCLE{}
+ & \LEFTcircle{}\tnote{2} & \LEFTcircle{}\tnote{2} & \CIRCLE{}
+ & \LEFTcircle{}\tnote{3}\\
+ Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{}
+ & \CIRCLE{} & \CIRCLE{} & \Circle{}
+ & \LEFTcircle{}\tnote{4}\\
+ Little boilerplate & \CIRCLE{} & \CIRCLE{} & \Circle{}
+ & \CIRCLE{} & \CIRCLE{} & \Circle{}
+ & \LEFTcircle{}\tnote{4}\\
+ \bottomrule
+ \end{tabular}
+ \begin{tablenotes}
+ \item [1] Only if the extension is expressible in the core language.
+ \item [2] Requires ingenuity and are sometimes awkward to write.
+ \item [3] Cross-extensional pattern matching requires \emph{safe} dynamic typing.
+ \item [4] Either a simple type system or little boilerplate.
+ \end{tablenotes}
+ \end{threeparttable}
+\end{table}
+
\section*{Acknowledgements}
This research is partly funded by the Royal Netherlands Navy.
Furthermore, I would like to thank Pieter and Rinus for the fruitful discussions, Ralf for inspiring me to write a functional pearl, and the anonymous reviewers for their valuable and honest comments.
\begin{subappendices}
-\section{Reprise: reducing boilerplate}\label{sec:classy_reprise}
-\todo{Improve text}
+\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.
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 of the boilerplate can be inferred or generated\footnote{The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.}.
+If we are willing to work with extensions, almost all of the boilerplate can be inferred or generated.
-The \gls{DSL} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
+In classy deep embedding, the \gls{DSL} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
When using multiple interpretations, these need to be bundled in a data type.
Using the \gls{GHC}'s \GHCmod{ConstraintKind} extension, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
Furthermore, this constraint does not necessarily has to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead.
-The data type for this list of witnesses is \haskelllhstexinline{Record}.
-The \haskelllhstexinline{Record} \gls{GADT} is parametrised by two type variables, the first type variable (\haskelllhstexinline{dt}) is the data type on which the constraints can be applied.
-The second type variable (\haskelllhstexinline{clist}) is the list of constraints itself.
-It is not just a list of \haskelllhstexinline{Constraint} but it is a list containing constraint constructors that will, when given a type of the polymorphic kind \haskelllhstexinline{k}, produce a constraint.
-This means that when \haskelllhstexinline{Cons} is pattern matched, the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
-\GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of the data type is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL}s using type classes but also type constructor classes (e.g.\ when using \glspl{GADT})..
+The data type for this list of witnesses is \haskelllhstexinline{Record} as shown in \cref{lst_cbde:record_type}.
+This \gls{GADT} is parametrised by two type variables.
+The first type variable (\haskelllhstexinline{dt}) is the type or type constructor on which the constraints can be applied and the second type variable (\haskelllhstexinline{clist}) is the list of constraints constructors itself.
+This means that when \haskelllhstexinline{Cons} is pattern matched, the overloading of the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
+\GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of \haskelllhstexinline{dt} is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL} using type classes but also type constructor classes (e.g.\ when using \glspl{GADT}).
-\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+\begin{lstHaskellLhstex}[label={lst_cbde:record_type},caption={Data type for a list of constraints}]
data Record (dt :: k) (clist :: [k -> Constraint]) where
Nil :: Record dt '[]
Cons :: c dt => Record dt cs -> Record dt (c ': cs)
\end{lstHaskellLhstex}
-To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes as follows:
+To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes from containing a single witness dictionary to a \haskelllhstexinline{Record} type containing all the required dictionaries.
\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
data Expr c
| Ext (Record x c) x
\end{lstHaskellLhstex}
-Furthermore, we define a type class that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
+Furthermore, we define a type class (\haskelllhstexinline{In}) that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
+Since the constraints become available as soon as the \haskelllhstexinline{Cons} constructor is matched, the implementation is a trivial type-level list traversal.
\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
class c `In` cs where
project (Cons xs) = project xs
\end{lstHaskellLhstex}
-Finally, creating these \haskelllhstexinline{Record} witnesses is a chore so this can be automated as well using a \haskelllhstexinline{CreateRecord} multi-parameter type class (requiring the \GHCmod{MultiParamTypeclasses} and \GHCmod{FlexibleInstances} extension).
+The final scaffolding is a multi-parameter type class \haskelllhstexinline{CreateRecord} (requiring the \GHCmod{MultiParamTypeclasses} and \GHCmod{FlexibleInstances} extension) to create these \haskelllhstexinline{Record} witnesses automatically.
This type class creates a record structure cons by cons if and only if all type class constraints are available in the list of constraints.
+It is not required to provide instances for this for specific records or type classes, the two instances describe all the required constraints.
\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
class CreateRecord dt c where
Using \haskelllhstexinline{`In`}'s \haskelllhstexinline{project} function, a dictionary can be brought into scope.
This dictionary can then subsequently be used to apply the type class function on the extension using the \haskelllhstexinline{withDict} function from the \haskelllhstexinline{Data.Constraint} library\footnote{\haskelllhstexinline{withDict :: Dict c -> (c => r) -> r}}.
The \GHCmod{ScopedTypeVariables} extension is used to make sure the existentially quantified type variable for the extension is matched to the type of the dictionary.
-Furthermore, because the class constraint is seemingly not smaller than the instance head, \GHCmod{UndecidableInstances} should be enabled.
+Furthermore, because the class constraint is not smaller than the instance head, \GHCmod{UndecidableInstances} should be enabled.
-\begin{lstHaskellLhstex}[caption={Evaluation instance for the main data type}]
+\begin{lstHaskellLhstex}
class Eval v where
eval :: v -> Int
\end{lstHaskellLhstex}
Smart constructors need to be adapted as well, as can be seen from the smart constructor \haskelllhstexinline{subst}.
+Instead of a \haskelllhstexinline{GDict} class constraint, a \haskelllhstexinline{CreateRecord} class constraint needs to be added.
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
-subst :: (Typeable c, CreateRecord (Subt c) c) => Expr c -> Expr c -> Expr c
+\begin{lstHaskellLhstex}
+subst :: (Typeable c, CreateRecord (Subt c) c)
+ => Expr c -> Expr c -> Expr c
subst l r = Ext createRecord (l `Subt` r)
\end{lstHaskellLhstex}
-Finally, defining terms in the language is can be done immediately if the interpretations are known.
-For example, if we want to print and/or optimise the term $~(~(42+(38-4)))$, we can define it as follows.
+Finally, defining terms in the language can be done immediately if the interpretations are known.
+For example, if we want to print and/or optimise the term $~(~(42+(38-4)))$, we can define it as follows:
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+\begin{lstHaskellLhstex}
e0 :: Expr '[Print,Opt]
e0 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
\end{lstHaskellLhstex}
It is also possible to define terms in the \gls{DSL} as being overloaded in the interpretation.
-This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension.
+This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension in a similar fashion as was required for \haskelllhstexinline{GDict}.
At the call site, the concrete list of constraints must be known.
-\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+\begin{lstHaskellLhstex}
e1 :: (Typeable c
, CreateRecord (Neg c) c
, CreateRecord (Subst c) c
e1 :: (Typeable c, UsingExt '[Neg, Subst]) => Expr c
\end{lstHaskellLhstex}
-Giving an instance for \haskelllhstexinline{Interp} for \haskelllhstexinline{DataType} that uses the extensions \haskelllhstexinline{e_1,e2,...} and depends on interpretations \haskelllhstexinline{i_1,i_2,...} is done as follows:
+Giving an instance for \haskelllhstexinline{Interp} for \haskelllhstexinline{DataType} that uses the extensions \haskelllhstexinline{e_1, e2, ...} and depends on interpretations \haskelllhstexinline{i_1,i_2, ...} is done as follows:
\begin{lstHaskellLhstex}
-instance ( UsingExt '[e_1,e_2,...] s
- , DependsOn '[i_1, i_2,...] s
+instance ( UsingExt '[e_1, e_2, ...] s
+ , DependsOn '[i_1, i_2, ...] s
) => Interp (DataType s) where
...
\end{lstHaskellLhstex}
+With these enhancements, there is hardly any boilerplate required to use classy deep embedding.
+The \haskelllhstexinline{Record} data type; the \haskelllhstexinline{CreateRecord} type class; and the \haskelllhstexinline{UsingExt} and \haskelllhstexinline{DependsOn} type families can be provided as a library only requiring the programmer to create the extension constructors with their respective implementations and smart constructors for language construct extensions.
+The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.
+
\section{Data types and definitions}%
\label{sec:cde:appendix}
\begin{lstHaskellLhstex}[caption={Data type definitions.}]
repositories / phd-thesis.git / blobdiff