From 40dfd7d1e32916bce678f7078ec178cb793cc872 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 22 Sep 2022 16:41:53 +0200 Subject: [PATCH] insert first-class datatype --- domain-specific_languages/.chktexrc | 22 + .../first-class_datatypes.tex | 898 +++++++++++++++++- glossaries.tex | 4 + lstlanghaskell.sty | 65 +- other.bib | 668 ++++++++++++- preamble.tex | 45 +- 6 files changed, 1672 insertions(+), 30 deletions(-) create mode 100644 domain-specific_languages/.chktexrc diff --git a/domain-specific_languages/.chktexrc b/domain-specific_languages/.chktexrc new file mode 100644 index 0000000..bf386c6 --- /dev/null +++ b/domain-specific_languages/.chktexrc @@ -0,0 +1,22 @@ +CmdLine { + -v +} +VerbEnvir { + lstinline lstlisting algorithm code spec lstClean lstHaskell lstHaskellLhstex lstArduino +} +WipeArg { + \cleaninline:{} + \haskellinline:{} + \haskelllshtexinline:{} + \arduinoinline:{} + \texttt:{} + \url:{} + \only:{} + \orcid:{} +} +Silent { + \pause +} +MathEnvir { + code +} diff --git a/domain-specific_languages/first-class_datatypes.tex b/domain-specific_languages/first-class_datatypes.tex index 7e277fb..683f57d 100644 --- a/domain-specific_languages/first-class_datatypes.tex +++ b/domain-specific_languages/first-class_datatypes.tex @@ -5,8 +5,902 @@ \pagenumbering{arabic} }{} -\mychapter{chp:first-class_datatypes}{First-class datatypes \ldots}% -TFP22 +\chapter[First-class data types in shallow \acrshortpl{EDSL} using metaprogramming]{First-class data types in shallow \acrlongpl{EDSL} using metaprogramming}% +\label{chp:first-class_datatypes}% +\begin{chapterabstract} + Functional programming languages are excellent candidates for hosting \glspl{EDSL} because of their rich type systems, minimal syntax, and referential transparency. + However, data types defined in the host language are not automatically available in the embedded language. + To do so, all the operations on the data type must be ported to the \gls{EDSL} resulting in a lot of boilerplate. + + This paper shows that by using metaprogramming, all first order user-defined data types can be automatically made first class in shallow \glspl{EDSL}. + We show this by providing an implementation in \gls{TH} for a typical \gls{DSL} with two different semantics. + Furthermore, we show that by utilising quasiquotation, there is hardly any burden on the syntax. + Finally, the paper also serves as a gentle introduction to \gls{TH}. +\end{chapterabstract} + +\section{Introduction} +Functional programming languages are excellent candidates for hosting \glspl{EDSL} because of their rich type systems, minimal syntax, and referential transparency. +By expressing the language constructs in the host language, the parser, the type checker, and the run time can be inherited from the host language. +Unfortunately, data types defined in the host language are not automatically available in the \gls{EDSL}. + +The two main strategies for embedding \glspl{DSL} in a functional language are deep embedding (also called initial) and shallow embedding (also called final). +Deep embedding represents the constructs in the language as data types and the semantics as functions over these data types. +This makes extending the language with new semantics effortless: just add another function. +In contrast, adding language constructs requires changing the data type and updating all existing semantics to support this new construct. +Shallow embedding on the other hand models the language constructs as functions with the semantics embedded. +Consequently, adding a construct is easy, i.e.\ it only entails adding another function. +Contrarily, adding semantics requires adapting all language constructs. +Lifting the functions to type classes, i.e.\ parametrising the constructs over the semantics, allows extension of the language both in constructs and in semantics orthogonally. This advanced style of embedding is called tagless-final or class-based shallow embedding~\cite{kiselyov_typed_2012}. + +While it is often possible to lift values of a user-defined data type to a value in the \gls{DSL}, it is not possible to interact with it using \gls{DSL} constructs, they are not first-class citizens. + +Concretely, it is not possible to +\begin{enumerate*} + \item construct values from expressions using a constructor, + \item deconstruct values into expressions using a deconstructor or pattern matching, + \item test which constructor the value holds. +\end{enumerate*} +The functions for this are simply not available automatically in the embedded language. +For some semantics---such as an interpreter---it is possible to directly lift the functions from the host language to the \gls{DSL}. +In other cases---e.g.\ \emph{compiling} \glspl{DSL} such as a compiler or a printer---this is not possible~\cite{elliott_compiling_2003}. %the torget this is not possible. cannot just be lifted from the host language to the \gls{DSL} so it requires a lot of boilerplate to define and implement them. +Thus, all of the operations on the data type have to be defined by hand requiring a lot of plumbing and resulting in a lot of boilerplate code. + +To relieve the burden of adding all these functions, metaprogramming\nobreak---\nobreak\hskip0pt and custom quasiquoters---can be used. +Metaprogramming entails that some parts of the program are generated by a program itself, i.e.\ the program is data. +Quasiquotation is a metaprogramming mechanism that allows entering verbatim code for which a---possibly user defined---translation is used to convert the verbatim code to host language AST nodes. +Metaprogramming allows functions to be added to the program at compile time based on the structure of user-defined data types. + +\subsection{Contributions of the paper} +This paper shows that with the use of metaprogramming, all first-order user-defined data types can automatically be made first class for shallow \glspl{EDSL}. +It does so by providing an implementation in \gls{TH} for a typical \gls{DSL} with two different semantics: an interpreter and a pretty printer. +Furthermore, we show that by utilising quasiquotation, there is hardly any burden on the syntax. +Finally, the paper also serves as a gentle introduction to \gls{TH} and reflects on the process of using \gls{TH}. + +\section{Tagless-final embedding} +Tagless-final embedding is an upgrade to standard shallow embedding achieved by lifting all language construct functions to type classes. +As a result, views on the \gls{DSL} are data types implementing these classes. + +To illustrate the technique, a simple \gls{DSL}, a language consisting of literals and addition, is outlined. +This language, implemented according to the tagless-final style~\cite{carette_finally_2009} in \gls{HASKELL}~\cite{peyton_jones_haskell_2003} consists initially only of one type class containing two functions. +The \haskellinline{lit} function lifts values from the host language to the \gls{DSL} domain. +The class constraint \haskellinline{Show} is enforced on the type variable \haskellinline{a} to make sure that the value can be printed. +The infix function \haskellinline{+.} represents the addition of two expressions in the \gls{DSL}. + +\begin{lstHaskell} +class Expr v where + lit :: Show a => a -> v a + (+.) :: Num a => v a -> v a -> v a +infixl 6 +. +\end{lstHaskell} + +The implementation of a view on the \gls{DSL} is achieved by implementing the type classes with the data type representing the view. +In the case of our example \gls{DSL}, an interpreter accounting for failure may be implemented as an instance for the \haskellinline{Maybe} type. +The standard infix functor application and infix sequential application are used so that potential failure is abstracted away from\footnotemark{}. +\begin{lrbox}{\LstBox} + \begin{lstHaskell}[frame=] +<$> :: (a -> b) -> f a -> f b +<*> :: f (a -> b) -> f a -> f b +infixl 4 <$>, <*> + \end{lstHaskell} +\end{lrbox} +\footnotetext{\usebox{\LstBox}} + +\begin{lstHaskell} +instance Expr Maybe where + lit a = Just a + (+.) l r = (+) <$> l <*> r +\end{lstHaskell} + +\subsection{Adding language constructs} +To add an extra language construct we define a new class housing it. +For example, to add division we define a new class as follows: + +\begin{lstHaskell} +class Div v where + (/.) :: Integral a => v a -> v a -> v a +infixl 7 /. +\end{lstHaskell} + +Division is an operation that undefined if the right operand is equal to zero. +To capture this behaviour, the \haskellinline{Nothing} constructor from \haskellinline{Maybe} is used to represent errors. +The right-hand side of the division operator is evaluated first. +If the right-hand side is zero, the division is not performed and an error is returned instead: + +\begin{lstHaskell} +instance Div Maybe where + (/.) l r = l >>= \x->r >>= \y-> + if y == 0 then Nothing else Just (x `div` y) +\end{lstHaskell} + +\subsection{Adding semantics} +To add semantics to the \gls{DSL}, the existing classes are implemented with a novel data type representing the view on the \gls{DSL}. +First a data type representing the semantics is defined. In this case, the printer is kept very simple for brevity and just defined as a \haskellinline{newtype} of a string to store the printed representation\footnotemark{}. +\footnotetext{% + In this case a \haskellinline{newtype} is used instead of regular \haskellinline{data} declarations. + \haskellinline{newtype}s are special data types only consisting a single constructor with one field to which the type is isomorphic. + During compilation the constructor is completely removed resulting in no overhead~\cite[Sec.~4.2.3]{peyton_jones_haskell_2003}. +} +Since the language is typed, the printer data type has to have a type variable but it is only used during typing---i.e.\ a phantom type~\cite{leijen_domain_2000}: + +\begin{lstHaskell} +newtype Printer a = P { runPrinter :: String } +\end{lstHaskell} + +The class instances for \haskellinline{Expr} and \haskellinline{Div} for the pretty printer are straightforward and as follows: + +\begin{lstHaskell} +instance Expr Printer where + lit a = P (show a) + (+.) l r = P ("(" ++ runPrinter l + ++ "+" ++ runPrinter r ++ ")") + +instance Div Printer where + (/.) l r = P ("(" ++ runPrinter l + ++ "/" ++ runPrinter r ++ ")") +\end{lstHaskell} + +\subsection{Functions} +Adding functions to the language is achieved by adding a multi-parameter class to the \gls{DSL}. +The type of the class function allows for the implementation to only allow first order function by supplying the arguments in a tuple. +Furthermore, by defining the \haskellinline{Main} type, the \gls{DSL} forces all functions to be defined at the top level and with the \haskellinline{:-} operator the syntax becomes usable. +Finally, by defining the functions as a higher order abstract syntax (HOAS) type safety is achieved~\cite{pfenning_higher-order_1988,chlipala_parametric_2008}. +The complete definition looks as follows: + +\begin{lstHaskell} +class Function a v where + fun :: ( (a -> v s) -> In (a -> v s) (Main (v u)) ) -> Main (v u) +newtype Main a = Main { unmain :: a } +data In a b = a :- b +infix 1 :- +\end{lstHaskell} + +Using the \haskellinline{Function} type class can be used to define functions with little syntactic overhead\footnote{The \GHCmod{LambdaCase} extension of GHC is used to reduce the number of brackets that allows lambda's to be an argument to a function without brackets or explicit function application using \haskellinline{\$}}. +The following listing shows an expression in the \gls{DSL} utilising two user-defined functions: + +\begin{lstHaskell} + fun \increment-> (\x ->x +. lit 1) +:- fun \divide-> (\(x, y)->x /. y ) +:- Main (increment (divide (lit 38, lit 5))) +\end{lstHaskell} + +The interpreter only requires one instance of the \haskellinline{Function} class that works for any argument type. +In the implementation, the resulting function \haskellinline{g} is simultaneously provided to the definition \haskellinline{def}. +Because the laziness of \gls{HASKELL}'s lazy let bindings, this results in a fixed point calculation: + +\begin{lstHaskell} +instance Function a Maybe where + fun def = Main (let g :- m = def g in unmain m) +\end{lstHaskell} + +The given \haskellinline{Printer} type is not sufficient to implement the instances for the \haskellinline{Function} class, it must be possible to generate fresh function names. +After extending the \haskellinline{Printer} type to contain some sort of state to generate fresh function names and a \haskellinline{MonadWriter [String]}\footnotemark{} to streamline the output, we define an instance for every arity. +\begin{lrbox}{\LstBox} + \begin{lstHaskell}[frame=] +freshLabel :: Printer String +tell :: MonadWriter w m => w -> m () + \end{lstHaskell} +\end{lrbox} +\footnotetext{\usebox{\LstBox}} +To illustrate this, the instance for unary functions is shown, all other arities are implemented in similar fashion. + +\begin{lstHaskell} +instance Function () Printer where ... +instance Function (Printer a) Printer where ... + fun def = Main $ freshLabel >>= \f-> + let g :- m = def $ \a0->const undefined + <$> (tell ["f", show f, " ("] + >> a0 >> tell [")"]) + in tell ["let f", f, " a0 = "] + >> g (const undefined <$> tell ["a0"]) + >> tell [" in "] >> unmain m +instance Function (Printer a, Printer b) Printer where ... +\end{lstHaskell} + +Running the given printer on the example code shown before produces roughly the following output, running the interpreter on this code results in \haskellinline{Just 8}. + +\begin{lstHaskell} + let f0 a1 = a1 + 1 +in let f2 a3 a4 = a3 / a4 +in f0 (f2 38 5) +\end{lstHaskell} + +\subsection{Data types} +Lifting values from the host language to the \gls{DSL} is possible using the \haskellinline{lit} function as long as type of the value has instances for all the class constraints. +Unfortunately, once lifted, it is not possible to do anything with values of the user-defined data type other than passing them around. +It is not possible to construct new values from expressions in the \gls{DSL}, to deconstruct a value into the fields, nor to test of which constructor the value is. +Furthermore, while in the our language the only constraint is the automatically derivable \haskellinline{Show}, in real-world languages the class constraints may be very difficult to satisfy for complex types, for example serialisation to a single stack cell in the case of a compiler. + +As a consequence, for user-defined data types---such as a pro\-gram\-mer-defined list type\footnotemark{}---to become first-class citizens in the \gls{DSL}, language constructs for constructors, deconstructors and constructor predicates must be defined. +Field selectors are also useful functions for working with user-defined data types, they are not considered for the sake of brevity but can be implemented using the deconstructor functions. +\footnotetext{ + For example: \haskellinline{data List a = Nil \| Cons \{hd :: a, tl :: List a\}} +} +The constructs for the list type would result in the following class definition: + +\begin{lstHaskell} +class ListDSL v where + -- constructors + nil :: v (List a) + cons :: v a -> v (List a) -> v (List a) + -- deconstructors + unNil :: v (List a) -> v b -> v b + unCons :: v (List a) + -> (v a -> v (List a) -> v b) -> v b + -- constructor predicates + isNil :: v (List a) -> v Bool + isCons :: v (List a) -> v Bool +\end{lstHaskell} + +Furthermore, instances for the \gls{DSL}'s views need to be created. +For example, to use the interpreter, the following instance must be available. +Note that at first glance, it would feel natural to have \haskellinline{isNil} and \haskellinline{isCons} return \haskellinline{Nothing} since we are in the \haskellinline{Maybe} monad. +However, the this would fail the entire expression and the idea is that the constructor test can be done from within the \gls{DSL}. + +\begin{lstHaskell} +instance ListDSL Maybe where + nil = Just Nil + cons hd tl = Cons <$> hd <*> tl + unNil d f = d >>= \Nil->f + unCons d f = d + >>= \(Cons hd tl)->f (Just hd) (Just tl) + isNil d = d >>= \case[+\footnotemark+] + Nil -> Just True + _ -> Just False + isCons d = d >>= \case + Cons _ _ -> Just True + Nil -> Just False +\end{lstHaskell} +\footnotetext{% + \haskellinline{\\case} is an abbreviation for \haskellinline{\\x->case x of ...} when using GHC's \GHCmod{LambdaCase} extension. +} + +Adding these classes and their corresponding instances is tedious and results in boilerplate code. +We therefore resort to metaprogramming, and in particular \gls{TH}~\cite{sheard_template_2002} to alleviate this burden. + +\section{Template metaprogramming} +Metaprogramming is a special flavour of programming where programs have the ability to treat and manipulate programs or program fragments as data. +There are several techniques to facilitate metaprogramming, moreover it has been around for many years now~\cite{lilis_survey_2019}. +Even though it has been around for many years, it is considered complex~\cite{sheard_accomplishments_2001}. + +\gls{TH} is GHC's de facto metaprogramming system, implemented as a compiler extension together with a library~\cite{sheard_template_2002}\cite[Sec.~6.13.1]{ghc_team_ghc_2021}. +Readers already familiar with \gls{TH} can safely skip this section. + +\gls{TH} adds four main concepts to the language, na\-me\-ly AST data types, splicing, quasiquotation and reification. +With this machinery, regular \gls{HASKELL} functions can be defined that are called at compile time, inserting generated code into the {AST}. +These functions are monadic functions operating in the \haskellinline{Q} monad. +The \haskellinline{Q} monad facilitates failure, reification and fresh identifier generation for hygienic macros~\cite{kohlbecker_hygienic_1986}. +Within the \haskellinline{Q} monad, capturable and non-capturable identifiers can be generated using the \haskellinline{mkName} and \haskellinline{newName} functions respectively. +The \emph{Peter Parker principle}\footnote{With great power comes great responsibility.} holds for the \haskellinline{Q} monad as well because it executes at compile time and is very powerful. +For example it can subvert module boundaries, thus accessing constructors that were hidden; access the structure of abstract types; and it may cause side effects during compilation because it is possible to call \haskellinline{IO} operations~\cite{terei_safe_2012}. +To achieve the goal of embedding data types in a \gls{DSL} we refrain from using these \emph{unsafe} features. + +\subsubsection{Data types} +Firstly, for all of \gls{HASKELL}'s AST elements, data types are provided that are mostly isomorphic to the actual data types used in the compiler. +With these data types, the entire syntax of a \gls{HASKELL} program can be specified. +Often, a data type is suffixed with the context, e.g.\ there is a \haskellinline{VarE} and a \haskellinline{VarP} for a variable in an expression or in a pattern respectively. +To give an impression of these data types, a selection of data types available in \gls{TH} is given below: + +\begin{lstHaskell} +data Dec = FunD Name [Clause] | DataD Cxt Name ... + | SigD Name Type | ClassD Cxt Name | ... +data Clause = Clause [Pat] Body [Dec] +data Pat = LitP Lit | VarP Name | TupP [Pat] + | WildP | ListP [Pat] | ... +data Body = GuardedB [(Guard, Exp)] | NormalB Exp +data Guard = NormalG Exp | PatG [Stmt] +data Exp = VarE Name | LitE Lit | AppE Exp Exp + | TupE [Maybe Exp] | LamE [Pat] Exp | ... +data Lit = CharL Char | StringL String + | IntegerL Integer | ... +\end{lstHaskell} + +To ease creating AST data types in the \haskellinline{Q} monad, lowercase variants of the constructors are available that lift the constructor to the \haskellinline{Q} monad as. +For example, for the \haskellinline{LamE} constructor, the following \haskellinline{lamE} function is available. + +\begin{lstHaskell} +lamE :: [Q Pat] -> Q Exp -> Q Exp +lamE ps es = LamE <$> sequence ps <*> es +\end{lstHaskell} + +\subsubsection{Splicing} +Special splicing syntax (\haskellinline{\$(...)}) marks functions for compile-time execution. +Other than that they always produce a value of an AST data type, they are regular functions. +Depending on the context and location of the splice, the result type is either a list of declarations, a type, an expression or a pattern. +The result of this function, when successful, is then spliced into the code and treated as regular code by the compiler. +Consequently, the code that is generated may not be type safe, in which case the compiler provides a type error on the generated code. +The following listing shows an example of a \gls{TH} function generating on-the-fly functions for arbitrary field selection in a tuple. +When called as \haskellinline{\$(tsel 2 4)} it expands at compile time to \haskellinline{\\(_, _, f, _)->f}: + +\begin{lstHaskell} +tsel :: Int -> Int -> Q Exp +tsel field total = do + f <- newName "f" + lamE [ tupP [if i == field then varP f else wildP + | i<-[0..total-1]]] (varE f) +\end{lstHaskell} + +\subsubsection{Quasiquotation} +Another key concept of \gls{TH} is Quasiquotation, the dual of splicing~\cite{bawden_quasiquotation_1999}. +While it is possible to construct entire programs using the provided data types, it is a little cumbersome. +Using \emph{Oxford brackets} or single or double apostrophes, verbatim \gls{HASKELL} code can be entered that is converted automatically to the corresponding AST nodes easing the creation of language constructs. +Depending on the context, different quasiquotes are used: +\begin{itemize*} + \item \haskellinline{[|...|]} or \haskellinline{[e|...|]} for expressions + \item \haskellinline{[d|...|]} for declarations + \item \haskellinline{[p|...|]} for patterns + \item \haskellinline{[t|...|]} for types + \item \haskellinline{'...} for function names + \item \haskellinline{''...} for type names +\end{itemize*}. +It is possible to escape the quasiquotes again by splicing. +Variables defined within quasiquotes are always fresh---as if defined with \haskellinline{newName}---but it is possible to capture identifiers using \haskellinline{mkName}. +For example, \haskellinline{[|\\x->x|]} translates to \haskellinline{newName "x" >>= \\x->lamE [varP x] (varE x)} and does not interfere with other \haskellinline{x}s already defined. + +\subsubsection{Reification} +Reification is the act of querying the compiler for information about a certain name. +For example, reifying a type name results in information about the type and the corresponding AST nodes of the type's definition. +This information can then be used to generate code according to the structure of data types. +Reification is done using the \haskellinline{reify :: Name -> Q Info} function. +The \haskellinline{Info} type is an \gls{ADT} containing all the---known to the compiler---information about the matching type: constructors, instances, etc. + +\section{Metaprogramming for generating \gls{DSL} functions} +With the power of metaprogramming, we can generate the boilerplate code for our user-defined data types automatically at compile time. +To generate the code required for the \gls{DSL}, we define the \haskellinline{genDSL} function. +The type belonging to the name passed as an argument to this function is made available for the \gls{DSL} by generating the \haskellinline{typeDSL} class and view instances. +For the \haskellinline{List} type it is called as: \haskellinline{\$(genDSL ''List)}\footnotemark{}. +\footnotetext{ + \haskellinline{''} is used instead of \haskellinline{'} to instruct the compiler to look up the information for \haskellinline{List} as a type and not as a constructor. +} + +The \haskellinline{genDSL} function is a regular function---though \gls{TH} requires that it is defined in a separate module---that has type: \haskellinline{Name -> Q [Dec]}, i.e.\ given a name, it produces a list of declarations in the \haskellinline{Q} monad. +The \haskellinline{genDSL} function first reifies the name to retrieve the structural information. +If the name matches a type constructor containing a data type declaration, the structure of the type---the type variables, the type name and information about the constructors\footnotemark{}---are passed to the \haskellinline{genDSL'} function. +\footnotetext{ + Defined as \haskellinline{type VarBangType = (Name, Bang, Type)} by \gls{TH}. +} +The \haskellinline{getConsName} function filters out unsupported data types such as \glspl{GADT} and makes sure that every field has a name. +For regular \glspl{ADT}, the \haskellinline{adtFieldName} function is used to generate a name for the constructor based on the indices of the fields\footnotemark{}. +\footnotetext{ + \haskellinline{adtFieldName :: Name -> Integer -> Name} +} +From this structure of the type, \haskellinline{genDSL'} generates a list of declarations containing a class definition (\cref{sec_fcd:class}), instances for the interpreter (\cref{sec_fcd:interpreter}), and instances of the printer (\cref{sec_fcd:prettyprinter}) respectively. + +\begin{lstHaskell} +genDSL :: Name -> Q [Dec] +genDSL name = reify name >>= \case + TyConI (DataD cxt typeName tvs mkind + constructors derives) + -> mapM getConsName constructors + >>= \d->genDSL' tvs typeName d + t -> fail ("genDSL does not support: " ++ show t) + +getConsName :: Con -> Q (Name, [VarBangType]) +getConsName (NormalC consName fs) = pure (consName, + [(adtFieldName consName i, b, t) + | (i, (b, t))<-[0..] `zip` fs]) +getConsName (RecC consName fs) = pure (consName, fs) +getConsName c + = fail ("genDSL does not support: " ++ show c) + +genDSL' :: [TyVarBndr] -> Name -> [(Name, [VarBangType])] + -> Q [Dec] +genDSL' typeVars typeName constructors = sequence + [ mkClass, mkInterpreter, mkPrinter, ... ] + where + (consNames, fields) = unzip constructors + ... +\end{lstHaskell} + +\subsection{Class generation}\label{sec_fcd:class} +The function for generating the class definition is defined in the \haskellinline{where} clause of the \haskellinline{genDSL'} function. +Using the \haskellinline{classD} constructor, a single type class is created with a single type variable \haskellinline{v}. +The \haskellinline{classD} function takes five arguments: +\begin{enumerate*} + \item a context, i.e.\ the class constraints, which is empty in this case + \item a name, generated from the type name using the \haskellinline{className} function that simply appends the text \haskellinline{DSL} + \item a list of type variables, in this case the only type variable is the view on the \gls{DSL}, i.e.\ \haskellinline{v} + \item functional dependencies, empty in our case + \item a list of function declarations, i.e.\ the class members, in this case it is a concatenation of the constructors, deconstructors, and constructor predicates +\end{enumerate*} +Depending on the required information, either \haskellinline{zipWith} or \haskellinline{map} is used to apply the generation function to all constructors. + +\begin{lstHaskell} +mkClass :: Q Dec +mkClass = classD (cxt []) (className typeName) [PlainTV (mkName "v")] [] + ( zipWith mkConstructor consNames fields + ++ zipWith mkDeconstructor consNames fields + ++ map mkPredicate consNames + ) +\end{lstHaskell} + +In all class members, the view \haskellinline{v} plays a crucial role. +Therefore, a definition for \haskellinline{v} is accessible for all generation functions. +Furthermore, the \haskellinline{res} type represents the \emph{result} type, it is defined as the type including all type variables. +This result type is derived from the type name and the list of type variables. +In case of the \haskellinline{List} type, \haskellinline{res} is defined as \haskellinline{v (List a)} and is available for as well: + +\begin{lstHaskell} +v = varT (mkName "v") +res = v `appT` foldl appT (conT typeName) + (map getName typeVars) + where getName (PlainTV name) = varT name + getName (KindedTV name _) = varT name +\end{lstHaskell} + +\subsubsection{Constructors} +The constructor definitions are generated from just the constructor names and the field information. +All class members are defined using the \haskellinline{sigD} constructor that represents a function signature. +The first argument is the name of the constructor function, a lowercase variant of the actual constructor name generated using the \haskellinline{constructorName} function. +The second argument is the type of the function. +A constructor $C_k$ of type $T$ where +$T~tv_0~\ldots~tv_n = \ldots |~ C_k~a_0~\ldots~a_m~| \ldots~$ +is defined as a \gls{DSL} function +$c_k \dcolon v~a_0 \shortrightarrow \ldots \shortrightarrow v~a_m \shortrightarrow v~(T~v_0~\ldots~v_n) $. +In the implementation, first the view \haskellinline{v} is applied to all the field types. +Then, the constructor type is constructed by folding over the lifted field types with the result type as the initial value using \haskellinline{mkCFun}. + +\begin{lstHaskell} +mkConstructor :: Name -> [VarBangType] -> Q Dec +mkConstructor n fs + = sigD (constructorName n) (mkCFun fs res) + +mkCFun :: [VarBangType] -> Q Type -> Q Type +mkCFun fs res = foldr (\x y->[t|$x -> $y|]) + (map (\(_, _, t)->v `appT` pure t) fs) +\end{lstHaskell} + +\subsubsection{Deconstructors} +The deconstructor is generated similarly to the constructor as the function for generating the constructor is the second argument modulo change in the result type. +A deconstructor $C_k$ of type $T$ is defined as a \gls{DSL} function +$\mathit{unC_k} \dcolon v~(T~v_0 \ldots v_n) \shortrightarrow (v~a_0 \shortrightarrow \ldots \shortrightarrow v~a_m \shortrightarrow v~b) \shortrightarrow v~b $. +In the implementation, \haskellinline{mkCFun} is reused to construct the type of the deconstructor as follows: + +\begin{lstHaskell} +mkDeconstructor :: Name -> [VarBangType] -> Q Dec +mkDeconstructor n fs = sigD (deconstructorName n) + [t|$res -> $(mkCFun fs [t|$v $b|]) -> $v $b|] + where b = varT (mkName "b") +\end{lstHaskell} + +\subsubsection{Constructor predicates} +The last part of the class definition are the constructor predicates, a function that checks whether the provided value of type $T$ contains a value with constructor $C_k$. +A constructor predicate for constructor $C_k$ of type $T$ is defined as a \gls{DSL} function $\mathit{isC_k} \dcolon v~(T~v_0~\ldots~v_n) \shortrightarrow v~\mathit{Bool}$. +A constructor predicate---name prefixed by \haskellinline{is}---is generated for all constructors. +They all have the same type: + +\begin{lstHaskell} +mkPredicate :: Name -> Q Dec +mkPredicate n = sigD (predicateName n) + [t|$res -> $v Bool|] +\end{lstHaskell} + +\subsection{Interpreter instance generation}\label{sec_fcd:interpreter} +Generating the interpreter for the \gls{DSL} means generating the class instance for the \haskellinline{Interpreter} data type using the \haskellinline{instanceD} function. +The first argument of the instance is the context, this is left empty. +The second argument of the instance is the type, the \haskellinline{Interpreter} data type applied to the class name. +Finally, the class function instances are generated using the information derived from the structure of the type. +The structure for generating the function instances is very similar to the class definition, only for the function instances of the constructor predicates, the field information is required as well as the constructor names. + +\begin{lstHaskell} +mkInterpreter :: Q Dec +mkInterpreter = instanceD (cxt []) + [t|$(conT (className typeName)) Interpreter|] + ( zipWith mkConstructor consNames fields + ++ zipWith mkDeconstructor consNames fields + ++ zipWith mkPredicate consNames fields) + where ... +\end{lstHaskell} + +\subsubsection{Constructors} +The interpreter is a view on the \gls{DSL} that immediately executes all operations in the \haskellinline{Maybe} monad. +Therefore, the constructor function can be implemented by lifting the actual constructor to the \haskellinline{Maybe} type using sequential application. +I.e.\ for a constructor $C_k$ this results in the following constructor: \haskellinline{ck a0 ... am = pure Ck <*> a0 <*> ... <*> am}. +To avoid accidental shadowing, fresh names for all the arguments are generated. +The \haskellinline{ifx} function is used as a shorthand for defining infix expressions\footnotemark{} +\begin{lrbox}{\LstBox} + \begin{lstHaskell}[frame=] +ifx :: String -> Q Exp -> Q Exp -> Q Exp +ifx op a b = infixE (Just a) (varE (mkName op)) (Just b) + \end{lstHaskell} +\end{lrbox} +\footnotetext{\usebox{\LstBox}} + +\begin{lstHaskell} +mkConstructor :: Name -> [VarBangType] -> Q Dec +mkConstructor consName fs = do + fresh <- sequence [newName "a" | _<-fs] + fun (constructorName consName) (map varP fresh) + (foldl (ifx "<*>") [|pure $(conE consName)|] + (map varE fresh)) +\end{lstHaskell} + + +\subsubsection{Deconstructors} +In the case of a deconstructor a function with two arguments is created: the object itself (\haskellinline{f}) and the function doing something with the individual fields (\haskellinline{d}). +To avoid accidental shadowing first fresh names for the arguments and fields are generated. +Then, a function is created with the two arguments. +First \haskellinline{d} is evaluated and bound to a host language function that deconstructs the constructor and passes the fields to \haskellinline{f}. +I.e.\ a deconstructor function $C_k$ is defined as: \haskellinline{unCk d f = d >>= \\(Ck a0 .. am)->f (pure a0) ... (pure am))}\footnotemark{}. +\footnotetext{ + The \haskellinline{nameBase :: Name -> String} function from the \gls{TH} library is used to convert a name to a string. +} + +\begin{lstHaskell} +mkDeconstructor :: Name -> [VarBangType] -> Q Dec +mkDeconstructor consName fs = do + d <- newName "d" + f <- newName "f" + fresh <- mapM (newName . nameBase . fst3) fs + fun (deconstructorName consName) [varP d, varP f] + [|$(varE d) >>= \($(match f))->$(fapp f fresh)|] + where fapp f = foldl appE (varE f) + . map (\f->[|pure $(varE f)|]) + match f = pure (ConP consName (map VarP f)) +\end{lstHaskell} + +\subsubsection{Constructor predicates} +Constructor predicates evaluate the argument and make a case distinction on the result to determine the constructor. +To be able to generate a valid pattern in the case distinction, the total number of fields must be known. +To avoid having to explicitly generate a fresh name for the first argument, a lambda function is used. +In general, the constructor selector for $C_k$ results in the following code \haskellinline{isCk f = f >>= \\case Ck _ ... _ -> pure True; _ -> pure False}. +Generating this code is done with the following function: + +\begin{lstHaskell} +mkPredicate :: Name -> [(Var, Bang, Type)] -> Q Dec +mkPredicate n fs = fun (predicateName n) [] + [|\x->x >>= \case + $(conP n [wildP | _<-fs]) -> pure True + _ -> pure False|] +\end{lstHaskell} + +\subsection{Pretty printer instance generation}\label{sec_fcd:prettyprinter} +Generating the printer happen analogously to the interpreter, a class instance for the \haskellinline{Printer} data type using the \haskellinline{instanceD} function. + +\begin{lstHaskell} +mkPrinter :: Q Dec +mkPrinter = instanceD (cxt []) [t|$(conT (className typeName)) Printer|] + ( zipWith mkConstructor consNames fields + ++ zipWith mkDeconstructor consNames fields + ++ map mkPredicate consNames) +\end{lstHaskell} + +To be able to define a printer that is somewhat more powerful, we provide instances for \haskellinline{MonadWriter}; add a state for fresh variables and a context; and define some helper functions the \haskellinline{Printer} datatype. +The \haskellinline{printLit} function is a variant of \haskellinline{MonadWriter}s \haskellinline{tell} that prints a literal string but it can be of any type (it is a phantom type anyway). +\haskellinline{printCons} prints a constructor name followed by an expression, it inserts parenthesis only when required depending on the state. +\haskellinline{paren} always prints parenthesis around the given printer. +\haskellinline{>->} is a variant of the sequence operator \haskellinline{>>} from the \haskellinline{Monad} class, it prints whitespace in between the arguments. + +\begin{lstHaskell} +printLit :: String -> Printer a +printCons :: String -> Printer a -> Printer a +paren :: Printer a -> Printer a +(>->) :: Printer a1 -> Printer a2 -> Printer a3 +pl :: String -> Q Exp +\end{lstHaskell} + +\subsubsection{Constructors} +For a constructor $C_k$ the printer is defined as: \haskellinline{ck a0 ... am = printCons "Ck" (printLit "" >-> a0 >-> ... >-> am)}. +To generate the second argument to the \haskellinline{printCons} function, a fold is used with \haskellinline{printLit ""} as the initial element to account for constructors without any fields as well, e.g.\ \haskellinline{Nil} is translated to \haskellinline{nil = printCons "Nil" (printLit "")}. + +\begin{lstHaskell} +mkConstructor :: Name -> [VarBangType] -> Q Dec +mkConstructor consName fs = do + fresh <- sequence [newName "f" | _<- fs] + fun (constructorName consName) (map varP fresh) + (pcons `appE` pargs fresh) + where pcons = [|printCons $(lift (nameBase consName))|] + pargs fresh = foldl (ifx ">->") (pl "") + (map varE fresh) +\end{lstHaskell} + +\subsubsection{Deconstructors} +Printing the deconstructor for $C_k$ is defined as: +\begin{lstHaskell} +unCk d f + = printLit "unCk d" + >-> paren ( + printLit "\(Ck" >-> printLit "a0 ... am" >> printLit ")->" + >> f (printLit "a0") ... (printLit "am") + ) +\end{lstHaskell} + +The implementation for this is a little elaborate and it heavily uses the \haskellinline{pl} function, a helper function that translates a string literal \haskellinline{s} to \haskellinline{[|printLit \$(lift s)|]}, i.e.\ it lifts the \haskellinline{printLit} function to the \gls{TH} domain. + +\begin{lstHaskell} +mkDeconstructor :: Name -> [VarBangType] -> Q Dec +mkDeconstructor consName fs = do + d <- newName "d" + f <- newName "f" + fresh <- sequence [newName "a" | _<-fs] + fun (deconstructorName consName) (map varP [d, f]) + [| $(pl (nameBase (deconstructorName consName))) + >-> $(pl (nameBase d)) + >-> paren ($(pl ('\\':'(':nameBase consName)) + >-> $lam >> printLit ")->" + >> $(hoas f))|] + where + lam = pl $ unwords [nameBase f | (f, _, _)<-fs] + hoas f = foldl appE (varE f) + [pl (nameBase f) | (f, _, _)<-fs] +\end{lstHaskell} + +\subsubsection{Constructor predicates} +For the printer, the constructor selector for $C_k$ results in the following code \haskellinline{isCk f = printLit "isCk" >-> f}. + +\begin{lstHaskell} +mkPredicate :: Name -> Q Dec +mkPredicate n = fun (predicateName n) [] + [|\x-> $(pl $ nameBase $ predicateName n) >-> x|] +\end{lstHaskell} + +\section{Pattern matching} +It is possible to construct and deconstruct values from other \gls{DSL} expressions, and to perform tests on the constructor but with a clunky and unwieldy syntax. +They have become first-class citizens in a grotesque way. +For example, given that we have some language constructs to denote failure and conditionals\footnotemark{}, writing a list summation function in our \gls{DSL} would be done as follows. +For the sake of the argument we take a little shortcut here and assume that the interpretation of the \gls{DSL} supports lazy evaluation by using the host language as a metaprogramming language as well, allowing us to use functions in the host language to contstruct expressions in the \gls{DSL}. + +\begin{lrbox}{\LstBox} + \begin{lstHaskell}[frame=] +class Support v where + if' :: v Bool -> v a -> v a -> v a + bottom :: String -> v a + \end{lstHaskell} +\end{lrbox} +\footnotetext{\usebox{\LstBox}} + +\begin{lstHaskell} +program :: (ListDSL v, Support v, ...) => Main (v Int) +program + = fun \sum->(\l->if'(isNil l) + (lit 0) + (unCons l (\hd tl->hd +. sum tl))) + :- Main (sum (cons (lit 38) (cons (lit 4) nil))) +\end{lstHaskell} + +A similar \gls{HASKELL} implementation is much more elegant and less cluttered because of the support for pattern matching. +Pattern matching offers a convenient syntax for doing deconstruction and constructor tests at the same time. + +\begin{lstHaskell} +sum :: List Int -> Int +sum Nil = 0 +sum (List hd tl) = hd + sum tl + +main = sum (Cons 38 (Cons 4 Nil)) +\end{lstHaskell} + +\subsection{Custom quasiquoters} +The syntax burden of \glspl{EDSL} can be reduced using quasiquotation. +In \gls{TH}, quasiquotation is a convenient way to create \gls{HASKELL} language constructs by entering them verbatim using Oxford brackets. +However, it is also possible to create so-called custom quasiquoters~\cite{mainland_why_2007}. +If the programmer writes down a fragment of code between \emph{tagged} Oxford brackets, the compiler executes the associated quasiquoter functions at compile time. +A quasiquoter is a value of the following data type: + +\begin{lstHaskell} +data QuasiQuoter = QuasiQuoter + { quoteExp :: String -> Q Exp + , quotePat :: String -> Q Pat + , quoteType :: String -> Q Type + , quoteDec :: String -> Q Dec + } +\end{lstHaskell} + +The code between \emph{dsl} brackets (\haskellinline{[dsl|...|]}) is preprocessed by the \haskellinline{dsl} quasiquoter. +Because the functions are executed at compile time, errors---thrown using the \haskellinline{MonadFail} instance of the \haskellinline{Q} monad---in these functions result in compile time errors. +The AST nodes produced by the quasiquoter are inserted into the location and checked as if they were written by the programmer. + +To illustrate writing a custom quasiquoter, we show an implementation of a quasiquoter for binary literals. +The \haskellinline{bin} quasiquoter is only defined for expressions and parses subsequent zeros and ones as a binary number and splices it back in the code as a regular integer. +Thus, \haskellinline{[bin|101010|]} results in the literal integer expression \haskellinline{42}. +If an invalid character is used, a compile-time error is shown. +The quasiquoter is defined as follows: + +\begin{lstHaskell} +bin :: QuasiQuoter +bin = QuasiQuoter { quoteExp = parseBin } + where + parseBin :: String -> Q Exp + parseBin s = LitE . IntegerL <$> foldM bindigit 0 s + + bindigit :: Integer -> Char -> Q Integer + bindigit acc '0' = pure (2 * acc) + bindigit acc '1' = pure (2 * acc + 1) + bindigit acc c = fail ("invalid char: " ++ show c) +\end{lstHaskell} + +\subsection{Quasiquotation for pattern matching} +Custom quasiquoters allow the \gls{DSL} user to enter fragments verbatim, bypassing the syntax of the host language. +Pattern matching in general is not suitable for a custom quasiquoter because it does not really fit in one of the four syntactic categories for which custom quasiquoter support is available. +However, a concrete use of pattern matching, interesting enough to be beneficial, but simple enough for a demonstration is the \emph{simple case expression}, a case expression that does not contain nested patterns and is always exhaustive. +They correspond to a multi-way conditional expressions and can thus be converted to \gls{DSL} constructs straightforwardly~\cite[Chp.~4.4]{peyton_jones_implementation_1987}. + +In contrast to the binary literal quasiquoter example, we do not create the parser by hand. +The parser combinator library \emph{parsec} is used instead to ease the creation of the parser~\cite{leijen_parsec_2001}. +First the location of the quasiquoted code is retrieved using the \haskellinline{location} function that operates in the \haskellinline{Q} monad. +This location is inserted in the parsec parser so that errors are localised in the source code. +Then, the \haskellinline{expr} parser is called that returns an \haskellinline{Exp} in the \haskellinline{Q} monad. +The \haskellinline{expr} parser uses parsec's commodity expression parser primitive \haskellinline{buildExpressionParser}. +The resulting parser translates the string directly into \gls{TH}'s AST data types in the \haskellinline{Q} monad. +The most interesting parser is the parser for the case expression that is an alternative in the basic expression parser \haskellinline{basic}. +A case expression is parsed when a keyword \haskellinline{case} is followed by an expression that is in turn followed by a non-empty list of matches. +A match is parsed when a pattern (\haskellinline{pat}) is followed by an arrow and an expression. +The results of this parser are fed into the \haskellinline{mkCase} function that transforms the case into an expression using \gls{DSL} primitives such as conditionals, deconstructors and constructor predicates. +The above translates to the following skeleton implementation: + +\begin{lstHaskell} +expr :: Parser (Q Exp) +expr = buildExpressionParser [...] basic + where + basic :: Parser (Q Exp) + basic = ... + <|> mkCase <$ reserved "case" <*> expr + <* reserved "of" <*> many1 match + <|> ... + + match :: Parser (Q Pat, Q Exp) + match = (,) <$> pat <* reserved "->" <*> expr + + pat :: Parser (Q Pat) + pat = conP <$> con <*> many var +\end{lstHaskell} + +Case expressions are transformed into constructors, deconstructors and constructor predicates, e.g.\ \haskellinline{case e1 of Cons hd tl -> e2; Nil -> e3;} is converted to: +\begin{lstHaskell} +if' (isList e1) + (unCons e1 (\hd tl->e2)) + (if' (isNil e1) + (unNil e1 e3) + (bottom "Exhausted case")) +\end{lstHaskell} + +The \haskellinline{mkCase} (\cref{mkcase_fcd:mkcase}) function transforms a case expression into constructors, deconstructors and constructor predicates. +\Cref{mkcase_fcd:eval} first evaluates the patterns. +Then the patterns and their expressions are folded using the \haskellinline{mkCase`} function (\cref{mkcase_fcd:pairs}). +While a case exhaustion error is used as the initial value, this is never called since all case expressions are exhaustive. +For every case, code is generated that checks whether the constructor used in the pattern matches the constructor of the value using constructor predicates (\cref{mkcase_fcd:conspred}). +If the constructor matches, the deconstructor (\cref{mkcase_fcd:consdec}) is used to bind all names to the correct identifiers and evaluate the expression. +If the constructor does not match, the continuation (\haskellinline{\$rest}) is used (\cref{mkcase_fcd:consstart}). + +\begin{lstHaskell}[numbers=left] +mkCase :: Q Exp -> [(Q Pat, Q Exp)] -> Q Exp [+\label{mkcase_fcd:mkcase} +] +mkCase name cases = do + pats <- mapM fst cases [+ \label{mkcase_fcd:eval} +] + foldr (uncurry mkCase') [|bottom "Exhausted case"|][+ \label{mkcase_fcd:fold}\label{mkcase_fcd:foldinit} +] + (zip pats (map snd cases)) [+\label{mkcase_fcd:pairs}+] + where + mkCase' :: Pat -> Q Exp -> Q Exp -> Q Exp + mkCase' (ConP cons fs) e rest + = [|if' $pred $then_ $rest|] [+\label{mkcase_fcd:consstart}+] + where + pred = varE (predicateName cons) `appE` name[+\label{mkcase_fcd:conspred}+] + then_ = [|$(varE (deconstructorName cons))[+\label{mkcase_fcd:consdec}+] + $name $(lamE [pure f | f<-fs] e)|][+\label{mkcase_fcd:consend}+] +\end{lstHaskell} + +Finally, with this quasiquotation mechanism we can define our list summation using a case expression. +As a byproduct, syntactic cruft such as the special symbols for the operators and calls to \haskellinline{lit} can be removed as well resulting in the following summation implementation: + +\begin{lstHaskell} +program :: (ListDSL v, DSL v, ...) => Main (v Int) +program + = fun \sum->(\l->[dsl|case l of + Cons hd tl -> hd + sum tl + Nil -> 0|]) + :- Main (sum (cons (lit 38) (cons (lit 4) nil))) +\end{lstHaskell} + +\section{Related work} +Generic or polytypic programming is a promising technique at first glance for automating the generation of function implementations~\cite{lammel_scrap_2003}. +However, while it is possible to define a function that works on all first-order types, adding a new function with a new name to the language is not possible. +This does not mean that generic programming is not useable for embedding pattern matches. +In generic programming, types are represented as sums of products and using this representation it is possible to define pattern matching functions. + +For example, Rhiger showed a method for expressing statically typed pattern matching using typed higher-order functions~\cite{rhiger_type-safe_2009}. +If not the host language but the \gls{DSL} contains higher order functions, the same technique could be applied to port pattern matching to \glspl{DSL} though using an explicit sums of products representation. +Atkey et al.\ describe embedding pattern matching in a \gls{DSL} by giving patterns an explicit representation in the \gls{DSL} by using pairs, sums and injections~\cite[Section~3.3]{atkey_unembedding_2009}. + +McDonell et al.\ extends on this idea, resulting in a very similar but different solution to ours~\cite{mcdonell_embedded_2021}. +They used the technique that Atkey et al.\ showed and applied it to deep embedding using the concrete syntax of the host language. +The scaffolding---e.g.\ generating the pairs, sums and injections---for embedding is automated using generics but the required pattern synonyms are generated using \gls{TH}. +The key difference to our approach is that we specialise the implementation for each of the backends instead of providing a general implementation of data type handling operations. +Furthermore, our implementation does not require a generic function to trace all constructors, resulting in problems with (mutual) recursion. + +Young et al.\ added pattern matching to a deeply \gls{EDSL} using a compiler plugin~\cite{young_adding_2021}. +This plugin implements an \haskellinline{externalise :: a -> E a} function that allows lifting all machinery required for pattern matching automatically from the host language to the \gls{DSL}. +Under the hood, this function translates the pattern match to constructors, deconstructors, and constructor predicates. +The main difference with this work is that it requires a compiler plugin while our metaprogramming approach works on any compiler supporting a metaprogramming system similar to \gls{TH}. + +\subsection{Related work on \gls{TH}} +Metaprogramming in general is a very broad research topic and has been around for years already. +We therefore do not claim an exhaustive overview of related work on all aspects of metaprogramming. +However, we have have tried to present most research on metaprogramming in \gls{TH}. +Czarnecki et al.\ provide a more detailed comparison of different metaprogramming techniques. +They compare staged interpreters, metaprogramming and templating by comparing MetaOCaml, \gls{TH} and C++ templates~\cite{czarnecki_dsl_2004}. +\gls{TH} has been used to implement related work. +They all differ slightly in functionality from our domain and can be divided into several categories. + +\subsubsection{Generating extra code} +Using \gls{TH} or other metaprogramming systems it is possible to add extra code to your program. +The original \gls{TH} paper showed that it is possible to create variadic functions such as \haskellinline{printf} using \gls{TH} that would be almost impossible to define without~\cite{sheard_template_2002}. +Hammond et al.\ used \gls{TH} to generate parallel programming skeletons~\cite{hammond_automatic_2003}. +In practise, this means that the programmer selects a skeleton and, at compile time, the code is massaged to suit the pattern and information about the environment is inlined for optimisation. + +Polak et al.\ implemented automatic GUI generation using \gls{TH}~\cite{polak_automatic_2006}. +Dureg\aa{}rd et al.\ wrote a parser generator using \gls{TH} and the custom quasiquoting facilities~\cite{duregard_embedded_2011}. +From a specification of the grammar, given in verbatim using a custom quasiquoter, a parser is generated at compile time. +Shioda et al.\ used metaprogramming in the D programming language to create a \gls{DSL} toolkit~\cite{shioda_libdsl_2014}. +They also programmatically generate parsers and a backend for either compiling or interpreting the \gls{IR}. +Blanchette et al.\ use \gls{TH} to simplify the development of Liquid \gls{HASKELL} proofs~\cite{blanchette_liquid_2022}. +Folmer et al.\ used \gls{TH} to synthesize C$\lambda$aSH~\cite{baaij_digital_2015} abstract syntax trees to be processed~\cite{folmer_high-level_2022}. +In similar fashion, Materzok used \gls{TH} to translate YieldFSM programs to C$\lambda$aSH~\cite{materzok_generating_2022}. + +\subsubsection{Optimisation} +Besides generating code, it is also possible to analyse existing code and perform optimisations. +Yet, this is dangerous territory because unwantedly the semantics of the optimised program may be slightly different from the original program. +For example, Lynagh implemented various optimisations in \gls{TH} such as automatic loop unrolling~\cite{lynagh_unrolling_2003}. +The compile-time executed functions analyse the recursive function and unroll the recursion to a fixed depth to trade execution speed for program space. +Also, O'Donnell embedded Hydra, a hardware description language, in \gls{HASKELL} utilising \gls{TH}~\cite{odonnell_embedding_2004}. +Using intensional analysis of the AST, it detects cycles by labelling nodes automatically so that it can generate \emph{netlists}. +The authors mention that alternatively this could have be done using a monad but this hampers equational reasoning greatly, which is a key property of Hydra. +Finally, Viera et al.\ present a way of embedding attribute grammars in \gls{HASKELL} in a staged fashion~\cite{viera_staged_2018}. +Checking several aspects of the grammar is done at compile time using \gls{TH} while other safety checks are performed at runtime. + +\subsubsection{Compiler extension} +Sometimes, expressing certain functionalities in the host languages requires a lot of boilerplate, syntax wrestling, or other pains. +Metaprogramming can relieve some of this stress by performing this translation to core constructs automatically. +For example, implementing generic---or polytypic--- functions in the compiler is a major effort. +Norell et al.\ used \gls{TH} to implement the machinery required to implement generic functions at compile time~\cite{norell_prototyping_2004}. +Adams et al.\ also explores implementing generic programming using \gls{TH} to speed things up considerably compared to regular generic programming~\cite{adams_template_2012}. +Clifton et al.\ use \gls{TH} with a custom quasiquoter to offer skeletons for workflows and embed foreign function interfaces in a \gls{DSL}~\cite{clifton-everest_embedding_2014}. +Eisenberg et al.\ showed that it is possible to programmatically lift some functions from the function domain to the type domain at compile time, i.e.\ type families~\cite{eisenberg_promoting_2014}. +Furthermore, Seefried et al.\ argued that it is difficult to do some optimisations in \glspl{EDSL} and that metaprogramming can be of use there~\cite{seefried_optimising_2004}. +They use \gls{TH} to change all types to unboxed types, unroll loops to a certain depth and replace some expressions by equivalent more efficient ones. +Torrano et al.\ showed that it is possible to use \gls{TH} to perform a strictness analysis and perform let-to-case translation~\cite{torrano_strictness_2005}. +Both applications are examples of compiler extensions that can be implemented using \gls{TH}. +Another example of such a compiler extension is shown by Gill et al.~\cite{gill_haskell_2009}. +They created a meta level \gls{DSL} to describe rewrite rules on \gls{HASKELL} syntax that are applied on the source code at compile time. + +\subsubsection{Quasiquotation} +By means of quasiquotation, the host language syntax that usually seeps through the embedding can be hidden. +The original \gls{TH} quasiquotation paper~\cite{mainland_why_2007} shows how this can be done for regular expressions, not only resulting in a nicer syntax but syntax errors are also lifted to compile time instead of run time. +Also, Kariotis et al.\ used \gls{TH} to automatically construct monad stacks without having to resort to the monad transformers library which requires advanced type system extensions~\cite{kariotis_making_2008}. + +Najd uses the compile time to be able to do normalisation for a \gls{DSL}, dubbing it \glspl{QDSL}~\cite{najd_everything_2016}. +They utilise the quasiquation facilities of \gls{TH} to convert \gls{HASKELL} \gls{DSL} code to constructs in the \gls{DSL}, applying optimisations such as eliminating lambda abstractions and function applications along the way. +Egi et al.\ extended \gls{HASKELL} to support non-free data type pattern matching---i.e.\ data type with no standard form, e.g.\ sets, graphs---using \gls{TH}~\cite{egi_embedding_2022}. +Using quasiquotation, they make a complicated embedding of non-linear pattern matching available through a simple lens. + +\subsubsection{\gls{TTH}}\label{ssec_fcd:typed_template_haskell} +\gls{TTH} is a very recent extension/alternative to normal \gls{TH}~\cite{pickering_multi-stage_2019,xie_staging_2022}. +Where in \gls{TH} you can manipulate arbitrary parts of the syntax tree, add top-level splices of data types, definitions and functions, in \gls{TTH} the programmer can only splice expressions but the abstract syntax tree fragments representing the expressions are well-typed by construction instead of untyped. + +Pickering et al.\ implemented staged compilation for the \emph{generics-sop}~\cite{de_vries_true_2014} generics library to improve the efficiency of the code using \gls{TTH}~\cite{pickering_staged_2020}. +Willis et al.\ used \gls{TTH} to remove the overhead of parsing combinators~\cite{willis_staged_2020}. + +\section{Discussion} +Functional programming languages are especially suitable for embedding \glspl{DSL} but adding user-defined data types is still an issue. +The tagless-final style of embedding offers great modularity, extensibility and flexibility. +However, user-defined data types are awkward to handle because the built-in operations on them---construction, deconstruction and constructor tests---are not inherited from the host language. +By giving an implementation, we showed how to create a \gls{TH} function that will splice the required class definitions and view instances. +The code dataset also contains an implementation for defining field selectors and provides an implementation for a compiler (see \cref{chp:research_data_management}). +Furthermore, by writing a custom quasiquoter, pattern matches in natural syntax can be automatically converted to the internal representation of the \gls{DSL}, thus removing the syntax burden of the facilities. +The use of a custom quasiquoter does require the \gls{DSL} programmer to write a parser for their \gls{DSL}, i.e.\ the parser is not inherited from the host language as is often the case in an embedded \gls{DSL}. +However, by making use of modern parser combinator libraries, this overhead is limited and errors are already caught at compilation. + +\subsection{Future work} +For future work, it would be interesting to see how generating boilerplate for user-defined data types translates from shallow embedding to deep embedding. +In deep embedding, the language constructs are expressed as data types in the host language. +Adding new constructs, e.g.\ constructors, deconstructors, and constructor tests, for the user-defined data type therefore requires extending the data type. +Techniques such as data types \`a la carte~\cite{swierstra_data_2008} and open data types~\cite{loh_open_2006} show that it is possible to extend data types orthogonally but whether metaprogramming can still readily be used is something that needs to be researched. +It may also be possible to implemented (parts) of the boilerplate generation using \gls{TTH} (see \cref{ssec_fcd:typed_template_haskell}) to achieve more confidence in the type correctness of the implementation. + +Another venue of research is to try to find the limits of this technique regarding richer data type definitions. +It would be interesting to see whether it is possible to apply the technique on data types with existentially quantified type variables or full-fledged generalised \glspl{ADT}~\cite{hinze_fun_2003}. +It is not possible to straightforwardly lift the deconstructors to type classes because existentially quantified type variables will escape. +Rank-2 polymorphism offers tools to define the types in such a way that this is not the case anymore. +However, implementing compiling views on the \gls{DSL} is complicated because it would require inventing values of an existentially quantified type variable to satisfy the type system which is difficult. + +Finally, having to write a parser for the \gls{DSL} is extra work. +Future research could determine whether it is possible to generate this using \gls{TH} as well. \input{subfilepostamble} \end{document} diff --git a/glossaries.tex b/glossaries.tex index afe557e..f21d473 100644 --- a/glossaries.tex +++ b/glossaries.tex @@ -7,6 +7,7 @@ \newacronym{CWS}{PWS}{clean wemos supersensor} \newacronym{DSL}{DSL}{domain-specific language} \newacronym{EDSL}{eDSL}{embedded \acrshort{DSL}} +\newacronym{QDSL}{QDSL}{quoted \acrshort{DSL}} \newacronym{FP}{FP}{functional programming} \newacronym{GADT}{GADT}{generalised \acrshort{ADT}} \newacronym{GHC}{GHC}{Glasgow Haskell Compiler} @@ -16,6 +17,7 @@ \newacronym{GUI}{GUI}{graphical \acrlong{UI}} \newacronym{IOT}{IoT}{internet of things} \newacronym{IO}{IO}{input/output} +\newacronym{IR}{IL}{intermediate representation} \newacronym{LEAN}{LEAN}{language of East-Anglia and Nijmegen} \newacronym{LED}{LED}{light-emitting diode} \newacronym{MCU}{MCU}{microcontroller unit} @@ -29,6 +31,8 @@ \newacronym{SDS}{SDS}{shared data source} \newacronym{SN}{SN}{sensor network} \newacronym{TOP}{TOP}{task-oriented programming} +\newacronym{TH}{TH}{Template Haskell} +\newacronym{TTH}{TTH}{Typed \acrlong{TH}} \newacronym{TOSD}{TOSD}{task-oriented software development} \newacronym{TRS}{TRS}{term rewriting system} \newacronym{UI}{UI}{user interface} diff --git a/lstlanghaskell.sty b/lstlanghaskell.sty index 5a74664..c45f848 100644 --- a/lstlanghaskell.sty +++ b/lstlanghaskell.sty @@ -1,12 +1,57 @@ \lstdefinestyle{haskell}{% language=Haskell, deletekeywords={% - True,False,% - Bool,Int,Integer,Float,Double,String,% - Maybe,Nothing,Just,% - zip,length,Show,show,Num,Eq,print,% - error,id}, - morekeywords={forall}, + Applicative,% + Bool,% + Char,% + Double,% + Either,% + Eq,% + False,% + Float,% + Fractional,% + Functor,% + Int,% + Integer,% + Just,% + Left,% + List,% + Maybe,% + Monad,% + Nothing,% + Num,% + Right,% + Show,% + String,% + True,% + concatMap,% + const,% + div,% + error,% + fail,% + foldM,% + foldl,% + foldr,% + fst,% + id,% + length,% + map,% + mapM,% + pred,% + print,% + product,% + sequence,% + show,% + snd,% + sum,% + uncurry,% + undefined,% + unwords,% + unzip,% + zip,% + zipWith,% + } + morekeywords={forall,Q}, literate=% {forall}{{$\forall$}}1 {\_}{{\raisebox{.15ex}{\_}}}1 @@ -17,4 +62,12 @@ {=>}{{$\Rightarrow$}}2 {<=}{{$\Leftarrow$}}2 {...}{{$\cdots$}}1 %chktex 11 + {\[p|}{{$\llbracket_p$}}2 + {\[d|}{{$\llbracket_d$}}2 + {\[t|}{{$\llbracket_t$}}2 + {\[e|}{{$\llbracket_e$}}2 + {\[dsl|}{{$\llbracket_{dsl}$}}4 + {\[bin|}{{$\llbracket_{bin}$}}4 + {\[|}{{$\llbracket$}}1 + {|\]}{{$\rrbracket$}}1 } diff --git a/other.bib b/other.bib index 46bff99..ba881fd 100644 --- a/other.bib +++ b/other.bib @@ -597,6 +597,42 @@ few changes in existing programs.}, file = {Cheney and Hinze - 2002 - A lightweight implementation of generics and dynam.pdf:/home/mrl/.local/share/zotero/storage/FZ6EGJRJ/Cheney and Hinze - 2002 - A lightweight implementation of generics and dynam.pdf:application/pdf;HW02.pdf:/home/mrl/.local/share/zotero/storage/A8Z49NK6/HW02.pdf:application/pdf}, } +@article{lilis_survey_2019, + title = {A {Survey} of {Metaprogramming} {Languages}}, + volume = {52}, + issn = {0360-0300}, + url = {https://doi.org/10.1145/3354584}, + doi = {10.1145/3354584}, + abstract = {Metaprogramming is the process of writing computer programs that treat programs as data, enabling them to analyze or transform existing programs or generate new ones. While the concept of metaprogramming has existed for several decades, activities focusing on metaprogramming have been increasing rapidly over the past few years, with most languages offering some metaprogramming support and the amount of metacode being developed growing exponentially. In this article, we introduce a taxonomy of metaprogramming languages and present a survey of metaprogramming languages and systems based on the taxonomy. Our classification is based on the metaprogramming model adopted by the language, the phase of the metaprogram evaluation, the metaprogram source location, and the relation between the metalanguage and the object language.}, + number = {6}, + journal = {ACM Comput. Surv.}, + author = {Lilis, Yannis and Savidis, Anthony}, + month = oct, + year = {2019}, + note = {Place: New York, NY, USA +Publisher: Association for Computing Machinery}, + keywords = {aspect-oriented programming, generative programming, macro systems, meta-object protocols, Metaprogramming, multistage languages, reflection}, + file = {Lilis and Savidis - 2019 - A Survey of Metaprogramming Languages.pdf:/home/mrl/.local/share/zotero/storage/9MS6TUNR/Lilis and Savidis - 2019 - A Survey of Metaprogramming Languages.pdf:application/pdf}, +} + +@inproceedings{mainland_why_2007, + address = {New York, NY, USA}, + series = {Haskell '07}, + title = {Why {It}'s {Nice} to {Be} {Quoted}: {Quasiquoting} for {Haskell}}, + isbn = {978-1-59593-674-5}, + url = {https://doi.org/10.1145/1291201.1291211}, + doi = {10.1145/1291201.1291211}, + abstract = {Quasiquoting allows programmers to use domain specific syntax to construct program fragments. By providing concrete syntax for complex data types, programs become easier to read, easier to write, and easier to reason about and maintain. Haskell is an excellent host language for embedded domain specific languages, and quasiquoting ideally complements the language features that make Haskell perform so well in this area. Unfortunately, until now no Haskell compiler has provided support for quasiquoting. We present an implementation in GHC and demonstrate that by leveraging existing compiler capabilities, building a full quasiquoter requires little more work than writing a parser. Furthermore, we provide a compile-time guarantee that all quasiquoted data is type-correct.}, + booktitle = {Proceedings of the {ACM} {SIGPLAN} {Workshop} on {Haskell} {Workshop}}, + publisher = {Association for Computing Machinery}, + author = {Mainland, Geoffrey}, + year = {2007}, + note = {event-place: Freiburg, Germany}, + keywords = {meta programming, quasiquoting}, + pages = {73--82}, + file = {Mainland - 2007 - Why It's Nice to Be Quoted Quasiquoting for Haske.pdf:/home/mrl/.local/share/zotero/storage/PSJ59GY2/Mainland - 2007 - Why It's Nice to Be Quoted Quasiquoting for Haske.pdf:application/pdf}, +} + @article{tratt_domain_2008, title = {Domain {Specific} {Language} {Implementation} via {Compile}-{Time} {Meta}-{Programming}}, volume = {30}, @@ -615,7 +651,40 @@ Publisher: Association for Computing Machinery}, file = {Tratt - 2008 - Domain Specific Language Implementation via Compil.pdf:/home/mrl/.local/share/zotero/storage/HHGYJK4H/Tratt - 2008 - Domain Specific Language Implementation via Compil.pdf:application/pdf}, } +@inproceedings{kariotis_making_2008, + address = {New York, NY, USA}, + series = {Haskell '08}, + title = {Making {Monads} {First}-{Class} with {Template} {Haskell}}, + isbn = {978-1-60558-064-7}, + url = {https://doi.org/10.1145/1411286.1411300}, + doi = {10.1145/1411286.1411300}, + abstract = {Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.}, + booktitle = {Proceedings of the {First} {ACM} {SIGPLAN} {Symposium} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Kariotis, Pericles S. and Procter, Adam M. and Harrison, William L.}, + year = {2008}, + note = {event-place: Victoria, BC, Canada}, + keywords = {domain-specific languages, monads, staged programming}, + pages = {99--110}, + file = {Kariotis et al. - 2008 - Making Monads First-Class with Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/ZLX24WE8/Kariotis et al. - 2008 - Making Monads First-Class with Template Haskell.pdf:application/pdf}, +} + +@inproceedings{gill_haskell_2009, + address = {Berlin, Heidelberg}, + title = {A {Haskell} {Hosted} {DSL} for {Writing} {Transformation} {Systems}}, + isbn = {978-3-642-03034-5}, + abstract = {KURE is a Haskell hosted Domain Specific Language (DSL) for writing transformation systems based on rewrite strategies. When writing transformation systems, a significant amount of engineering effort goes into setting up plumbing to make sure that specific rewrite rules can fire. Systems like Stratego and Strafunski provide most of this plumbing as infrastructure, allowing the DSL user to focus on the rewrite rules. KURE is a strongly typed strategy control language in the tradition of Stratego and Strafunski. It is intended for writing reasonably efficient rewrite systems, makes use of type families to provide a delimited generic mechanism for tree rewriting, and provides support for efficient identity rewrite detection.}, + booktitle = {Domain-{Specific} {Languages}}, + publisher = {Springer Berlin Heidelberg}, + author = {Gill, Andy}, + editor = {Taha, Walid Mohamed}, + year = {2009}, + pages = {285--309}, + file = {Gill2009_Chapter_AHaskellHostedDSLForWritingTra.pdf:/home/mrl/.local/share/zotero/storage/I9RJNDYR/Gill2009_Chapter_AHaskellHostedDSLForWritingTra.pdf:application/pdf}, +} + @book{peyton_jones_implementation_1987, + address = {Hertfordshire}, title = {The {Implementation} of {Functional} {Programming} {Languages}}, url = {https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/}, abstract = {My 1987 book is now out of print, but it is available here in its entirety in PDF form, in one of two formats: single-page portrait double-page landscape Both are fully searchable, thanks to OCR and Norman Ramsey. Errata Section 5.2.4, p87. We need an extra rule match us [] E = E This accounts for the possibility that in the constructor rule (Section 5.2.4) there may be some non-nullary constructors for which there are no equations. P168, line 2, "VAR" should be "TVAR".}, @@ -626,6 +695,111 @@ Publisher: Association for Computing Machinery}, file = {Peyton Jones - 1987 - The Implementation of Functional Programming Langu.pdf:/home/mrl/.local/share/zotero/storage/9RIR6KGD/Peyton Jones - 1987 - The Implementation of Functional Programming Langu.pdf:application/pdf}, } +@inproceedings{sheard_template_2002, + address = {New York, NY, USA}, + series = {Haskell '02}, + title = {Template {Meta}-{Programming} for {Haskell}}, + isbn = {1-58113-605-6}, + url = {https://doi.org/10.1145/581690.581691}, + doi = {10.1145/581690.581691}, + abstract = {We propose a new extension to the purely functional programming language Haskell that supports compile-time meta-programming. The purpose of the system is to support the algorithmic construction of programs at compile-time.The ability to generate code at compile time allows the programmer to implement such features as polytypic programs, macro-like expansion, user directed optimization (such as inlining), and the generation of supporting data structures and functions from existing data structures and functions.Our design is being implemented in the Glasgow Haskell Compiler, ghc.}, + booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} {Workshop} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Sheard, Tim and Jones, Simon Peyton}, + year = {2002}, + note = {event-place: Pittsburgh, Pennsylvania}, + keywords = {meta programming, templates}, + pages = {1--16}, + file = {Sheard and Jones - 2002 - Template Meta-Programming for Haskell.pdf:/home/mrl/.local/share/zotero/storage/2GSK6DSF/Sheard and Jones - 2002 - Template Meta-Programming for Haskell.pdf:application/pdf}, +} + +@inproceedings{seefried_optimising_2004, + address = {Berlin, Heidelberg}, + title = {Optimising {Embedded} {DSLs} {Using} {Template} {Haskell}}, + isbn = {978-3-540-30175-2}, + abstract = {Embedded domain specific languages (EDSLs) provide a specialised language for a particular application area while harnessing the infrastructure of an existing general purpose programming language. The reduction in implementation costs that results from this approach comes at a price: the EDSL often compiles to inefficient code since the host language's compiler only optimises at the level of host language constructs. The paper presents an approach to solving this problem based on compile-time meta-programming which retains the simplicity of the embedded approach. We use PanTHeon, our implementation of an existing EDSL for image synthesis to demonstrate the benefits and drawbacks of this approach. Furthermore, we suggest potential improvements to Template Haskell, the meta-programming framework we are using, which would greatly improve its applicability to this kind of task.}, + booktitle = {Generative {Programming} and {Component} {Engineering}}, + publisher = {Springer Berlin Heidelberg}, + author = {Seefried, Sean and Chakravarty, Manuel and Keller, Gabriele}, + editor = {Karsai, Gabor and Visser, Eelco}, + year = {2004}, + pages = {186--205}, + file = {Seefried et al. - 2004 - Optimising Embedded DSLs Using Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/ZRKQ9AH6/Seefried et al. - 2004 - Optimising Embedded DSLs Using Template Haskell.pdf:application/pdf}, +} + +@article{hammond_automatic_2003, + title = {{AUTOMATIC} {SKELETONS} {IN} {TEMPLATE} {HASKELL}}, + volume = {13}, + url = {https://doi.org/10.1142/S0129626403001380}, + doi = {10.1142/S0129626403001380}, + abstract = {This paper uses Template Haskell to automatically select appropriate skeleton implementations in the Eden parallel dialect of Haskell. The approach allows implementation parameters to be statically tuned according to architectural cost models based on source analyses. This permits us to target a range of parallel architecture classes from a single source specification. A major advantage of the approach is that cost models are user-definable and can be readily extended to new data or computation structures etc.}, + number = {03}, + journal = {Parallel Processing Letters}, + author = {Hammond, Kevin and Berthold, Jost and Loogen, Rita}, + year = {2003}, + note = {\_eprint: https://doi.org/10.1142/S0129626403001380}, + pages = {413--424}, + file = {Hammond et al. - 2003 - AUTOMATIC SKELETONS IN TEMPLATE HASKELL.pdf:/home/mrl/.local/share/zotero/storage/HBQ8UXY3/Hammond et al. - 2003 - AUTOMATIC SKELETONS IN TEMPLATE HASKELL.pdf:application/pdf}, +} + +@inproceedings{adams_template_2012, + address = {New York, NY, USA}, + series = {Haskell '12}, + title = {Template {Your} {Boilerplate}: {Using} {Template} {Haskell} for {Efficient} {Generic} {Programming}}, + isbn = {978-1-4503-1574-6}, + url = {https://doi.org/10.1145/2364506.2364509}, + doi = {10.1145/2364506.2364509}, + abstract = {Generic programming allows the concise expression of algorithms that would otherwise require large amounts of handwritten code. A number of such systems have been developed over the years, but a common drawback of these systems is poor runtime performance relative to handwritten, non-generic code. Generic-programming systems vary significantly in this regard, but few consistently match the performance of handwritten code. This poses a dilemma for developers. Generic-programming systems offer concision but cost performance. Handwritten code offers performance but costs concision.This paper explores the use of Template Haskell to achieve the best of both worlds. It presents a generic-programming system for Haskell that provides both the concision of other generic-programming systems and the efficiency of handwritten code. Our system gives the programmer a high-level, generic-programming interface, but uses Template Haskell to generate efficient, non-generic code that outperforms existing generic-programming systems for Haskell.This paper presents the results of benchmarking our system against both handwritten code and several other generic-programming systems. In these benchmarks, our system matches the performance of handwritten code while other systems average anywhere from two to twenty times slower.}, + booktitle = {Proceedings of the 2012 {Haskell} {Symposium}}, + publisher = {Association for Computing Machinery}, + author = {Adams, Michael D. and DuBuisson, Thomas M.}, + year = {2012}, + note = {event-place: Copenhagen, Denmark}, + keywords = {generic programming, scrap your boilerplate, template haskell}, + pages = {13--24}, + file = {Adams and DuBuisson - 2012 - Template Your Boilerplate Using Template Haskell .pdf:/home/mrl/.local/share/zotero/storage/ANAHWLB5/Adams and DuBuisson - 2012 - Template Your Boilerplate Using Template Haskell .pdf:application/pdf}, +} + +@inproceedings{norell_prototyping_2004, + address = {Berlin, Heidelberg}, + title = {Prototyping {Generic} {Programming} in {Template} {Haskell}}, + isbn = {978-3-540-27764-4}, + abstract = {Generic Programming deals with the construction of programs that can be applied to many different datatypes. This is achieved by parameterizing the generic programs by the structure of the datatypes on which they are to be applied. Programs that can be defined generically range from simple map functions through pretty printers to complex XML tools.}, + booktitle = {Mathematics of {Program} {Construction}}, + publisher = {Springer Berlin Heidelberg}, + author = {Norell, Ulf and Jansson, Patrik}, + editor = {Kozen, Dexter}, + year = {2004}, + pages = {314--333}, + file = {Norell and Jansson - 2004 - Prototyping Generic Programming in Template Haskel.pdf:/home/mrl/.local/share/zotero/storage/S3EXD65Z/Norell and Jansson - 2004 - Prototyping Generic Programming in Template Haskel.pdf:application/pdf}, +} + +@incollection{odonnell_embedding_2004, + address = {Berlin, Heidelberg}, + title = {Embedding a {Hardware} {Description} {Language} in {Template} {Haskell}}, + isbn = {978-3-540-25935-0}, + url = {https://doi.org/10.1007/978-3-540-25935-0_9}, + abstract = {Hydra is a domain-specific language for designing digital circuits, which is implemented by embedding within Haskell. Many features required for hardware specification fit well within functional languages, leading in many cases to a perfect embedding. There are some situations, including netlist generation and software logic probes, where the DSL does not fit exactly within the host functional language. A new solution to these problems is based on program transformations performed automatically by metaprograms in Template Haskell.}, + booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}}, + publisher = {Springer Berlin Heidelberg}, + author = {O'Donnell, John T.}, + editor = {Lengauer, Christian and Batory, Don and Consel, Charles and Odersky, Martin}, + year = {2004}, + doi = {10.1007/978-3-540-25935-0_9}, + pages = {143--164}, + file = {O'Donnell - 2004 - Embedding a Hardware Description Language in Templ.pdf:/home/mrl/.local/share/zotero/storage/Z2XT7SM3/O'Donnell - 2004 - Embedding a Hardware Description Language in Templ.pdf:application/pdf}, +} + +@misc{lynagh_unrolling_2003, + title = {Unrolling and {Simplifying} {Expressions} with {Template} {Haskell}}, + url = {http://web.comlab.ox.ac.uk/oucl/work/ian.lynagh/papers/}, + urldate = {2021-09-07}, + author = {Lynagh, Ian}, + month = may, + year = {2003}, + file = {10.1.1.5.9813.pdf:/home/mrl/.local/share/zotero/storage/G4AFM8XZ/10.1.1.5.9813.pdf:application/pdf}, +} + @article{elliott_compiling_2003, title = {Compiling embedded languages}, volume = {13}, @@ -639,6 +813,22 @@ Publisher: Association for Computing Machinery}, file = {Elliott et al. - 2003 - Compiling embedded languages.pdf:/home/mrl/.local/share/zotero/storage/3X4Z6AKB/Elliott et al. - 2003 - Compiling embedded languages.pdf:application/pdf}, } +@incollection{czarnecki_dsl_2004, + address = {Berlin, Heidelberg}, + title = {{DSL} {Implementation} in {MetaOCaml}, {Template} {Haskell}, and {C}++}, + isbn = {978-3-540-25935-0}, + url = {https://doi.org/10.1007/978-3-540-25935-0_4}, + abstract = {A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques – staged interpreters and templates – can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.}, + booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}}, + publisher = {Springer Berlin Heidelberg}, + author = {Czarnecki, Krzysztof and O'Donnell, John T. and Striegnitz, Jörg and Taha, Walid}, + editor = {Lengauer, Christian and Batory, Don and Consel, Charles and Odersky, Martin}, + year = {2004}, + doi = {10.1007/978-3-540-25935-0_4}, + pages = {51--72}, + file = {Czarnecki et al. - 2004 - DSL Implementation in MetaOCaml, Template Haskell,.pdf:/home/mrl/.local/share/zotero/storage/U6E3325Q/Czarnecki et al. - 2004 - DSL Implementation in MetaOCaml, Template Haskell,.pdf:application/pdf}, +} + @inproceedings{sheard_accomplishments_2001, address = {Berlin, Heidelberg}, title = {Accomplishments and {Research} {Challenges} in {Meta}-programming}, @@ -653,6 +843,140 @@ Publisher: Association for Computing Machinery}, file = {Sheard - 2001 - Accomplishments and Research Challenges in Meta-pr.pdf:/home/mrl/.local/share/zotero/storage/M7NT6USA/Sheard - 2001 - Accomplishments and Research Challenges in Meta-pr.pdf:application/pdf}, } +@inproceedings{kohlbecker_hygienic_1986, + address = {New York, NY, USA}, + series = {{LFP} '86}, + title = {Hygienic {Macro} {Expansion}}, + isbn = {0-89791-200-4}, + url = {https://doi.org/10.1145/319838.319859}, + doi = {10.1145/319838.319859}, + booktitle = {Proceedings of the 1986 {ACM} {Conference} on {LISP} and {Functional} {Programming}}, + publisher = {Association for Computing Machinery}, + author = {Kohlbecker, Eugene and Friedman, Daniel P. and Felleisen, Matthias and Duba, Bruce}, + year = {1986}, + note = {event-place: Cambridge, Massachusetts, USA}, + pages = {151--161}, + file = {Kohlbecker et al. - 1986 - Hygienic Macro Expansion.pdf:/home/mrl/.local/share/zotero/storage/MFH642JU/Kohlbecker et al. - 1986 - Hygienic Macro Expansion.pdf:application/pdf}, +} + +@inproceedings{lammel_scrap_2003, + address = {New York, NY, USA}, + series = {{TLDI} '03}, + title = {Scrap {Your} {Boilerplate}: {A} {Practical} {Design} {Pattern} for {Generic} {Programming}}, + isbn = {1-58113-649-8}, + url = {https://doi.org/10.1145/604174.604179}, + doi = {10.1145/604174.604179}, + abstract = {We describe a design pattern for writing programs that traverse data structures built from rich mutually-recursive data types. Such programs often have a great deal of "boilerplate" code that simply walks the structure, hiding a small amount of "real" code that constitutes the reason for the traversal.Our technique allows most of this boilerplate to be written once and for all, or even generated mechanically, leaving the programmer free to concentrate on the important part of the algorithm. These generic programs are much more adaptive when faced with data structure evolution because they contain many fewer lines of type-specific code.Our approach is simple to understand, reasonably efficient, and it handles all the data types found in conventional functional programming languages. It makes essential use of rank-2 polymorphism, an extension found in some implementations of Haskell. Further it relies on a simple type-safe cast operator.}, + booktitle = {Proceedings of the 2003 {ACM} {SIGPLAN} {International} {Workshop} on {Types} in {Languages} {Design} and {Implementation}}, + publisher = {Association for Computing Machinery}, + author = {Lämmel, Ralf and Jones, Simon Peyton}, + year = {2003}, + note = {event-place: New Orleans, Louisiana, USA}, + keywords = {generic programming, rank-2 types, traversal, type cast}, + pages = {26--37}, + file = {Lämmel and Jones - 2003 - Scrap Your Boilerplate A Practical Design Pattern.pdf:/home/mrl/.local/share/zotero/storage/P2PJYYY3/Lämmel and Jones - 2003 - Scrap Your Boilerplate A Practical Design Pattern.pdf:application/pdf}, +} + +@inproceedings{bawden_quasiquotation_1999, + address = {Aarhus, Denmark}, + series = {{BRICS} {Notes} {Series}}, + title = {Quasiquotation in {Lisp}}, + volume = {NS-99-1}, + doi = {10.1.1.22.1290}, + booktitle = {O. {Danvy}, {Ed}., {University} of {Aarhus}, {Dept}. of {Computer} {Science}}, + publisher = {BRICS}, + author = {Bawden, Alan}, + year = {1999}, + pages = {88--99}, + file = {Bawden - 1999 - Quasiquotation in Lisp.pdf:/home/mrl/.local/share/zotero/storage/CIFANZAW/Bawden - 1999 - Quasiquotation in Lisp.pdf:application/pdf}, +} + +@inproceedings{clifton-everest_embedding_2014, + address = {Cham}, + title = {Embedding {Foreign} {Code}}, + isbn = {978-3-319-04132-2}, + abstract = {Special purpose embedded languages facilitate generating high-performance code from purely functional high-level code; for example, we want to program highly parallel GPUs without the usual high barrier to entry and the time-consuming development process. We previously demonstrated the feasibility of a skeleton-based, generative approach to compiling such embedded languages.}, + booktitle = {Practical {Aspects} of {Declarative} {Languages}}, + publisher = {Springer International Publishing}, + author = {Clifton-Everest, Robert and McDonell, Trevor L. and Chakravarty, Manuel M. T. and Keller, Gabriele}, + editor = {Flatt, Matthew and Guo, Hai-Feng}, + year = {2014}, + pages = {136--151}, + file = {Clifton-Everest et al. - 2014 - Embedding Foreign Code.pdf:/home/mrl/.local/share/zotero/storage/JTJGK5BX/Clifton-Everest et al. - 2014 - Embedding Foreign Code.pdf:application/pdf}, +} + +@inproceedings{shioda_libdsl_2014, + address = {New York, NY, USA}, + series = {{GPCE} 2014}, + title = {{LibDSL}: {A} {Library} for {Developing} {Embedded} {Domain} {Specific} {Languages} in d via {Template} {Metaprogramming}}, + isbn = {978-1-4503-3161-6}, + url = {https://doi.org/10.1145/2658761.2658770}, + doi = {10.1145/2658761.2658770}, + abstract = {This paper presents a library called LibDSL that helps the implementer of an embedded domain specific language (EDSL) effectively develop it in D language. The LibDSL library accepts as input some kinds of “specifications” of the EDSL that the implementer is going to develop and a D program within which an EDSL source program written by the user is embedded. It produces the front-end code of an LALR parser for the EDSL program and back-end code of the execution engine. LibDSL is able to produce two kinds of execution engines, namely compiler-based and interpreter-based engines, either of which the user can properly choose depending on whether an EDSL program is known at compile time or not. We have implemented the LibDSL system by using template metaprogramming and other advanced facilities such as compile-time function execution of D language. EDSL programs developed by means of LibDSL have a nice integrativeness with the host language.}, + booktitle = {Proceedings of the 2014 {International} {Conference} on {Generative} {Programming}: {Concepts} and {Experiences}}, + publisher = {Association for Computing Machinery}, + author = {Shioda, Masato and Iwasaki, Hideya and Sato, Shigeyuki}, + year = {2014}, + note = {event-place: Västerås, Sweden}, + keywords = {D language, Embedded domain specific languages, Library, Metaprogramming}, + pages = {63--72}, + file = {Shioda et al. - 2014 - LibDSL A Library for Developing Embedded Domain S.pdf:/home/mrl/.local/share/zotero/storage/3WFYJPFR/Shioda et al. - 2014 - LibDSL A Library for Developing Embedded Domain S.pdf:application/pdf}, +} + +@inproceedings{duregard_embedded_2011, + address = {New York, NY, USA}, + series = {Haskell '11}, + title = {Embedded {Parser} {Generators}}, + isbn = {978-1-4503-0860-1}, + url = {https://doi.org/10.1145/2034675.2034689}, + doi = {10.1145/2034675.2034689}, + abstract = {We present a novel method of embedding context-free grammars in Haskell, and to automatically generate parsers and pretty-printers from them. We have implemented this method in a library called BNFC-meta (from the BNF Converter, which it is built on). The library builds compiler front ends using metaprogramming instead of conventional code generation. Parsers are built from labelled BNF grammars that are defined directly in Haskell modules. Our solution combines features of parser generators (static grammar checks, a highly specialised grammar DSL) and adds several features that are otherwise exclusive to combinatory libraries such as the ability to reuse, parameterise and generate grammars inside Haskell.To allow writing grammars in concrete syntax, BNFC-meta provides a quasi-quoter that can parse grammars (embedded in Haskell files) at compile time and use metaprogramming to replace them with their abstract syntax. We also generate quasi-quoters so that the languages we define with BNFC-meta can be embedded in the same way. With a minimal change to the grammar, we support adding anti-quotation to the generated quasi-quoters, which allows users of the defined language to mix concrete and abstract syntax almost seamlessly. Unlike previous methods of achieving anti-quotation, the method used by BNFC-meta is simple, efficient and avoids polluting the abstract syntax types.}, + booktitle = {Proceedings of the 4th {ACM} {Symposium} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Duregård, Jonas and Jansson, Patrik}, + year = {2011}, + note = {event-place: Tokyo, Japan}, + keywords = {domain specific languages, metaprogramming}, + pages = {107--117}, + file = {Duregård and Jansson - 2011 - Embedded Parser Generators.pdf:/home/mrl/.local/share/zotero/storage/H5A8TPWV/Duregård and Jansson - 2011 - Embedded Parser Generators.pdf:application/pdf}, +} + +@inproceedings{eisenberg_promoting_2014, + address = {New York, NY, USA}, + series = {Haskell '14}, + title = {Promoting {Functions} to {Type} {Families} in {Haskell}}, + isbn = {978-1-4503-3041-1}, + url = {https://doi.org/10.1145/2633357.2633361}, + doi = {10.1145/2633357.2633361}, + abstract = {Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement.We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.}, + booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} {Symposium} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Eisenberg, Richard A. and Stolarek, Jan}, + year = {2014}, + note = {event-place: Gothenburg, Sweden}, + keywords = {defunctionalization, Haskell, type-level programming}, + pages = {95--106}, + file = {Eisenberg and Stolarek - 2014 - Promoting Functions to Type Families in Haskell.pdf:/home/mrl/.local/share/zotero/storage/PQXGBM6M/Eisenberg and Stolarek - 2014 - Promoting Functions to Type Families in Haskell.pdf:application/pdf}, +} + +@inproceedings{viera_staged_2018, + address = {New York, NY, USA}, + series = {{IFL} 2018}, + title = {A {Staged} {Embedding} of {Attribute} {Grammars} in {Haskell}}, + isbn = {978-1-4503-7143-8}, + url = {https://doi.org/10.1145/3310232.3310235}, + doi = {10.1145/3310232.3310235}, + abstract = {In this paper, we present an embedding of attribute grammars in Haskell, that is both modular and type-safe, while providing the user with domain specific error messages.Our approach involves to delay part of the safety checks to runtime. When a grammar is correct, we are able to extract a function that can be run without expecting any runtime error related to the EDSL.}, + booktitle = {Proceedings of the 30th {Symposium} on {Implementation} and {Application} of {Functional} {Languages}}, + publisher = {Association for Computing Machinery}, + author = {Viera, Marcos and Balestrieri, Florent and Pardo, Alberto}, + year = {2018}, + note = {event-place: Lowell, MA, USA}, + keywords = {Attribute Grammars, Dynamics, EDSL, Haskell, Staging}, + pages = {95--106}, + file = {Viera et al. - 2018 - A Staged Embedding of Attribute Grammars in Haskel.pdf:/home/mrl/.local/share/zotero/storage/53D4HT9C/Viera et al. - 2018 - A Staged Embedding of Attribute Grammars in Haskel.pdf:application/pdf}, +} + @incollection{kiselyov_typed_2012, address = {Berlin, Heidelberg}, title = {Typed {Tagless} {Final} {Interpreters}}, @@ -712,6 +1036,36 @@ Publisher: Association for Computing Machinery}, file = {Boulton et al. - Experience with embedding hardware description lan.pdf:/home/mrl/.local/share/zotero/storage/USAAA6WM/Boulton et al. - Experience with embedding hardware description lan.pdf:application/pdf}, } +@inproceedings{terei_safe_2012, + address = {New York, NY, USA}, + series = {Haskell '12}, + title = {Safe {Haskell}}, + isbn = {978-1-4503-1574-6}, + url = {https://doi.org/10.1145/2364506.2364524}, + doi = {10.1145/2364506.2364524}, + abstract = {Though Haskell is predominantly type-safe, implementations contain a few loopholes through which code can bypass typing and module encapsulation. This paper presents Safe Haskell, a language extension that closes these loopholes. Safe Haskell makes it possible to confine and safely execute untrusted, possibly malicious code. By strictly enforcing types, Safe Haskell allows a variety of different policies from API sandboxing to information-flow control to be implemented easily as monads. Safe Haskell is aimed to be as unobtrusive as possible. It enforces properties that programmers tend to meet already by convention. We describe the design of Safe Haskell and an implementation (currently shipping with GHC) that infers safety for code that lies in a safe subset of the language. We use Safe Haskell to implement an online Haskell interpreter that can securely execute arbitrary untrusted code with no overhead. The use of Safe Haskell greatly simplifies this task and allows the use of a large body of existing code and tools.}, + booktitle = {Proceedings of the 2012 {Haskell} {Symposium}}, + publisher = {Association for Computing Machinery}, + author = {Terei, David and Marlow, Simon and Peyton Jones, Simon and Mazières, David}, + year = {2012}, + note = {event-place: Copenhagen, Denmark}, + keywords = {haskell, security, type safety}, + pages = {137--148}, + file = {2364506.2364524.pdf:/home/mrl/.local/share/zotero/storage/5SMB272R/2364506.2364524.pdf:application/pdf}, +} + +@techreport{leijen_parsec_2001, + address = {Utrecht}, + title = {Parsec: {Direct} {Style} {Monadic} {Parser} {Combinators} {For} {The} {Real} {World}}, + language = {en}, + number = {UU-CS-2001-27}, + institution = {Universiteit Utrecht}, + author = {Leijen, Daan and Meijer, Erik}, + year = {2001}, + pages = {22}, + file = {Leijen - Parsec Direct Style Monadic Parser Combinators Fo.pdf:/home/mrl/.local/share/zotero/storage/J78G3FZ2/Leijen - Parsec Direct Style Monadic Parser Combinators Fo.pdf:application/pdf}, +} + @inproceedings{gibbons_folding_2014, address = {New York, NY, USA}, series = {{ICFP} '14}, @@ -765,6 +1119,24 @@ Publisher: Association for Computing Machinery}, file = {Odersky and Läufer - 1996 - Putting Type Annotations to Work.pdf:/home/mrl/.local/share/zotero/storage/WC37TU5H/Odersky and Läufer - 1996 - Putting Type Annotations to Work.pdf:application/pdf}, } +@inproceedings{najd_everything_2016, + address = {New York, NY, USA}, + series = {{PEPM} '16}, + title = {Everything {Old} is {New} {Again}: {Quoted} {Domain}-{Specific} {Languages}}, + isbn = {978-1-4503-4097-7}, + url = {https://doi.org/10.1145/2847538.2847541}, + doi = {10.1145/2847538.2847541}, + abstract = {We describe a new approach to implementing Domain-Specific Languages(DSLs), called Quoted DSLs (QDSLs), that is inspired by two old ideas:quasi-quotation, from McCarthy's Lisp of 1960, and the subformula principle of normal proofs, from Gentzen's natural deduction of 1935. QDSLs reuse facilities provided for the host language, since host and quoted terms share the same syntax, type system, and normalisation rules. QDSL terms are normalised to a canonical form, inspired by the subformula principle, which guarantees that one can use higher-order types in the source while guaranteeing first-order types in the target, and enables using types to guide fusion. We test our ideas by re-implementing Feldspar, which was originally implemented as an Embedded DSL (EDSL), as a QDSL; and we compare the QDSL and EDSL variants. The two variants produce identical code.}, + booktitle = {Proceedings of the 2016 {ACM} {SIGPLAN} {Workshop} on {Partial} {Evaluation} and {Program} {Manipulation}}, + publisher = {Association for Computing Machinery}, + author = {Najd, Shayan and Lindley, Sam and Svenningsson, Josef and Wadler, Philip}, + year = {2016}, + note = {event-place: St. Petersburg, FL, USA}, + keywords = {domain-specific language, DSL, EDSL, embedded language, normalisation, QDSL, quotation, subformula principle}, + pages = {25--36}, + file = {Najd et al. - 2016 - Everything Old is New Again Quoted Domain-Specifi.pdf:/home/mrl/.local/share/zotero/storage/NZJW5ZVF/Najd et al. - 2016 - Everything Old is New Again Quoted Domain-Specifi.pdf:application/pdf}, +} + @article{carette_finally_2009, title = {Finally tagless, partially evaluated: {Tagless} staged interpreters for simpler typed languages}, volume = {19}, @@ -778,6 +1150,23 @@ Publisher: Association for Computing Machinery}, file = {CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:/home/mrl/.local/share/zotero/storage/T8C8VMHP/CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:application/pdf}, } +@inproceedings{leijen_domain_2000, + address = {New York, NY, USA}, + series = {{DSL} '99}, + title = {Domain {Specific} {Embedded} {Compilers}}, + isbn = {1-58113-255-7}, + url = {https://doi.org/10.1145/331960.331977}, + doi = {10.1145/331960.331977}, + abstract = {Domain-specific embedded languages (DSELs) expressed in higher-order, typed (HOT) languages provide a composable framework for domain-specific abstractions. Such a framework is of greater utility than a collection of stand-alone domain-specific languages. Usually, embedded domain specific languages are build on top of a set of domain specific primitive functions that are ultimately implemented using some form of foreign function call. We sketch a general design pattern/or embedding client-server style services into Haskell using a domain specific embedded compiler for the server's source language. In particular we apply this idea to implement Haskell/DB, a domain specific embdedded compiler that dynamically generates of SQL queries from monad comprehensions, which are then executed on an arbitrary ODBC database server.}, + booktitle = {Proceedings of the 2nd {Conference} on {Domain}-{Specific} {Languages}}, + publisher = {Association for Computing Machinery}, + author = {Leijen, Daan and Meijer, Erik}, + year = {2000}, + note = {event-place: Austin, Texas, USA}, + pages = {109--122}, + file = {Leijen and Meijer - 2000 - Domain Specific Embedded Compilers.pdf:/home/mrl/.local/share/zotero/storage/YHPF2VZ6/Leijen and Meijer - 2000 - Domain Specific Embedded Compilers.pdf:application/pdf}, +} + @incollection{koopman_simulation_2018, address = {Cham}, title = {Simulation of a {Task}-{Based} {Embedded} {Domain} {Specific} {Language} for the {Internet} of {Things}}, @@ -942,6 +1331,21 @@ Publisher: Association for Computing Machinery}, file = {Baars and Swierstra - 2002 - Typing dynamic typing.pdf:/home/mrl/.local/share/zotero/storage/QSGVSTM4/Baars and Swierstra - 2002 - Typing dynamic typing.pdf:application/pdf}, } +@inproceedings{young_adding_2021, + address = {Berlin, Heidelberg}, + title = {On {Adding} {Pattern} {Matching} to {Haskell}-{Based} {Deeply} {Embedded} {Domain} {Specific} {Languages}}, + isbn = {978-3-030-67437-3}, + url = {https://doi.org/10.1007/978-3-030-67438-0_2}, + doi = {10.1007/978-3-030-67438-0_2}, + abstract = {Capturing control flow is the Achilles heel of Haskell-based deeply embedded domain specific languages. Rather than use the builtin control flow mechanisms, artificial control flow combinators are used instead. However, capturing traditional control flow in a deeply embedded domain specific language would support the writing of programs in a natural style by allowing the programmer to use the constructs that are already builtin to the base language, such as pattern matching and recursion. In this paper, we expand the capabilities of Haskell-based deep embeddings with a compiler extension for reifying conditionals and pattern matching. With this new support, the subset of Haskell that we use for expressing deeply embedded domain specific languages can be cleaner, Haskell-idiomatic, and more declarative in nature.}, + booktitle = {Practical {Aspects} of {Declarative} {Languages}: 23rd {International} {Symposium}, {PADL} 2021, {Copenhagen}, {Denmark}, {January} 18-19, 2021, {Proceedings}}, + publisher = {Springer-Verlag}, + author = {Young, David and Grebe, Mark and Gill, Andy}, + year = {2021}, + note = {event-place: Copenhagen, Denmark}, + pages = {20--36}, +} + @incollection{hinze_generic_2003, address = {Berlin, Heidelberg}, title = {Generic {Haskell}: {Practice} and {Theory}}, @@ -958,6 +1362,38 @@ Publisher: Association for Computing Machinery}, file = {Hinze and Jeuring - Generic Haskell practice and theory.pdf:/home/mrl/.local/share/zotero/storage/QDRNI5VB/Hinze and Jeuring - Generic Haskell practice and theory.pdf:application/pdf}, } +@inproceedings{torrano_strictness_2005, + address = {Bristol, UK}, + series = {Trends in {Functional} {Programming}}, + title = {Strictness {Analysis} and let-to-case {Transformation} using {Template} {Haskell}}, + volume = {6}, + isbn = {978-1-84150-176-5}, + booktitle = {Revised {Selected} {Papers} from the {Sixth} {Symposium} on {Trends} in {Functional} {Programming}, {TFP} 2005, {Tallinn}, {Estonia}, 23-24 {September} 2005}, + publisher = {Intellect}, + author = {Torrano, Carmen and Segura, Clara}, + editor = {Eekelen, Marko C. J. D. van}, + year = {2005}, + note = {event-place: Talinn, Estonia}, + pages = {429--442}, + file = {Torrano and Segura - Strictness Analysis and let-to-case Transformation.pdf:/home/mrl/.local/share/zotero/storage/RIYW9WFT/Torrano and Segura - Strictness Analysis and let-to-case Transformation.pdf:application/pdf}, +} + +@inproceedings{polak_automatic_2006, + address = {Bristol, UK}, + series = {Trends in {Functional} {Programming}}, + title = {Automatic {Graphical} {User} {Interface} {Form} {Generation} {Using} {Template} {Haskell}}, + volume = {7}, + isbn = {978-1-84150-188-8}, + booktitle = {Revised {Selected} {Papers} from the {Seventh} {Symposium} on {Trends} in {Functional} {Programming}, {TFP} 2006, {Nottingham}, {United} {Kingdom}, 19-21 {April} 2006}, + publisher = {Intellect}, + author = {Polak, Gracjan and Jarosz, Janusz}, + editor = {Nilsson, Henrik}, + year = {2006}, + note = {event-place: Nottingham, UK}, + pages = {1--11}, + file = {Polak and Jarosz - Automatic Graphical User Interface Form Generation.pdf:/home/mrl/.local/share/zotero/storage/8VK3D8JQ/Polak and Jarosz - Automatic Graphical User Interface Form Generation.pdf:application/pdf}, +} + @phdthesis{antonova_mtask_2022, address = {Nijmegen}, type = {Bachelor's {Thesis}}, @@ -969,6 +1405,17 @@ Publisher: Association for Computing Machinery}, file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/YIEQ97KK/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf}, } +@article{mcdonell_embedded_2021, + title = {Embedded {Pattern} {Matching}}, + volume = {abs/2108.13114}, + url = {https://arxiv.org/abs/2108.13114}, + journal = {CoRR}, + author = {McDonell, Trevor L. and Meredith, Joshua D. and Keller, Gabriele}, + year = {2021}, + note = {arXiv: 2108.13114}, + file = {2108.13114.pdf:/home/mrl/.local/share/zotero/storage/AJAT8AXI/2108.13114.pdf:application/pdf}, +} + @misc{wadler_expression_1998, title = {The expression problem}, url = {https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt}, @@ -993,7 +1440,7 @@ Publisher: Association for Computing Machinery}, @misc{wikipedia_contributors_rhapsody_2022, title = {Rhapsody (music) — {Wikipedia}, {The} {Free} {Encyclopedia}}, - url = {https://en.wikipedia.org/w/index.php?title=Rhapsody_(music)&oldid=1068385257}, + url = {https://en.wikipedia.org/w/index.php?title=Rhapsody_(music)\&oldid=1068385257}, urldate = {2022-09-06}, journal = {Wikipedia}, author = {{Wikipedia contributors}}, @@ -1012,6 +1459,18 @@ Publisher: Association for Computing Machinery}, pages = {219--247}, } +@article{achten_ins_1995, + title = {The ins and outs of {Clean} {I}/{O}}, + volume = {5}, + doi = {10.1017/S0956796800001258}, + number = {1}, + journal = {Journal of Functional Programming}, + author = {Achten, Peter and Plasmeijer, Rinus}, + year = {1995}, + note = {Publisher: Cambridge University Press}, + pages = {81--110}, +} + @inproceedings{peyton_jones_imperative_1993, address = {New York, NY, USA}, series = {{POPL} '93}, @@ -1028,3 +1487,210 @@ Publisher: Association for Computing Machinery}, pages = {71--84}, file = {Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/9DQ5V3N3/Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:application/pdf}, } + +@inproceedings{achten_high_1993, + address = {London}, + title = {High {Level} {Specification} of {I}/{O} in {Functional} {Languages}}, + isbn = {978-1-4471-3215-8}, + abstract = {The interface with the outside world has always been one of the weakest points of functional languages. It is not easy to incorporate I/O without being allowed to do side-effects. Furthermore, functional languages allow redexes to be evaluated in any order while I/O generally has to be performed in a very specific order. In this paper we present a new solution for the I/O problem which we have incorporated in the language Concurrent Clean. Concurrent Clean offers a linear type system called Unique Types. It makes it possible to define functions with side-effects without violating the functional semantics. Now it is possible to change any object in the world in the way we wanted: e.g. arrays can be updated in-situ, arbitrary file manipulation is possible. We have used this powerful tool among others to create a library for window based I/O. Using an explicit environment passing scheme provides a high-level and elegant functional specification method for I/O, called Event I/O. Now the specification of I/O has become one of the strengths of functional languages: interactive programs written in Concurrent Clean are concise, easy to write and comprehend as well as efficient. The presented solution can in principle be applied for any other functional language as well provided that it actually uses graph rewriting semantics in the implementation.}, + booktitle = {Functional {Programming}, {Glasgow} 1992}, + publisher = {Springer London}, + author = {Achten, Peter and van Groningen, John and Plasmeijer, Rinus}, + editor = {Launchbury, John and Sansom, Patrick}, + year = {1993}, + pages = {1--17}, + file = {Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:/home/mrl/.local/share/zotero/storage/4QVH7AYC/Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:application/pdf}, +} + +@inproceedings{pickering_staged_2020, + address = {New York, NY, USA}, + series = {Haskell 2020}, + title = {Staged {Sums} of {Products}}, + isbn = {978-1-4503-8050-8}, + url = {https://doi.org/10.1145/3406088.3409021}, + doi = {10.1145/3406088.3409021}, + abstract = {Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.}, + booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Pickering, Matthew and Löh, Andres and Wu, Nicolas}, + year = {2020}, + note = {event-place: Virtual Event, USA}, + keywords = {generic programming, staging}, + pages = {122--135}, + file = {Pickering et al. - 2020 - Staged Sums of Products.pdf:/home/mrl/.local/share/zotero/storage/Q6ZWX4YP/Pickering et al. - 2020 - Staged Sums of Products.pdf:application/pdf}, +} + +@article{xie_staging_2022, + title = {Staging with {Class}: {A} {Specification} for {Typed} {Template} {Haskell}}, + volume = {6}, + url = {https://doi.org/10.1145/3498723}, + doi = {10.1145/3498723}, + abstract = {Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs. We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus λ⇒ that elaborates into an explicit core calculus F. We show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations. Our design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation.}, + number = {POPL}, + journal = {Proc. ACM Program. Lang.}, + author = {Xie, Ningning and Pickering, Matthew and Löh, Andres and Wu, Nicolas and Yallop, Jeremy and Wang, Meng}, + month = jan, + year = {2022}, + note = {Place: New York, NY, USA +Publisher: Association for Computing Machinery}, + keywords = {Staging, Type Classes, Typed Template Haskell}, + file = {Xie et al. - 2022 - Staging with Class A Specification for Typed Temp.pdf:/home/mrl/.local/share/zotero/storage/QGDB5YHR/Xie et al. - 2022 - Staging with Class A Specification for Typed Temp.pdf:application/pdf}, +} + +@article{rhiger_type-safe_2009, + title = {Type-safe pattern combinators}, + volume = {19}, + doi = {10.1017/S0956796808007089}, + number = {2}, + journal = {Journal of Functional Programming}, + author = {Rhiger, Morten}, + year = {2009}, + note = {Publisher: Cambridge University Press}, + pages = {145--156}, + file = {RHIGER - 2009 - Type-safe pattern combinators.pdf:/home/mrl/.local/share/zotero/storage/D4N7PGBS/RHIGER - 2009 - Type-safe pattern combinators.pdf:application/pdf}, +} + +@inproceedings{de_vries_true_2014, + address = {New York, NY, USA}, + series = {{WGP} '14}, + title = {True {Sums} of {Products}}, + isbn = {978-1-4503-3042-8}, + url = {https://doi.org/10.1145/2633628.2633634}, + doi = {10.1145/2633628.2633634}, + abstract = {We introduce the sum-of-products (SOP) view for datatype-generic programming (in Haskell). While many of the libraries that are commonly in use today represent datatypes as arbitrary combinations of binary sums and products, SOP reflects the structure of datatypes more faithfully: each datatype is a single n-ary sum, where each component of the sum is a single n-ary product. This representation turns out to be expressible accurately in GHC with today's extensions. The resulting list-like structure of datatypes allows for the definition of powerful high-level traversal combinators, which in turn encourage the definition of generic functions in a compositional and concise style. A major plus of the SOP view is that it allows to separate function-specific metadata from the main structural representation and recombining this information later.}, + booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} {Workshop} on {Generic} {Programming}}, + publisher = {Association for Computing Machinery}, + author = {de Vries, Edsko and Löh, Andres}, + year = {2014}, + note = {event-place: Gothenburg, Sweden}, + keywords = {datatype-generic programming, generic views, json, lenses, metadata, sums of products, universes}, + pages = {83--94}, + file = {de Vries and Löh - 2014 - True Sums of Products.pdf:/home/mrl/.local/share/zotero/storage/QHT5IPQA/de Vries and Löh - 2014 - True Sums of Products.pdf:application/pdf}, +} + +@article{willis_staged_2020, + title = {Staged {Selective} {Parser} {Combinators}}, + volume = {4}, + url = {https://doi.org/10.1145/3409002}, + doi = {10.1145/3409002}, + abstract = {Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts. This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.}, + number = {ICFP}, + journal = {Proc. ACM Program. Lang.}, + author = {Willis, Jamie and Wu, Nicolas and Pickering, Matthew}, + month = aug, + year = {2020}, + note = {Place: New York, NY, USA +Publisher: Association for Computing Machinery}, + keywords = {combinators, meta-programming, parsers}, + file = {Willis et al. - 2020 - Staged Selective Parser Combinators.pdf:/home/mrl/.local/share/zotero/storage/RCD842QK/Willis et al. - 2020 - Staged Selective Parser Combinators.pdf:application/pdf}, +} + +@inproceedings{pickering_multi-stage_2019, + address = {New York, NY, USA}, + series = {Haskell 2019}, + title = {Multi-{Stage} {Programs} in {Context}}, + isbn = {978-1-4503-6813-1}, + url = {https://doi.org/10.1145/3331545.3342597}, + doi = {10.1145/3331545.3342597}, + abstract = {Cross-stage persistence is an essential aspect of multi-stage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit information—which are pervasive in Haskell—subtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multi-stage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a type-system, and an implementation in GHC is presented that fixes problems of the previous incarnation.}, + booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}}, + publisher = {Association for Computing Machinery}, + author = {Pickering, Matthew and Wu, Nicolas and Kiss, Csongor}, + year = {2019}, + note = {event-place: Berlin, Germany}, + keywords = {implicits, metaprogramming, staging}, + pages = {71--84}, + file = {Pickering et al. - 2019 - Multi-Stage Programs in Context.pdf:/home/mrl/.local/share/zotero/storage/3EW7FM44/Pickering et al. - 2019 - Multi-Stage Programs in Context.pdf:application/pdf}, +} + +@article{pickering_specification_2021, + title = {A {Specification} for {Typed} {Template} {Haskell}}, + volume = {abs/2112.03653}, + url = {https://arxiv.org/abs/2112.03653}, + journal = {CoRR}, + author = {Pickering, Matthew and Löh, Andres and Wu, Nicolas}, + year = {2021}, + note = {arXiv: 2112.03653}, + file = {Pickering et al. - 2021 - A Specification for Typed Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/YBTN4DLK/Pickering et al. - 2021 - A Specification for Typed Template Haskell.pdf:application/pdf}, +} + +@inproceedings{folmer_high-level_2022, + address = {Cham}, + title = {High-{Level} {Synthesis} of {Digital} {Circuits} from {Template} {Haskell} and {SDF}-{AP}}, + isbn = {978-3-031-15074-6}, + abstract = {Functional languages as input specifications for HLS-tools allow to specify data dependencies but do not contain a notion of time nor execution order. In this paper, we propose a method to add this notion to the functional description using the dataflow model SDF-AP. SDF-AP consists of patterns that express consumption and production that we can use to enforce resource usage. We created an HLS-tool that can synthesize parallel hardware, both data and control path, based on the repetition, expressed in Higher-Order Functions, combined with specified SDF-AP patterns.}, + booktitle = {Embedded {Computer} {Systems}: {Architectures}, {Modeling}, and {Simulation}}, + publisher = {Springer International Publishing}, + author = {Folmer, H. H. and Groote, R. de and Bekooij, M. J. G.}, + editor = {Orailoglu, Alex and Reichenbach, Marc and Jung, Matthias}, + year = {2022}, + pages = {3--27}, + file = {Folmer et al. - 2022 - High-Level Synthesis of Digital Circuits from Temp.pdf:/home/mrl/.local/share/zotero/storage/5JSW6MAL/Folmer et al. - 2022 - High-Level Synthesis of Digital Circuits from Temp.pdf:application/pdf}, +} + +@article{materzok_generating_2022, + title = {Generating {Circuits} with {Generators}}, + volume = {6}, + url = {https://doi.org/10.1145/3549821}, + doi = {10.1145/3549821}, + abstract = {The most widely used languages and methods used for designing digital hardware fall into two rough categories. One of them, register transfer level (RTL), requires specifying each and every component in the designed circuit. This gives the designer full control, but burdens the designer with many trivial details. The other, the high-level synthesis (HLS) method, allows the designer to abstract the details of hardware away and focus on the problem being solved. This method however cannot be used for a class of hardware design problems because the circuit's clock is also abstracted away. We present YieldFSM, a hardware description language that uses the generator abstraction to represent clock-level timing in a digital circuit. It represents a middle ground between the RTL and HLS approaches: the abstraction level is higher than in RTL, but thanks to explicit information about clock-level timing, it can be used in applications where RTL is traditionally used. We also present the YieldFSM compiler, which uses methods developed by the functional programming community – including continuation-passsing style translation and defunctionalization – to translate YieldFSM programs to Mealy machines. It is implemented using Template Haskell and the Clash functional hardware description language. We show that this approach leads to short and conceptually simple hardware descriptions.}, + number = {ICFP}, + journal = {Proc. ACM Program. Lang.}, + author = {Materzok, Marek}, + month = aug, + year = {2022}, + note = {Place: New York, NY, USA +Publisher: Association for Computing Machinery}, + keywords = {circuit synthesis, generators, hardware description languages}, + file = {Materzok - 2022 - Generating Circuits with Generators.pdf:/home/mrl/.local/share/zotero/storage/LH4Q8J73/Materzok - 2022 - Generating Circuits with Generators.pdf:application/pdf}, +} + +@article{egi_embedding_2022, + title = {Embedding {Non}-linear {Pattern} {Matching} with {Backtracking} for {Non}-free {Data} {Types} into {Haskell}}, + volume = {40}, + issn = {1882-7055}, + url = {https://doi.org/10.1007/s00354-022-00177-z}, + doi = {10.1007/s00354-022-00177-z}, + abstract = {Pattern matching is an important language construct for data abstraction. Many pattern-match extensions have been developed for extending the range of data types to which pattern matching is applicable. Among them, the pattern-match system proposed by Egi and Nishiwaki features practical pattern matching for non-free data types by providing a user-customizable non-linear pattern-match facility with backtracking. However, they implemented their proposal only in dynamically typed programming languages, and there were no proposals that allow programmers to benefit from both static type systems and expressive pattern matching. This paper proposes a method for implementing this pattern-match facility by meta-programming in Haskell. There are two technical challenges: (i) we need to design a set of typing rules for the pattern-match facility; (ii) we need to embed these typing rules in Haskell to make types of the pattern-match expressions inferable by the Haskell type system. We propose a set of typing rules and show that several GHC extensions, such as multi-parameter type classes, datatype promotion, GADTs, existential types, and view patterns, play essential roles for embedding these typing rules into Haskell. The implementation has already been distributed as a Haskell library miniEgison via Hackage.}, + number = {2}, + journal = {New Generation Computing}, + author = {Egi, Satoshi and Kawata, Akira and Kori, Mayuko and Ogawa, Hiromi}, + month = jul, + year = {2022}, + pages = {481--506}, + file = {Egi et al. - 2022 - Embedding Non-linear Pattern Matching with Backtra.pdf:/home/mrl/.local/share/zotero/storage/PXT9L9Z4/Egi et al. - 2022 - Embedding Non-linear Pattern Matching with Backtra.pdf:application/pdf}, +} + +@inproceedings{blanchette_liquid_2022, + address = {New York, NY, USA}, + series = {Haskell 2022}, + title = {Liquid {Proof} {Macros}}, + isbn = {978-1-4503-9438-3}, + url = {https://doi.org/10.1145/3546189.3549921}, + doi = {10.1145/3546189.3549921}, + abstract = {Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tactic-inspired DSL interface for more concise and user-friendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark.}, + booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} {International} {Haskell} {Symposium}}, + publisher = {Association for Computing Machinery}, + author = {Blanchette, Henry and Vazou, Niki and Lampropoulos, Leonidas}, + year = {2022}, + note = {event-place: Ljubljana, Slovenia}, + keywords = {Liquid Haskell, Proof Macros, Tactics}, + pages = {27--38}, + file = {Blanchette et al. - 2022 - Liquid Proof Macros.pdf:/home/mrl/.local/share/zotero/storage/YXPCWQNI/Blanchette et al. - 2022 - Liquid Proof Macros.pdf:application/pdf}, +} + +@phdthesis{baaij_digital_2015, + address = {Netherlands}, + type = {{PhD} {Thesis}}, + title = {Digital circuit in {C}\${\textbackslash}lambda\${aSH}: functional specifications and type-directed synthesis}, + abstract = {Over the last three decades, the number of transistors used in microchips has increased by three orders of magnitude, from millions to billions. The productivity of the designers, however, lags behind. Managing to implement complex algorithms, while keeping non-functional properties within desired bounds, and thoroughly verifying the design against its specification, are the main difficulties in circuit design. As a motivation for our work we make a qualitative analysis of the tools available to circuit designers. Here we see that progress has been slow, and that the same techniques have been used for over 20 years. We claim that functional languages can be used to raise the abstraction level in circuit design. Especially higher-order functional languages, where functions are first-class and can be manipulated by other functions, offer a single abstraction mechanism that can capture many design patterns. This thesis explores the idea of using the functional language Haskell directly as a hardware specification language, and move beyond the limitations of embedded languages. Additionally, we can use normal functions from existing Haskell libraries to model the behaviour of our circuits. This thesis describes the inner workings of our CλaSH compiler, which translates the aforementioned circuit descriptions written in Haskell to low-level descriptions in VHDL. The challenge then becomes the reduction of the higher-level abstractions in the descriptions to a form where synthesis is feasible. This thesis describes a term rewrite system (with bound variables) to achieve this reduction. We prove that this term rewrite system always reduces a polymorphic, higher-order circuit description to a synthesisable variant. Even when descriptions use high-level abstractions, the CλaSH compiler can synthesize efficient circuits. Case studies show that circuits designed in Haskell, and synthesized with the C?aSH compiler, are on par with hand-written VHDL, in both area and gate propagation delay. This thesis thus shows the merits of using a modern functional language for circuit design. The advanced type system and higher-order functions allow us to design circuits that have the desired property of being correct-by-construction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use high-level abstractions.}, + language = {Undefined}, + school = {University of Twente}, + author = {Baaij, C. P. R.}, + month = jan, + year = {2015}, + doi = {10.3990/1.9789036538039}, + note = {ISBN: 978-90-365-3803-9}, + keywords = {Digital Circuits, EC Grant Agreement nr.: FP7/248465, EC Grant Agreement nr.: FP7/610686, EWI-23939, FPGA, Functional Programming, Hardware, Haskell, IR-93962, Lambda calculus, METIS-308711, Rewrite Systems}, + file = {Baaij - 2015 - Digital circuit in CλaSH functional specification.pdf:/home/mrl/.local/share/zotero/storage/MYJ33ISL/Baaij - 2015 - Digital circuit in CλaSH functional specification.pdf:application/pdf}, +} diff --git a/preamble.tex b/preamble.tex index 9efb9df..8ddd2ef 100644 --- a/preamble.tex +++ b/preamble.tex @@ -13,6 +13,7 @@ \usepackage{atveryend} % \smaller command \everymath{\it\/} \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} %chktex 18 +\newcommand{\dcolon}[0]{\mathbin{::}} % Internationalisation \usepackage[dutch,russian,british]{babel} @@ -111,25 +112,6 @@ \nobibliography* \bibliographystyle{alpha} -% Hyperlinks and metadata -\usepackage[pagebackref]{hyperref} % hyperlinks -\renewcommand*{\backref}[1]{} -\renewcommand*{\backrefalt}[4]{[{% - \ifcase #1 not cited.\or p.~#2.\else pp. #2.\fi%chktex 1 -}]} -\hypersetup{% - pdftitle={\mytitle}, - pdfauthor={\myauthor}, - pdfkeywords={task-oriented programming, functional programming, domain specific languages, internet of things}, - hidelinks, -} -\usepackage[nodayofweek]{datetime} % Use a fixed document date -\urlstyle{same} -\usepackage{bookmark} -\usepackage{cleveref} % Easy references -\crefname{part}{movement}{movements} -\crefname{lstlisting}{listing}{listing} - % Graphics \usepackage{graphicx} % Images \graphicspath{{img/},{introduction/img}} @@ -152,13 +134,13 @@ % General listings settings \lstset{% basewidth=0.5em, - basicstyle=\tt\small, + basicstyle=\tt, breakatwhitespace=false, breaklines=true, captionpos=b, columns=[c]fixed, commentstyle=\sl, -% escapeinside={(+}{+)}, % chktex 9 + escapeinside={[+}{+]}, % chktex 9 frame=L, keepspaces=true, keywordstyle=\bf, @@ -179,6 +161,8 @@ \newcommand{\cleaninline}[1]{\lstinline[language=Clean,postbreak=]|#1|} \newcommand{\haskellinline}[1]{\lstinline[language=Haskell,style=haskell,postbreak=]|#1|} \newcommand{\haskelllhstexinline}[1]{\lstinline[language=Haskell,style=haskelllhstex,postbreak=]|#1|} +%For storing listings in footnotes +\newsavebox{\LstBox} % Fix list of listings title \renewcommand{\lstlistlistingname}{List of Listings} % Fix list of listings chapter separator @@ -214,6 +198,25 @@ } {} +% Hyperlinks and metadata +\usepackage[pagebackref]{hyperref} % hyperlinks +\renewcommand*{\backref}[1]{} +\renewcommand*{\backrefalt}[4]{[{% + \ifcase #1 not cited.\or p.~#2.\else pp. #2.\fi%chktex 1 +}]} +\hypersetup{% + pdftitle={\mytitle}, + pdfauthor={\myauthor}, + pdfkeywords={task-oriented programming, functional programming, domain specific languages, internet of things}, + hidelinks, +} +\usepackage[nodayofweek]{datetime} % Use a fixed document date +\urlstyle{same} +\usepackage{bookmark} +\usepackage{cleveref} % Easy references +\crefname{part}{movement}{movements} +\crefname{lstlisting}{listing}{listing} + % Glossaries and acronyms \usepackage[acronym,nonumberlist]{glossaries} \Addlcwords{of} -- 2.20.1