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.
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}
+\section{Reprise: reducing boilerplate}%
+\label{sec:classy_reprise}
\todo{Improve text}
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}]
class Eval v where
\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
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}]
e0 :: Expr '[Print,Opt]
\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}]
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
...
\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