[phd-thesis.git] / dsl / class_deep_embedding.tex

\documentclass[../thesis.tex]{subfiles}

\include{subfilepreamble}

\begin{document}
\chapter{Deep embedding with class}%
\label{chp:classy_deep_embedding}

\begin{chapterabstract}
        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.

        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.
        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 \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.

On the other hand, deep embedding models language constructs as data in the host language.
The semantics of the language are represented by functions over the data.
Consequently, adding new semantics, i.e.\ novel functions, is straightforward.
It can be stated that the language constructs are embedded in the functions that form a semantics.
If one wants to add a language construct, all semantics functions must be revisited and revised to avoid ending up with partial functions.

This juxtaposition has been known for many years~\citep{reynolds_user-defined_1978} and discussed by many others~\citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler~\citep{wadler_expression_1998}:

\begin{quote}
        The \emph{expression problem} is a new name for an old problem.
        The goal is to define a data type by cases, where one can add new cases to the data type and new functions over the data type, without recompiling existing code, and while retaining static type safety (e.g., no casts).
\end{quote}

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 \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 \glspl{GADT}.
While this paper 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.}.

\begin{lstHaskellLhstex}
data Expr_0
        = Lit_0 Int
        | Add_0 Expr_0 Expr_0
\end{lstHaskellLhstex}

Semantics are defined as functions on the \haskelllhstexinline{Expr_0} data type.
For example, a function transforming the term to an integer---an evaluator---is implemented as follows.

\begin{lstHaskellLhstex}
eval_0 :: Expr_0 -> Int
eval_0 (Lit_0 e)     = e
eval_0 (Add_0 e1 e2) = eval_0 e1 + eval_0 e2
\end{lstHaskellLhstex}

Adding semantics---e.g.\ a printer---just means adding another function while the existing functions remain untouched.
I.e.\ the key property of deep embedding.
The following function, transforming the \haskelllhstexinline{Expr_0} data type to a string, defines a simple printer for our language.

\begin{lstHaskellLhstex}
print_0 :: Expr_0 -> String
print_0 (Lit_0 v)     = show v
print_0 (Add_0 e1 e2) = "(" ++ print_0 e1 ++ "-" ++ print_0 e2 ++ ")"
\end{lstHaskellLhstex}

While the language is concise and elegant, it is not very expressive.
Traditionally, extending the language is achieved by adding a case to the \haskelllhstexinline{Expr_0} data type.
So, adding subtraction to the language results in the following revised data type.

\begin{lstHaskellLhstex}
data Expr_0
        = Lit_0 Int
        | Add_0 Expr_0 Expr_0
        | Sub_0 Expr_0 Expr_0
\end{lstHaskellLhstex}

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.

\section{Shallow embedding}
Conversely, let us see how this would be done in shallow embedding.
First, the data type is represented by functions in the host language with embedded semantics.
Therefore, the evaluators for literals and addition both become a function in the host language as follows.

\begin{lstHaskellLhstex}
type Sem_s = Int

lit_s :: Int -> Sem_s
lit_s i = i

add_s :: Sem_s -> Sem_s -> Sem_s
add_s e1 e2 = e1 + e2
\end{lstHaskellLhstex}

Adding constructions to the language is done by adding functions.
Hence, the following function adds subtraction to our language.

\begin{lstHaskellLhstex}
sub_s :: Sem_s -> Sem_s -> Sem_s
sub_s e1 e2 = e1 - e2
\end{lstHaskellLhstex}

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 \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}\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.

\begin{lstHaskellLhstex}
class Expr_t s where
        lit_t :: Int -> s
        add_t :: s -> s -> s
\end{lstHaskellLhstex}

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 \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~\citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}.
}

\begin{lstHaskellLhstex}
newtype Eval_t = E_t Int

instance Expr_t Eval_t where
        lit_t v               = E_t v
        add_t (E_t e1) (E_t e2) = E_t (e1 + e2)
\end{lstHaskellLhstex}

Adding constructs---e.g.\ subtraction---just results in an extra type class and corresponding instances.

\begin{lstHaskellLhstex}
class Sub_t s where
        sub_t :: s -> s -> s

instance Sub_t Eval_t where
        sub_t (E_t e1) (E_t e2) = E_t (e1 - e2)
\end{lstHaskellLhstex}

Finally, adding semantics such as a printer over the language is achieved by providing a data type representing the semantics accompanied by instances for the language constructs.

\begin{lstHaskellLhstex}
newtype Printer_t = P_t String

instance Expr_t Printer_t where
        lit_t i               = P_t (show i)
        add_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "+" ++ e2 ++ ")")

instance Sub_t Printer_t where
        sub_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "-" ++ e2 ++ ")")
\end{lstHaskellLhstex}

\section{Lifting the backends}%
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.
So, let us apply the same technique, i.e.\ make the semantics overloaded in the language constructs by abstracting the semantics functions to type classes.
The same effect may be achieved when using similar techniques such as explicit dictionary passing or ML style modules.
In our language this results in the following type class.

\begin{lstHaskellLhstex}
class Eval_1 v where
        eval_1 :: v -> Int

data Expr_1
        = Lit_1 Int
        | Add_1 Expr_1 Expr_1
\end{lstHaskellLhstex}

Implementing the semantics type class instances for the \haskelllhstexinline{Expr_1} data type is an elementary exercise.
By a copy-paste and some modifications, we come to the following implementation.

\begin{lstHaskellLhstex}
instance Eval_1 Expr_1 where
        eval_1 (Lit_1 v)     = v
        eval_1 (Add_1 e1 e2) = eval_1 e1 + eval_1 e2
\end{lstHaskellLhstex}

Subtraction can now be defined in a separate data type, leaving the original data type intact.
Instances for the additional semantics can now be implemented separately as instances of the type classes.

\begin{lstHaskellLhstex}
data Sub_1 = Sub_1 Expr_1 Expr_1

instance Eval_1 Sub_1 where
        eval_1 (Sub_1 e1 e2) = eval_1 e1 - eval_1 e2
\end{lstHaskellLhstex}

\section{Existential data types}%

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 \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~\citep{mitchell_abstract_1988} type with type class constraints~\citep{laufer_combining_1994,laufer_type_1996} for all semantics type classes~\citep[\citesection{6.4.6}]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.

\begin{lstHaskellLhstex}
data Expr_2
        =                      Lit_2 Int
        |                      Add_2 Expr_2 Expr_2
        | forall x. Eval_2 x => Ext_2 x
\end{lstHaskellLhstex}

The implementation of the extension case in the semantics type classes is in most cases just a matter of calling the function for the argument as can be seen in the semantics instances shown below.

\begin{lstHaskellLhstex}
instance Eval_2 Expr_2 where
        eval_2 (Lit_2  v)      = v
        eval_2 (Add_2  e1 e2)  = eval_2 e1 + eval_2 e2
        eval_2 (Ext_2  x)      = eval_2 x
\end{lstHaskellLhstex}

Adding language construct extensions in different data types does mean that an extra \haskelllhstexinline{Ext_2} tag is introduced when using the extension.
This burden can be relieved by creating a smart constructor for it that automatically wraps the extension with the \haskelllhstexinline{Ext_2} constructor so that it is of the type of the main data type.

\begin{lstHaskellLhstex}
sub_2 :: Expr_2 -> Expr_2 -> Expr_2
sub_2 e1 e2 = Ext_2 (Sub_2 e1 e2)
\end{lstHaskellLhstex}

In our example this means that the programmer can write\footnotemark{}:
\footnotetext{%
        Backticks are used to use functions or constructors in an infix fashion~\citep[\citesection{4.3.3}]{peyton_jones_haskell_2003}.
}
\begin{lstHaskellLhstex}
e2 :: Expr_2
e2 = Lit_2 42 `sub_2` Lit_2 1
\end{lstHaskellLhstex}
instead of having to write
\begin{lstHaskellLhstex}
e2p :: Expr_2
e2p = Ext_2 (Lit_2 42 `Sub_2` Lit_2 1)
\end{lstHaskellLhstex}

\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: \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.

\begin{lstHaskellLhstex}
class (Eval_2 x, Print_2 x) => Semantics_2 x

data Expr_2
        =                           Lit_2 Int
        |                           Add_2 Expr_2 Expr_2
        | forall x. Semantics_2 x => Ext_2 x
\end{lstHaskellLhstex}

The class alias removes the need for the programmer to visit the main data type when adding additional semantics.
Unfortunately, the compiler does need to visit the main data type again.
Some may argue that adding semantics happens less frequently than adding language constructs but in reality it means that we have to concede that the language is not as easily extensible in semantics as in language constructs.
More exotic type system extensions such as constraint kinds~\citep{bolingbroke_constraint_2011,yorgey_giving_2012} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
However, by adding some boilerplate, even without this extension, the language constructs can be parametrised by the semantics by putting the semantics functions in a data type.
First the data types for the language constructs are parametrised by the type variable \haskelllhstexinline{d} as follows.

\begin{lstHaskellLhstex}
data Expr_3 d
        =           Lit_3 Int
        |           Add_3 (Expr_3 d) (Expr_3 d)
        | forall x. Ext_3 (d x) x

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 \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)

class HasEval_3 d where
        getEval_3 :: d v -> v -> Int

instance HasEval_3 EvalDict_3 where
        getEval_3 (EvalDict_3 e) = e
\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 \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 (Lit_3 v)     = v
        eval_3 (Add_3 e1 e2) = eval_3 e1 + eval_3 e2
        eval_3 (Ext_3 d x)   = getEval_3 d x

instance HasEval_3 d => Eval_3 (Sub_3 d) where
        eval_3 (Sub_3 e1 e2) = eval_3 e1 - eval_3 e2
\end{lstHaskellLhstex}

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}
class GDict a where
        gdict :: a
\end{lstHaskellLhstex}

This type class has individual instances for all semantics dictionaries, linking the class instance to the witness value.
I.e.\ if there is a type class instance known, a witness value can be conjured using the \haskelllhstexinline{gdict} function.

\begin{lstHaskellLhstex}
instance Eval_3 v => GDict (EvalDict_3 v) where
        gdict = EvalDict_3 eval_3
\end{lstHaskellLhstex}

With these instances, the semantics function can be retrieved from the \haskelllhstexinline{Ext_3} constructor and in the smart constructors they can be generated as follows:

\begin{lstHaskellLhstex}
sub_3 :: GDict (d (Sub_3 d)) => Expr_3 d -> Expr_3 d -> Expr_3 d
sub_3 e1 e2 = Ext_3 gdict (Sub_3 e1 e2)
\end{lstHaskellLhstex}

Finally, we reached the end goal, orthogonal extension of both language constructs as shown by adding subtraction to the language and in language semantics.
Adding the printer can now be done without touching the original code as follows.
First the printer type class, dictionaries and instances for \haskelllhstexinline{GDict} are defined.

\begin{lstHaskellLhstex}
class Print_3 v where
        print_3 :: v -> String

newtype PrintDict_3 v = PrintDict_3 (v -> String)

class HasPrint_3 d where
        getPrint_3 :: d v -> v -> String

instance HasPrint_3 PrintDict_3 where
        getPrint_3 (PrintDict_3 e) = e

instance Print_3 v => GDict (PrintDict_3 v) where
        gdict = PrintDict_3 print_3
\end{lstHaskellLhstex}

Then the instances for \haskelllhstexinline{Print_3} of all the language constructs can be defined.

\begin{lstHaskellLhstex}
instance HasPrint_3 d => Print_3 (Expr_3 d) where
        print_3 (Lit_3 v)     = show v
        print_3 (Add_3 e1 e2) = "(" ++ print_3 e1 ++ "+" ++ print_3 e2 ++ ")"
        print_3 (Ext_3 d x)   = getPrint_3 d x
instance HasPrint_3 d => Print_3 (Sub_3 d) where
        print_3 (Sub_3 e1 e2) = "(" ++ print_3 e1 ++ "-" ++ print_3 e2 ++ ")"
\end{lstHaskellLhstex}

\section{Transformation semantics}
Most semantics convert a term to some final representation and can be expressed just by functions on the cases.
However, the implementation of semantics such as transformation or optimisation may benefit from a so-called intentional analysis of the abstract syntax tree.
In shallow embedding, the implementation for these types of semantics is difficult because there is no tangible abstract syntax tree.
In off-the-shelf deep embedding this is effortless since the function can pattern match on the constructor or structures of constructors.

To demonstrate intensional analyses in classy deep embedding we write an optimizer that removes addition and subtraction by zero.
In classy deep embedding, adding new semantics means first adding a new type class housing the function including the machinery for the extension constructor.

\begin{lstHaskellLhstex}
class Opt_3 v where
        opt_3 :: v -> v

newtype OptDict_3 v = OptDict_3 (v -> v)

class HasOpt_3 d where
        getOpt_3 :: d v -> v -> v

instance HasOpt_3 OptDict_3 where
        getOpt_3 (OptDict_3 e) = e

instance Opt_3 v => GDict (OptDict_3 v) where
        gdict = OptDict_3 opt_3
\end{lstHaskellLhstex}

The implementation of the optimizer for the \haskelllhstexinline{Expr_3} data type is no complicated task.
The only interesting bit occurs in the \haskelllhstexinline{Add_3} constructor, where we pattern match on the optimised children to determine whether an addition with zero is performed.
If this is the case, the addition is removed.

\begin{lstHaskellLhstex}
instance HasOpt_3 d => Opt_3 (Expr_3 d) where
        opt_3 (Lit_3 v)     = Lit_3 v
        opt_3 (Add_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
                (Lit_3 0, e2p    ) -> e2p
                (e1p,     Lit_3 0) -> e1p
                (e1p,     e2p    ) -> Add_3 e1p e2p
        opt_3 (Ext_3 d x)   = Ext_3 d (getOpt_3 d x)
\end{lstHaskellLhstex}

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
        opt_3 (Sub_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
                (e1p, Lit_3 0) -> e1p
                (e1p, e2p    ) -> Sub_3 e1p e2p
\end{lstHaskellLhstex}

Unsurprisingly, this code is rejected by the compiler.
When a literal zero is matched as the right-hand side of a subtraction, the left-hand side of type \haskelllhstexinline{Expr_3} is returned.
However, the type signature of the function dictates that it should be of type \haskelllhstexinline{Sub_3}.
To overcome this problem we add a convolution constructor.

\subsection{Convolution}
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.

\begin{lstHaskellLhstex}
data Sub_4 d
        = Sub_4     (Expr_4 d) (Expr_4 d)
        | SubLoop_4 (Expr_4 d)

instance HasEval_4 d => Eval_4 (Sub_4 d) where
        eval_4 (Sub_4     e1 e2) = eval_4 e1 - eval_4 e2
        eval_4 (SubLoop_4 e1)    = eval_4 e1
\end{lstHaskellLhstex}

With this loopback case in the toolbox, the following \haskelllhstexinline{Sub} instance optimises away subtraction with zero literals.

\begin{lstHaskellLhstex}
instance HasOpt_4 d => Opt_4 (Sub_4 d) where
        opt_4 (Sub_4 e1 e2) = case (opt_4 e1, opt_4 e2) of
                (e1p, Lit_4 0) -> SubLoop_4 e1p
                (e1p, e2p    ) -> Sub_4 e1p e2p
        opt_4 (SubLoop_4 e) =  SubLoop_4 (opt_4 e)
\end{lstHaskellLhstex}

\subsection{Pattern matching}
Pattern matching within datatypes and from an extension to the main data type works out of the box.
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~\citep{abadi_dynamic_1991,baars_typing_2002}.
To enable dynamic typing support, the \haskelllhstexinline{Typeable} type class as provided by \haskelllhstexinline{Data.Dynamic}~\citep{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
        |                         Add_4 (Expr_4 d) (Expr_4 d)
        | forall x. Typeable x => Ext_4 (d x) x
\end{lstHaskellLhstex}

First let us add negation to the language by defining a datatype representing it.
Negation elimination requires the removal of negation constructors, so a convolution constructor is defined as well.

\begin{lstHaskellLhstex}
data Neg_4 d
        = Neg_4     (Expr_4 d)
        | NegLoop_4 (Expr_4 d)

neg_4 :: (Typeable d, GDict (d (Neg_4 d))) => Expr_4 d -> Expr_4 d
neg_4 e = Ext_4 gdict (Neg_4 e)
\end{lstHaskellLhstex}

The evaluation and printer instances for the \haskelllhstexinline{Neg_4} datatype are defined as follows.

\begin{lstHaskellLhstex}
instance HasEval_4 d => Eval_4 (Neg_4 d) where
        eval_4 (Neg_4     e) = negate (eval_4 e)
        eval_4 (NegLoop_4 e) = eval_4 e

instance HasPrint_4 d => Print_4 (Neg_4 d) where
        print_4 (Neg_4     e) = "(~" ++ print_4 e ++ ")"
        print_4 (NegLoop_4 e) = print_4 e
\end{lstHaskellLhstex}

The \haskelllhstexinline{Opt_4} instance contains the interesting bit.
If the sub expression of a negation is an addition, negation is propagated downwards.
If the sub expression is again a negation, something that can only be found out by a dynamic pattern match, it is replaced by a \haskelllhstexinline{NegLoop_4} constructor.

\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)
\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 \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.

\subsection{Chaining semantics}
Now that the data types are parametrised by the semantics a final problem needs to be overcome.
The data type is parametrised by the semantics, thus, using multiple semantics, such as evaluation after optimising is not straightforwardly possible.
Luckily, a solution is readily at hand: introduce an ad-hoc combination semantics.

\begin{lstHaskellLhstex}
data OptPrintDict_4 v = OPD_4 (OptDict_4 v) (PrintDict_4 v)

instance HasOpt_4   OptPrintDict_4 where
        getOpt_4   (OPD_4 v _) = getOpt_4 v
instance HasPrint_4 OptPrintDict_4 where
        getPrint_4 (OPD_4 _ v) = getPrint_4 v

instance (Opt_4 v, Print_4 v) => GDict (OptPrintDict_4 v) where
        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 \haskelllhstexinline{e1} represents $(\sim(42+38))-0$ and is thus defined as follows.

\begin{lstHaskellLhstex}
e1 :: Expr_4  OptPrintDict_4
e1 = neg_4 (Lit_4 42 `Add_4` Lit_4 38) `sub_4` Lit_4 0
\end{lstHaskellLhstex}

When using classy deep embedding to the fullest, the ability of the compiler to infer very general types expires.
As a consequence, defining reusable expressions that are overloaded in their semantics requires quite some type class constraints that cannot be inferred by the compiler (yet) if they use many extensions.
Solving this remains future work.
For example, the expression $\sim(42-38)+1$ has to be defined as:

\begin{lstHaskellLhstex}
e3 :: (Typeable d, GDict (d (Neg_4 d)), GDict (d (Sub_4 d))) => Expr_4 d
e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
\end{lstHaskellLhstex}

\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}.
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 \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.
The omitted definitions and implementation can be found in \cref{sec:cde:appendix}.

\begin{lstHaskellLhstex}
data Expr_g d a where
        Lit_g     :: Show a        => a -> Expr_g d a
        Add_g     :: (Eq a, Num a) => Expr_g d a -> Expr_g d a -> Expr_g d a
        Ext_g     :: Typeable x    => d x -> x a -> Expr_g d a
data Neg_g  d a where
        Neg_g     :: (Typeable a, Num a) => Expr_g d a -> Neg_g d a
        NegLoop_g ::                        Expr_g d a -> Neg_g d a
data Not_g  d a where
        Not_g     :: Expr_g d Bool -> Not_g d Bool
        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 \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 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 e = Ext_g gdict (Not_g e)
\end{lstHaskellLhstex}

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}
class Eval_g  v where
        eval_g  :: v a -> a
class Print_g v where
        print_g :: v a -> String
class Opt_g   v where
        opt_g   :: v a -> v a
\end{lstHaskellLhstex}

Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
The introduced type variable \haskelllhstexinline{a} is not an argument to the type class, so it should not be an argument to the dictionary data type.
To represent this type class function, a rank-2 polymorphic function is needed~\citep[\citesection{6.4.15}]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
Concretely, for the evaluatior this results in the following definitions:

\begin{lstHaskellLhstex}
newtype EvalDict_g v = EvalDict_g (forall a. v a -> a)
class HasEval_g d where
        getEval_g :: d v -> v a -> a
instance HasEval_g EvalDict_g where
        getEval_g (EvalDict_g e) = e
\end{lstHaskellLhstex}

The \haskelllhstexinline{GDict} type class is general enough, so the instances can remain the same.
The \haskelllhstexinline{Eval_g} instance of \haskelllhstexinline{GDict} looks as follows:

\begin{lstHaskellLhstex}
instance Eval_g v => GDict (EvalDict_g v) where
        gdict = EvalDict_g eval_g
\end{lstHaskellLhstex}

Finally, the implementations for the instances can be ported without complication show using the optimisation instance of \haskelllhstexinline{Not_g}:

\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
                        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)
\end{lstHaskellLhstex}

\section{Conclusion}%

Classy deep embedding is a novel organically grown embedding technique that alleviates deep embedding from the extensibility problem in most cases.

By abstracting the semantics functions to type classes they become overloaded in the language constructs.
Thus, making it possible to add new language constructs in a separate type.
These extensions are brought together in a special extension constructor residing in the main data type.
This extension case is overloaded by the language construct using a data type containing the class dictionary.
As a result, orthogonal extension is possible for language constructs and semantics using only little syntactic overhead or type annotations.
The basic technique only requires---well established through history and relatively standard---existential data types.
However, if needed, the technique generalises to \glspl{GADT} as well, adding rank-2 types to the list of type system requirements as well.
Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.

Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.

\section{Related work}%
\label{sec:cde:related}

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 \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.
Because all the constructs are expressed in the type system, nifty type system tricks need to be employed to convince the compiler that everything is type safe and the class constraints can be solved.
Furthermore, it requires some boilerplate code such as functor instances for the data types.
In return, pattern matching is easier and does not require dynamic typing.
Classy deep embedding only strains the programmer with writing the extension case for the main data type and the occasional loopback constructor.

\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.

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.
They propose to add an extension descriptor as a type variable to a data type and a type family that can be used to decorate constructors with extra information and add additional constructors to the data type using an extension constructor.
Classy deep embedding works similarly but uses existentially quantified type variables to describe possible extensions instead of type variables and type families.
In classy deep embedding, the extensions do not need to be encoded in the type system and less boilerplate is required.
Furthermore, pattern matching on extensions becomes a bit more complicated but in return it allows for multiple extensions to be added orthogonally and avoids the necessity for type system extensions.

Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding~\citep{carette_finally_2009}.
Classy deep embedding was organically grown from observing the evolution of tagless-final embedding.
The main difference between tagless-final embedding and classy deep embedding---and in general between shallow and deep embedding---is that intensional analyses of the abstract syntax tree is more difficult because there is no tangible abstract syntax tree data structure.
In classy deep embedding, it is possible to define transformations even across extensions.
Furthermore, in classy deep embedding, defining (mutual) dependent interpretations is automatically supported whereas in tagless-final embedding this requires some amount of code duplication \citep{sun_compositional_2022}.

Hybrid approaches between deep and shallow embedding exist as well.
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}
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.

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} 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}[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 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
        = Lit Int
        | Add (Expr c) (Expr c)
        | Ext (Record x c) x
\end{lstHaskellLhstex}

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 :: Record dt cs -> Dict (c dt)
instance {-# OVERLAPPING #-} c `In` (c ': cs) where
        project (Cons _) = Dict
instance {-# OVERLAPPING #-} c `In` cs => c `In` (b ': cs) where
        project (Cons xs) = project xs
\end{lstHaskellLhstex}

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
        createRecord :: Record dt c
instance CreateRecord d '[] where
        createRecord = Nil
instance (c (d c0), CreateRecord (d c0) cs) =>
                CreateRecord (d c0) (c ': cs) where
        createRecord = Cons createRecord
\end{lstHaskellLhstex}

The class constraints for the interpretation instances can now be greatly simplified, as shown in the evaluation instance for \haskelllhstexinline{Expr}.
The implementation remains the same, only that for the extension case, a trick needs to be applied to convince the compiler of the correct instances.
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 not smaller than the instance head, \GHCmod{UndecidableInstances} should be enabled.

\begin{lstHaskellLhstex}
class Eval v where
        eval :: v -> Int

instance Eval `In` s => Eval (Expr s) where
        eval (Lit i) = i
        eval (Add l r) = eval l + eval r
        eval (Ext r (e :: x)) = withDict (project r :: Dict (Eval x)) eval e
\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}
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 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}
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 in a similar fashion as was required for \haskelllhstexinline{GDict}.
At the call site, the concrete list of constraints must be known.

\begin{lstHaskellLhstex}
e1 :: (Typeable c
        , CreateRecord (Neg c) c
        , CreateRecord (Subst c) c
        ) => Expr c
e1 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
\end{lstHaskellLhstex}

Finally, using the \GHCmod{TypeFamilies} extension, type families can be created for bundling \haskelllhstexinline{`In`} constraints (\haskelllhstexinline{UsingExt}) and \haskelllhstexinline{CreateRecord} constraints (\haskelllhstexinline{DependsOn}), making the syntax even more descriptive.
E.g.\ \haskelllhstexinline{UsingExt '[A, B, C] c} expands to \haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)} and \haskelllhstexinline{DependsOn '[A, B, C] s} expands to \haskelllhstexinline{(A `In` s, B `In` s, C `In` s)}.

\begin{lstHaskellLhstex}
type family UsingExt cs c :: Constraint where
        UsingExt '[] c = ()
        UsingExt (d ': cs) c = (CreateRecord (d c) c, UsingExt cs c)

type family DependsOn cs c :: Constraint where
        DependsOn '[] c = ()
        DependsOn (d ': cs) c = (d `In` c, DependsOn cs c)
\end{lstHaskellLhstex}

Defining the previous expression can now be done with the following shortened type that describes the semantics better:

\begin{lstHaskellLhstex}
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:

\begin{lstHaskellLhstex}
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.}]
data Sub_g d a where
        Sub_g     :: (Eq a, Num a)      => Expr_g d a -> Expr_g d a -> Sub_g d a
        SubLoop_g ::                       Expr_g d a -> Sub_g d a

data Eq_g d a  where
        Eq_g      :: (Typeable a, Eq a) => Expr_g d a -> Expr_g d a -> Eq_g d Bool
        EqLoop_g  ::                       Expr_g d a -> Eq_g d a
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={Smart constructions.}]
sub_g :: (Typeable d, GDict (d (Sub_g d)), Eq a, Num a) =>
        Expr_g d a -> Expr_g d a -> Expr_g d a
sub_g e1 e2 = Ext_g gdict (Sub_g e1 e2)

eq_g :: (Typeable d, GDict (d (Eq_g d)), Eq a, Typeable a) =>
        Expr_g d a -> Expr_g d a -> Expr_g d Bool
eq_g e1 e2 = Ext_g gdict (Eq_g e1 e2)
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={Semantics classes and data types.}]
newtype PrintDict_g v = PrintDict_g (forall a.v a -> String)

class HasPrint_g d where
        getPrint_g :: d v -> v a -> String

instance HasPrint_g PrintDict_g where
        getPrint_g (PrintDict_g e) = e

newtype OptDict_g v = OptDict_g (forall a.v a -> v a)

class HasOpt_g d where
        getOpt_g :: d v -> v a -> v a

instance HasOpt_g OptDict_g where
        getOpt_g (OptDict_g e) = e
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={\texorpdfstring{\haskelllhstexinline{GDict}}{GDict} instances}]
instance Print_g v => GDict (PrintDict_g v) where
        gdict = PrintDict_g print_g
instance Opt_g v   => GDict (OptDict_g v)   where
        gdict = OptDict_g opt_g
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={Evaluator instances}]
instance HasEval_g d => Eval_g (Expr_g d) where
        eval_g (Lit_g v)     = v
        eval_g (Add_g e1 e2) = eval_g e1 + eval_g e2
        eval_g (Ext_g d x)   = getEval_g d x

instance HasEval_g d => Eval_g (Sub_g d) where
        eval_g (Sub_g     e1 e2) = eval_g e1 - eval_g e2
        eval_g (SubLoop_g e)     = eval_g e

instance HasEval_g d => Eval_g (Neg_g d) where
        eval_g (Neg_g     e) = negate (eval_g e)
        eval_g (NegLoop_g e) = eval_g e

instance HasEval_g d => Eval_g (Eq_g d) where
        eval_g (Eq_g     e1 e2) = eval_g e1 == eval_g e2
        eval_g (EqLoop_g e)     = eval_g e

instance HasEval_g d => Eval_g (Not_g d) where
        eval_g (Not_g     e) = not (eval_g e)
        eval_g (NotLoop_g e) = eval_g e
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={Printer instances}]
instance HasPrint_g d => Print_g (Expr_g d) where
        print_g (Lit_g v)     = show v
        print_g (Add_g e1 e2) = "(" ++ print_g e1 ++ "+" ++ print_g e2 ++ ")"
        print_g (Ext_g d x)   = getPrint_g d x

instance HasPrint_g d => Print_g (Sub_g d) where
        print_g (Sub_g     e1 e2) = "(" ++ print_g e1 ++ "-" ++ print_g e2 ++ ")"
        print_g (SubLoop_g e)     = print_g e

instance HasPrint_g d => Print_g (Neg_g d) where
        print_g (Neg_g     e) = "(negate " ++ print_g e ++ ")"
        print_g (NegLoop_g e) = print_g e

instance HasPrint_g d => Print_g (Eq_g d) where
        print_g (Eq_g     e1 e2) = "(" ++ print_g e1 ++ "==" ++ print_g e2 ++ ")"
        print_g (EqLoop_g e)     = print_g e

instance HasPrint_g d => Print_g (Not_g d) where
        print_g (Not_g     e) = "(not " ++ print_g e ++ ")"
        print_g (NotLoop_g e) = print_g e
\end{lstHaskellLhstex}

\begin{lstHaskellLhstex}[caption={Optimisation instances}]
instance HasOpt_g d => Opt_g (Expr_g d) where
        opt_g (Lit_g v)     = Lit_g v
        opt_g (Add_g e1 e2) = case (opt_g e1, opt_g e2) of
                (Lit_g 0, e2p    ) -> e2p
                (e1p,     Lit_g 0) -> e1p
                (e1p,     e2p    ) -> Add_g e1p e2p
        opt_g (Ext_g d x)   = Ext_g d (getOpt_g d x)

instance HasOpt_g d => Opt_g (Sub_g d) where
        opt_g (Sub_g     e1 e2) = case (opt_g e1, opt_g e2) of
                (e1p, Lit_g 0) -> SubLoop_g e1p
                (e1p, e2p    ) -> Sub_g e1p e2p
        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
                        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)
        opt_g (NegLoop_g e) = NegLoop_g (opt_g e)

instance HasOpt_g d => Opt_g (Eq_g d) where
        opt_g (Eq_g     e1 e2) = Eq_g (opt_g e1) (opt_g e2)
        opt_g (EqLoop_g e)     = EqLoop_g (opt_g e)
\end{lstHaskellLhstex}

\end{subappendices}

\input{subfilepostamble}
\end{document}