\documentclass[../thesis.tex]{subfiles}
-\include{subfilepreamble}
+\input{subfilepreamble}
+
+\setcounter{chapter}{1}
\begin{document}
+\input{subfileprefix}
\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.
\end{chapterabstract}
\section{Introduction}
-The two flavours of \gls{DSL} embedding are deep and shallow embedding~\citep{boulton_experience_1992}.
+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.
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}:
+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 \citet{wadler_expression_1998}:
\begin{quote}
The \emph{expression problem} is a new name for an old problem.
\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.
+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}.
+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.
+\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}.}
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.
+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.
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}.
+ During compilation the constructor is completely removed \citep[\citesection{4.2.3}]{peyton_jones_haskell_2003}.
}
\begin{lstHaskellLhstex}
sub_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "-" ++ e2 ++ ")")
\end{lstHaskellLhstex}
-\section{Lifting the backends}%
+\section{Lifting the interpretations}%
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.
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.
+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
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}.
+ 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
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.
+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.
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.
+To demonstrate intensional analyses in classy deep embedding we write an optimiser 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}
gdict = OptDict_3 opt_3
\end{lstHaskellLhstex}
-The implementation of the optimizer for the \haskelllhstexinline{Expr_3} data type is no complicated task.
+The implementation of the optimiser 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.
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.
+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}
\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.
+As a consequence, defining reuseable 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:
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}.
+\section{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}.
+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.
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}:
+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 useable 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) =>
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:
+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 evaluator this results in the following definitions:
\begin{lstHaskellLhstex}
newtype EvalDict_g v = EvalDict_g (forall a. v a -> a)
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}.
+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, 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}.
+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.
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.
+Classy deep embedding differs from the hybrid approaches in the sense that it does not require the language extensions to be expressible in the core language.
\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.
+No \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requirements programmers have.
+\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two stated 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 first two rows describe the two axes of the original expression problem and the third row describes the added 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.
+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.
+Simple type system describes the whether it is possible to encode this embedding technique without 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{table}
\begin{threeparttable}[b]
\small
\caption{Comparison of embedding techniques, extended from \citet[\citesection{3.6}]{sun_compositional_2022}.}%
& \CIRCLE{}\\
Intensional analysis & \LEFTcircle{}\tnote{2} & \CIRCLE{} & \CIRCLE{}
& \LEFTcircle{}\tnote{2} & \LEFTcircle{}\tnote{2} & \CIRCLE{}
- & \LEFTcircle{}\tnote{3}\\
+ & \CIRCLE{}\tnote{3}\\
Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{}
& \CIRCLE{} & \CIRCLE{} & \Circle{}
& \LEFTcircle{}\tnote{4}\\
\end{threeparttable}
\end{table}
+\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 reuseable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around these issues remains future work.
+\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.
+
\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.
\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.
+If we are willing to work with extensions, almost all 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.
+Furthermore, this constraint does not necessarily have to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead \citep{yorgey_giving_2012}.
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}]
+\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)
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}]
+\begin{lstHaskellLhstex}[caption={Main data type with extension constructor.}]
data Expr c
= Lit Int
| Add (Expr c) (Expr c)
\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.
+Since the constraints become available as soon as the \haskelllhstexinline{Cons} constructor is matched, the implementation is a type-level list traversal.
-\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+\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
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}]
+\begin{lstHaskellLhstex}[caption={Functions for creating the witness records.}]
class CreateRecord dt c where
createRecord :: Record dt c
instance CreateRecord d '[] where
\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:
+For example, if we want to print and/or optimise the term $\displaystyle ~(~(42+(38-4)))$, we can define it as follows:
\begin{lstHaskellLhstex}
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 in a similar fashion as was required for \haskelllhstexinline{GDict}.
+This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension similarly 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 :: (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)}.
+Finally, using the \GHCmod{TypeFamilies} extension, type families can be created for bundling \haskelllhstexinline{`In`} constraints (\haskelllhstexinline{UsingExt}) and \haskelllhstexinline{CreateRecord} constraints \mbox{(\haskelllhstexinline{DependsOn})}, making the syntax even more descriptive.
+E.g.\ \mbox{\haskelllhstexinline{UsingExt '[A, B, C] c}} expands to\newline\haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)}.
+\hspace{-1.42284pt} Similarly, \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
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
+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}.
+The source code for this extension can be found here: \url{https://gitlab.com/mlubbers/classydeepembedding}.\footnote{Lubbers, M. (2022): Library and examples for enhanced classy deep embedding.\ Zenodo.\ \href{https://doi.org/10.5281/zenodo.7277498}{10.5281/zenodo.7277498}.}
+It contains examples for expressions, expressions using \glspl{GADT}, detection of sharing in expressions (modelled after \citet{kiselyov_implementing_2011}), a \gls{GADT} version of sharing detection, and a region \gls{DSL} (modelled after \citet{sun_compositional_2022}).
\section{Data types and definitions}%
\label{sec:cde:appendix}
+This appendix collects all definitions omitted for brevity.
+
+\lstset{basicstyle=\tt\footnotesize}
\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
EqLoop_g :: Expr_g d a -> Eq_g d a
\end{lstHaskellLhstex}
-\begin{lstHaskellLhstex}[caption={Smart constructions.}]
+\begin{lstHaskellLhstex}[caption={Smart constructors.}]
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)
getOpt_g (OptDict_g e) = e
\end{lstHaskellLhstex}
-\begin{lstHaskellLhstex}[caption={\texorpdfstring{\haskelllhstexinline{GDict}}{GDict} instances}]
+\begin{lstHaskellLhstex}[caption={{\tt 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}]
+\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 (NotLoop_g e) = eval_g e
\end{lstHaskellLhstex}
-\begin{lstHaskellLhstex}[caption={Printer instances}]
+\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 (NotLoop_g e) = print_g e
\end{lstHaskellLhstex}
-\begin{lstHaskellLhstex}[caption={Optimisation instances}]
+\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
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}
+\lstset{basicstyle=\tt\small}
\end{subappendices}
repositories / phd-thesis.git / blobdiff