1 \documentclass[../thesis.tex
]{subfiles
}
3 \input{subfilepreamble
}
5 \setcounter{chapter
}{1}
9 \chapter{Deep embedding with class
}%
10 \label{chp:classy_deep_embedding
}
11 \begin{chapterabstract
}
12 The two flavours of
\gls{DSL
} embedding are shallow and deep embedding.
13 In functional languages, shallow embedding models the language constructs as functions in which the semantics are embedded.
14 Adding semantics is therefore cumbersome while adding constructs is a breeze.
15 Upgrading the functions to type classes lifts this limitation to a certain extent.
17 Deeply embedded languages represent their language constructs as data and the semantics are functions on it.
18 As a result, the language constructs are embedded in the semantics, hence adding new language constructs is laborious where adding semantics is trouble free.
20 This chapter shows that by abstracting the semantics functions in deep embedding to type classes, it is possible to easily add language constructs as well.
21 So-called classy deep embedding results in
\glspl{DSL
} that are extensible both in language constructs and in semantics while maintaining a concrete abstract syntax tree.
22 Additionally, little type-level trickery or complicated boilerplate code is required to achieve this.
25 \section{Introduction
}
26 The two flavours of
\gls{DSL
} embedding are deep and shallow embedding
\citep{boulton_experience_1992
}.
27 In
\gls{FP
} languages, shallow embedding models language constructs as functions in the host language.
28 As a result, adding new language constructs---extra functions---is easy.
29 However, the semantics of the language is embedded in these functions, making it troublesome to add semantics since it requires updating all existing language constructs.
31 On the other hand, deep embedding models language constructs as data in the host language.
32 The semantics of the language are represented by functions over the data.
33 Consequently, adding new semantics, i.e.\ novel functions, is straightforward.
34 It can be stated that the language constructs are embedded in the functions that form a semantics.
35 If one wants to add a language construct, all semantics functions must be revisited and revised to avoid ending up with partial functions.
37 This juxtaposition has been known for many years
\citep{reynolds_user-defined_1978
} and discussed by many others
\citep{krishnamurthi_synthesizing_1998
} but most famously dubbed the
\emph{expression problem
} by
\citet{wadler_expression_1998
}:
40 The
\emph{expression problem
} is a new name for an old problem.
41 The goal is to define a data type by cases, where one can add new cases to the data type and new functions over the data type, without recompiling existing code, and while retaining static type safety (e.g., no casts).
44 In shallow embedding, abstracting the functions to type classes disentangles the language constructs from the semantics, allowing extension both ways.
45 This technique is dubbed tagless-final embedding
\citep{carette_finally_2009
}, nonetheless it is no silver bullet.
46 Some semantics that require an intensional analysis of the syntax tree, such as transformation and optimisations, are difficult to implement in shallow embedding due to the lack of an explicit data structure representing the abstract syntax tree.
47 The semantics of the
\gls{DSL
} have to be combined and must hold some kind of state or context, so that structural information is not lost
\citep{kiselyov_typed_2012
}.
49 \subsection{Research contribution
}
50 This chapter shows how to apply the technique observed in tagless-final embedding to deep embedding.
51 The presented basic technique, christened
\emph{classy deep embedding
}, does not require advanced type system extensions to be used.
52 However, it is suitable for type system extensions such as
\glspl{GADT
}.
53 While this chapter is written as a literate
54 \Gls{HASKELL
} \citep{peyton_jones_haskell_2003
} program using some minor extensions provided by
\gls{GHC
} \citep{ghc_team_ghc_2021
}, the idea is applicable to other languages as well
\footnotemark.
55 \footnotetext{Lubbers, M. (
2021): Literate Haskell/lhs2
\TeX{} source code of the paper ``Deep Embedding
56 with Class'': TFP
2022.\ DANS.\
\url{https://doi.org/
10.5281/zenodo
.5081386}.
}
58 \section{Deep embedding
}
59 Pick a
\gls{DSL
}, any
\gls{DSL
}, pick the language of literal integers and addition.
60 In deep embedding, terms in the language are represented by data in the host language.
61 Hence, defining the constructs is as simple as creating the following algebraic data type
\footnote{All data types and functions are subscripted to indicate the evolution. When definitions are omitted for version $n$, version $n-
1$ is assumed.
}.
63 \begin{lstHaskellLhstex
}
67 \end{lstHaskellLhstex
}
69 Semantics are defined as functions on the
\haskelllhstexinline{Expr_0
} data type.
70 For example, a function transforming the term to an integer---an evaluator---is implemented as follows.
72 \begin{lstHaskellLhstex
}
73 eval_0 :: Expr_0 -> Int
75 eval_0 (Add_0 e1 e2) = eval_0 e1 + eval_0 e2
76 \end{lstHaskellLhstex
}
78 Adding semantics---e.g.\ a printer---just means adding another function while the existing functions remain untouched.
79 I.e.\ the key property of deep embedding.
80 The following function, transforming the
\haskelllhstexinline{Expr_0
} data type to a string, defines a simple printer for our language.
82 \begin{lstHaskellLhstex
}
83 print_0 :: Expr_0 -> String
84 print_0 (Lit_0 v) = show v
85 print_0 (Add_0 e1 e2) = "(" ++ print_0 e1 ++ "-" ++ print_0 e2 ++ ")"
86 \end{lstHaskellLhstex
}
88 While the language is concise and elegant, it is not very expressive.
89 Traditionally, extending the language is achieved by adding a case to the
\haskelllhstexinline{Expr_0
} data type.
90 So, adding subtraction to the language results in the following revised data type.
92 \begin{lstHaskellLhstex
}
97 \end{lstHaskellLhstex
}
99 Extending the
\gls{DSL
} with language constructs exposes the Achilles' heel of deep embedding.
100 Adding a case to the data type means that all semantics functions have become partial and need to be updated to be able to handle this new case.
101 This does not seem like an insurmountable problem, but it does pose a problem if either the functions or the data type itself are written by others or are contained in a closed library.
103 \section{Shallow embedding
}
104 Conversely, let us see how this would be done in shallow embedding.
105 First, the data type is represented by functions in the host language with embedded semantics.
106 Therefore, the evaluators for literals and addition both become a function in the host language as follows.
108 \begin{lstHaskellLhstex
}
111 lit_s :: Int -> Sem_s
114 add_s :: Sem_s -> Sem_s -> Sem_s
115 add_s e1 e2 = e1 + e2
116 \end{lstHaskellLhstex
}
118 Adding constructions to the language is done by adding functions.
119 Hence, the following function adds subtraction to our language.
121 \begin{lstHaskellLhstex
}
122 sub_s :: Sem_s -> Sem_s -> Sem_s
123 sub_s e1 e2 = e1 - e2
124 \end{lstHaskellLhstex
}
126 Adding semantics on the other hand---e.g.\ a printer---is not that simple because the semantics are part of the functions representing the language constructs.
127 One way to add semantics is to change all functions to execute both semantics at the same time.
128 In our case this means changing the type of
\haskelllhstexinline{Sem_s
} to be
\haskelllhstexinline{(Int, String)
} so that all functions operate on a tuple containing the result of the evaluator and the printed representation at the same time.
%chktex 36
129 Alternatively, a single semantics can be defined that represents a fold over the language constructs
\citep{gibbons_folding_2014
}, delaying the selection of semantics to the moment the fold is applied.
131 \subsection{Tagless-final embedding
}\label{sec:tagless-final_embedding
}
132 Tagless-final embedding overcomes the limitations of standard shallow embedding.
133 To upgrade to this embedding technique, the language constructs are changed from functions to type classes.
134 For our language this results in the following type class definition.
136 \begin{lstHaskellLhstex
}
140 \end{lstHaskellLhstex
}
142 Semantics become data types implementing these type classes, resulting in the following instance for the evaluator
\footnotemark.
144 In this case
\haskelllhstexinline{newtype
}s are used instead of regular
\haskelllhstexinline{data
} declarations.
145 A
\haskelllhstexinline{newtype
} is a special data type with a single constructor containing a single value only to which it is isomorphic.
146 It allows the programmer to define separate class instances that the instances of the isomorphic type without any overhead.
147 During compilation the constructor is completely removed
\citep[\citesection{4.2.3}]{peyton_jones_haskell_2003
}.
150 \begin{lstHaskellLhstex
}
151 newtype Eval_t = E_t Int
153 instance Expr_t Eval_t where
155 add_t (E_t e1) (E_t e2) = E_t (e1 + e2)
156 \end{lstHaskellLhstex
}
158 Adding constructs---e.g.\ subtraction---just results in an extra type class and corresponding instances.
160 \begin{lstHaskellLhstex
}
164 instance Sub_t Eval_t where
165 sub_t (E_t e1) (E_t e2) = E_t (e1 - e2)
166 \end{lstHaskellLhstex
}
168 Finally, adding semantics such as a printer over the language is achieved by providing a data type representing the semantics accompanied by instances for the language constructs.
170 \begin{lstHaskellLhstex
}
171 newtype Printer_t = P_t String
173 instance Expr_t Printer_t where
174 lit_t i = P_t (show i)
175 add_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "+" ++ e2 ++ ")")
177 instance Sub_t Printer_t where
178 sub_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "-" ++ e2 ++ ")")
179 \end{lstHaskellLhstex
}
181 \section{Lifting the interpretations
}%
182 Let us rethink the deeply embedded
\gls{DSL
} design.
183 Remember that in shallow embedding, the semantics are embedded in the language construct functions.
184 Obtaining extensibility both in constructs and semantics was accomplished by abstracting the semantics functions to type classes, making the constructs overloaded in the semantics.
185 In deep embedding, the constructs are embedded in the semantics functions instead.
186 So, let us apply the same technique, i.e.\ make the semantics overloaded in the language constructs by abstracting the semantics functions to type classes.
187 The same effect may be achieved when using similar techniques such as explicit dictionary passing or ML style modules.
188 In our language this results in the following type class.
190 \begin{lstHaskellLhstex
}
196 | Add_1 Expr_1 Expr_1
197 \end{lstHaskellLhstex
}
199 Implementing the semantics type class instances for the
\haskelllhstexinline{Expr_1
} data type is an elementary exercise.
200 By a copy-paste and some modifications, we come to the following implementation.
202 \begin{lstHaskellLhstex
}
203 instance Eval_1 Expr_1 where
205 eval_1 (Add_1 e1 e2) = eval_1 e1 + eval_1 e2
206 \end{lstHaskellLhstex
}
208 Subtraction can now be defined in a separate data type, leaving the original data type intact.
209 Instances for the additional semantics can now be implemented separately as instances of the type classes.
211 \begin{lstHaskellLhstex
}
212 data Sub_1 = Sub_1 Expr_1 Expr_1
214 instance Eval_1 Sub_1 where
215 eval_1 (Sub_1 e1 e2) = eval_1 e1 - eval_1 e2
216 \end{lstHaskellLhstex
}
218 \section{Existential data types
}%
220 The astute reader might have noticed that we have dissociated ourselves from the original data type.
221 It is only possible to create an expression with a subtraction on the top level.
222 The recursive knot is left untied and as a result,
\haskelllhstexinline{Sub_1
} can never be reached from an
\haskelllhstexinline{Expr_1
}.
224 Luckily, we can reconnect them by adding a special constructor to the
\haskelllhstexinline{Expr_1
} data type for housing extensions.
225 It contains an existentially quantified
\citep{mitchell_abstract_1988
} type with type class constraints
\citep{laufer_combining_1994,laufer_type_1996
} for all semantics type classes
\citep[\citesection{6.4.6}]{ghc_team_ghc_2021
} to allow it to house not just subtraction but any future extension.
227 \begin{lstHaskellLhstex
}
230 | Add_2 Expr_2 Expr_2
231 | forall x. Eval_2 x => Ext_2 x
232 \end{lstHaskellLhstex
}
234 The implementation of the extension case in the semantics type classes is in most cases just a matter of calling the function for the argument as can be seen in the semantics instances shown below.
236 \begin{lstHaskellLhstex
}
237 instance Eval_2 Expr_2 where
239 eval_2 (Add_2 e1 e2) = eval_2 e1 + eval_2 e2
240 eval_2 (Ext_2 x) = eval_2 x
241 \end{lstHaskellLhstex
}
243 Adding language construct extensions in different data types does mean that an extra
\haskelllhstexinline{Ext_2
} tag is introduced when using the extension.
244 This burden can be relieved by creating a smart constructor for it that automatically wraps the extension with the
\haskelllhstexinline{Ext_2
} constructor so that it is of the type of the main data type.
246 \begin{lstHaskellLhstex
}
247 sub_2 :: Expr_2 -> Expr_2 -> Expr_2
248 sub_2 e1 e2 = Ext_2 (Sub_2 e1 e2)
249 \end{lstHaskellLhstex
}
251 In our example this means that the programmer can write
\footnotemark:
253 Backticks are used to use functions or constructors in an infix fashion
\citep[\citesection{4.3.3}]{peyton_jones_haskell_2003
}.
255 \begin{lstHaskellLhstex
}
257 e2 = Lit_2
42 `sub_2` Lit_2
1
258 \end{lstHaskellLhstex
}
259 instead of having to write
260 \begin{lstHaskellLhstex
}
262 e2p = Ext_2 (Lit_2
42 `Sub_2` Lit_2
1)
263 \end{lstHaskellLhstex
}
265 \subsection{Unbraiding the semantics from the data
}
266 This approach does reveal a minor problem.
267 Namely, that all semantics type classes are braided into our datatypes via the
\haskelllhstexinline{Ext_2
} constructor.
268 Say if we add the printer again, the
\haskelllhstexinline{Ext_2
} constructor has to be modified to contain the printer type class constraint as well.
\footnote{Resulting in the following constructor:
\haskelllhstexinline{forall x.(Eval_2 x, Print_2 x) => Ext_2 x
}.
} %chktex 36
269 Thus, if we add semantics, the main data type's type class constraints in the
\haskelllhstexinline{Ext_2
} constructor need to be updated.
270 To avoid this, the type classes can be bundled in a type class alias or type class collection as follows.
272 \begin{lstHaskellLhstex
}
273 class (Eval_2 x, Print_2 x) => Semantics_2 x
277 | Add_2 Expr_2 Expr_2
278 | forall x. Semantics_2 x => Ext_2 x
279 \end{lstHaskellLhstex
}
281 The class alias removes the need for the programmer to visit the main data type when adding additional semantics.
282 Unfortunately, the compiler does need to visit the main data type again.
283 Some may argue that adding semantics happens less frequently than adding language constructs but in reality it means that we have to concede that the language is not as easily extensible in semantics as in language constructs.
284 More exotic type system extensions such as constraint kinds
\citep{bolingbroke_constraint_2011,yorgey_giving_2012
} can untangle the semantics from the data types by making the data types parametrised by the particular semantics.
285 However, by adding some boilerplate, even without this extension, the language constructs can be parametrised by the semantics by putting the semantics functions in a data type.
286 First the data types for the language constructs are parametrised by the type variable
\haskelllhstexinline{d
} as follows.
288 \begin{lstHaskellLhstex
}
291 | Add_3 (Expr_3 d) (Expr_3 d)
292 | forall x. Ext_3 (d x) x
294 data Sub_3 d = Sub_3 (Expr_3 d) (Expr_3 d)
295 \end{lstHaskellLhstex
}
297 The
\haskelllhstexinline{d
} type variable is inhabited by an explicit dictionary for the semantics, i.e.\ a witness to the class instance.
298 Therefore, for all semantics type classes, a data type is made that contains the semantics function for the given semantics.
299 This means that for
\haskelllhstexinline{Eval_3
}, a dictionary with the function
\haskelllhstexinline{EvalDict_3
} is defined, a type class
\haskelllhstexinline{HasEval_3
} for retrieving the function from the dictionary and an instance for
\haskelllhstexinline{HasEval_3
} for
\haskelllhstexinline{EvalDict_3
}.
301 \begin{lstHaskellLhstex
}
302 newtype EvalDict_3 v = EvalDict_3 (v -> Int)
304 class HasEval_3 d where
305 getEval_3 :: d v -> v -> Int
307 instance HasEval_3 EvalDict_3 where
308 getEval_3 (EvalDict_3 e) = e
309 \end{lstHaskellLhstex
}
311 The instances for the type classes change as well according to the change in the datatype.
312 Given that there is a
\haskelllhstexinline{HasEval_3
} instance for the witness type
\haskelllhstexinline{d
}, we can provide an implementation of
\haskelllhstexinline{Eval_3
} for
\haskelllhstexinline{Expr_3 d
}.
314 \begin{lstHaskellLhstex
}
315 instance HasEval_3 d => Eval_3 (Expr_3 d) where
317 eval_3 (Add_3 e1 e2) = eval_3 e1 + eval_3 e2
318 eval_3 (Ext_3 d x) = getEval_3 d x
320 instance HasEval_3 d => Eval_3 (Sub_3 d) where
321 eval_3 (Sub_3 e1 e2) = eval_3 e1 - eval_3 e2
322 \end{lstHaskellLhstex
}
324 Because the
\haskelllhstexinline{Ext_3
} constructor from
\haskelllhstexinline{Expr_3
} now contains a value of type
\haskelllhstexinline{d
}, the smart constructor for
\haskelllhstexinline{Sub_3
} must somehow come up with this value.
325 To achieve this, a type class is introduced that allows the generation of such a dictionary.
327 \begin{lstHaskellLhstex
}
330 \end{lstHaskellLhstex
}
332 This type class has individual instances for all semantics dictionaries, linking the class instance to the witness value.
333 I.e.\ if there is a type class instance known, a witness value can be conjured using the
\haskelllhstexinline{gdict
} function.
335 \begin{lstHaskellLhstex
}
336 instance Eval_3 v => GDict (EvalDict_3 v) where
337 gdict = EvalDict_3 eval_3
338 \end{lstHaskellLhstex
}
340 With these instances, the semantics function can be retrieved from the
\haskelllhstexinline{Ext_3
} constructor and in the smart constructors they can be generated as follows:
342 \begin{lstHaskellLhstex
}
343 sub_3 :: GDict (d (Sub_3 d)) => Expr_3 d -> Expr_3 d -> Expr_3 d
344 sub_3 e1 e2 = Ext_3 gdict (Sub_3 e1 e2)
345 \end{lstHaskellLhstex
}
347 Finally, we reached the end goal, orthogonal extension of both language constructs as shown by adding subtraction to the language and in language semantics.
348 Adding the printer can now be done without touching the original code as follows.
349 First the printer type class, dictionaries and instances for
\haskelllhstexinline{GDict
} are defined.
351 \begin{lstHaskellLhstex
}
352 class Print_3 v where
353 print_3 :: v -> String
355 newtype PrintDict_3 v = PrintDict_3 (v -> String)
357 class HasPrint_3 d where
358 getPrint_3 :: d v -> v -> String
360 instance HasPrint_3 PrintDict_3 where
361 getPrint_3 (PrintDict_3 e) = e
363 instance Print_3 v => GDict (PrintDict_3 v) where
364 gdict = PrintDict_3 print_3
365 \end{lstHaskellLhstex
}
367 Then the instances for
\haskelllhstexinline{Print_3
} of all the language constructs can be defined.
369 \begin{lstHaskellLhstex
}
370 instance HasPrint_3 d => Print_3 (Expr_3 d) where
371 print_3 (Lit_3 v) = show v
372 print_3 (Add_3 e1 e2) = "(" ++ print_3 e1 ++ "+" ++ print_3 e2 ++ ")"
373 print_3 (Ext_3 d x) = getPrint_3 d x
374 instance HasPrint_3 d => Print_3 (Sub_3 d) where
375 print_3 (Sub_3 e1 e2) = "(" ++ print_3 e1 ++ "-" ++ print_3 e2 ++ ")"
376 \end{lstHaskellLhstex
}
378 \section{Transformation semantics
}
379 Most semantics convert a term to some final representation and can be expressed just by functions on the cases.
380 However, the implementation of semantics such as transformation or optimisation may benefit from a so-called intentional analysis of the abstract syntax tree.
381 In shallow embedding, the implementation for these types of semantics is difficult because there is no tangible abstract syntax tree.
382 In off-the-shelf deep embedding this is effortless since the function can pattern match on the constructor or structures of constructors.
384 To demonstrate intensional analyses in classy deep embedding we write an optimiser that removes addition and subtraction by zero.
385 In classy deep embedding, adding new semantics means first adding a new type class housing the function including the machinery for the extension constructor.
387 \begin{lstHaskellLhstex
}
391 newtype OptDict_3 v = OptDict_3 (v -> v)
393 class HasOpt_3 d where
394 getOpt_3 :: d v -> v -> v
396 instance HasOpt_3 OptDict_3 where
397 getOpt_3 (OptDict_3 e) = e
399 instance Opt_3 v => GDict (OptDict_3 v) where
400 gdict = OptDict_3 opt_3
401 \end{lstHaskellLhstex
}
403 The implementation of the optimiser for the
\haskelllhstexinline{Expr_3
} data type is no complicated task.
404 The only interesting bit occurs in the
\haskelllhstexinline{Add_3
} constructor, where we pattern match on the optimised children to determine whether an addition with zero is performed.
405 If this is the case, the addition is removed.
407 \begin{lstHaskellLhstex
}
408 instance HasOpt_3 d => Opt_3 (Expr_3 d) where
409 opt_3 (Lit_3 v) = Lit_3 v
410 opt_3 (Add_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
411 (Lit_3
0, e2p ) -> e2p
412 (e1p, Lit_3
0) -> e1p
413 (e1p, e2p ) -> Add_3 e1p e2p
414 opt_3 (Ext_3 d x) = Ext_3 d (getOpt_3 d x)
415 \end{lstHaskellLhstex
}
417 Replicating this for the
\haskelllhstexinline{Opt_3
} instance of
\haskelllhstexinline{Sub_3
} seems a clear-cut task at first glance.
419 \begin{lstHaskellLhstex
}
420 instance HasOpt_3 d => Opt_3 (Sub_3 d) where
421 opt_3 (Sub_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
422 (e1p, Lit_3
0) -> e1p
423 (e1p, e2p ) -> Sub_3 e1p e2p
424 \end{lstHaskellLhstex
}
426 Unsurprisingly, this code is rejected by the compiler.
427 When a literal zero is matched as the right-hand side of a subtraction, the left-hand side of type
\haskelllhstexinline{Expr_3
} is returned.
428 However, the type signature of the function dictates that it should be of type
\haskelllhstexinline{Sub_3
}.
429 To overcome this problem we add a convolution constructor.
431 \subsection{Convolution
}
432 Adding a loopback case or convolution constructor to
\haskelllhstexinline{Sub_3
} allows the removal of the
\haskelllhstexinline{Sub_3
} constructor while remaining the
\haskelllhstexinline{Sub_3
} type.
433 It should be noted that a loopback case is
\emph{only
} required if the transformation actually removes tags.
434 This changes the
\haskelllhstexinline{Sub_3
} data type as follows.
436 \begin{lstHaskellLhstex
}
438 = Sub_4 (Expr_4 d) (Expr_4 d)
439 | SubLoop_4 (Expr_4 d)
441 instance HasEval_4 d => Eval_4 (Sub_4 d) where
442 eval_4 (Sub_4 e1 e2) = eval_4 e1 - eval_4 e2
443 eval_4 (SubLoop_4 e1) = eval_4 e1
444 \end{lstHaskellLhstex
}
446 With this loopback case in the toolbox, the following
\haskelllhstexinline{Sub
} instance optimises away subtraction with zero literals.
448 \begin{lstHaskellLhstex
}
449 instance HasOpt_4 d => Opt_4 (Sub_4 d) where
450 opt_4 (Sub_4 e1 e2) = case (opt_4 e1, opt_4 e2) of
451 (e1p, Lit_4
0) -> SubLoop_4 e1p
452 (e1p, e2p ) -> Sub_4 e1p e2p
453 opt_4 (SubLoop_4 e) = SubLoop_4 (opt_4 e)
454 \end{lstHaskellLhstex
}
456 \subsection{Pattern matching
}
457 Pattern matching within datatypes and from an extension to the main data type works out of the box.
458 Cross-extensional pattern matching on the other hand---matching on a particular extension---is something that requires a bit of extra care.
459 Take for example negation propagation and double negation elimination.
460 Pattern matching on values with an existential type is not possible without leveraging dynamic typing
\citep{abadi_dynamic_1991,baars_typing_2002
}.
461 To enable dynamic typing support, the
\haskelllhstexinline{Typeable
} type class as provided by
\haskelllhstexinline{Data.Dynamic
} \citep{ghc_team_datadynamic_2021
} is added to the list of constraints in all places where we need to pattern match across extensions.
462 As a result, the
\haskelllhstexinline{Typeable
} type class constraints are added to the quantified type variable
\haskelllhstexinline{x
} of the
\haskelllhstexinline{Ext_4
} constructor and to
\haskelllhstexinline{d
}s in the smart constructors.
464 \begin{lstHaskellLhstex
}
467 | Add_4 (Expr_4 d) (Expr_4 d)
468 | forall x. Typeable x => Ext_4 (d x) x
469 \end{lstHaskellLhstex
}
471 First let us add negation to the language by defining a datatype representing it.
472 Negation elimination requires the removal of negation constructors, so a convolution constructor is defined as well.
474 \begin{lstHaskellLhstex
}
477 | NegLoop_4 (Expr_4 d)
479 neg_4 :: (Typeable d, GDict (d (Neg_4 d))) => Expr_4 d -> Expr_4 d
480 neg_4 e = Ext_4 gdict (Neg_4 e)
481 \end{lstHaskellLhstex
}
483 The evaluation and printer instances for the
\haskelllhstexinline{Neg_4
} datatype are defined as follows.
485 \begin{lstHaskellLhstex
}
486 instance HasEval_4 d => Eval_4 (Neg_4 d) where
487 eval_4 (Neg_4 e) = negate (eval_4 e)
488 eval_4 (NegLoop_4 e) = eval_4 e
490 instance HasPrint_4 d => Print_4 (Neg_4 d) where
491 print_4 (Neg_4 e) = "(~" ++ print_4 e ++ ")"
492 print_4 (NegLoop_4 e) = print_4 e
493 \end{lstHaskellLhstex
}
495 The
\haskelllhstexinline{Opt_4
} instance contains the interesting bit.
496 If the sub expression of a negation is an addition, negation is propagated downwards.
497 If the sub expression is again a negation, something that can only be found out by a dynamic pattern match, it is replaced by a
\haskelllhstexinline{NegLoop_4
} constructor.
499 \begin{lstHaskellLhstex
}
500 instance (Typeable d, GDict (d (Neg_4 d)), HasOpt_4 d) => Opt_4 (Neg_4 d) where
501 opt_4 (Neg_4 (Add_4 e1 e2))
502 = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2)))
503 opt_4 (Neg_4 (Ext_4 d x))
504 = case fromDynamic (toDyn (getOpt_4 d x)) of
505 Just (Neg_4 e) -> NegLoop_4 e
506 _ -> Neg_4 (Ext_4 d (getOpt_4 d x))
507 opt_4 (Neg_4 e) = Neg_4 (opt_4 e)
508 opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e)
509 \end{lstHaskellLhstex
}
511 Loopback cases do make cross-extensional pattern matching less modular in general.
512 For example,
\haskelllhstexinline{Ext_4 d (SubLoop_4 (Lit_4
0))
} is equivalent to
\haskelllhstexinline{Lit_4
0} in the optimisation semantics and would require an extra pattern match.
513 Fortunately, this problem can be mitigated---if required---by just introducing an additional optimisation semantics that removes loopback cases.
514 Luckily, one does not need to resort to these arguably blunt matters often.
515 Dependent language functionality often does not need to span extensions, i.e.\ it is possible to group them in the same data type.
517 \subsection{Chaining semantics
}
518 Now that the data types are parametrised by the semantics a final problem needs to be overcome.
519 The data type is parametrised by the semantics, thus, using multiple semantics, such as evaluation after optimising is not straightforwardly possible.
520 Luckily, a solution is readily at hand: introduce an ad-hoc combination semantics.
522 \begin{lstHaskellLhstex
}
523 data OptPrintDict_4 v = OPD_4 (OptDict_4 v) (PrintDict_4 v)
525 instance HasOpt_4 OptPrintDict_4 where
526 getOpt_4 (OPD_4 v _) = getOpt_4 v
527 instance HasPrint_4 OptPrintDict_4 where
528 getPrint_4 (OPD_4 _ v) = getPrint_4 v
530 instance (Opt_4 v, Print_4 v) => GDict (OptPrintDict_4 v) where
531 gdict = OPD_4 gdict gdict
532 \end{lstHaskellLhstex
}
534 And this allows us to write
\haskelllhstexinline{print_4 (opt_4 e1)
} resulting in
\verb|"((~
42)+(~
38))"| when
\haskelllhstexinline{e1
} represents $(
\sim(
42+
38))-
0$ and is thus defined as follows.
536 \begin{lstHaskellLhstex
}
537 e1 :: Expr_4 OptPrintDict_4
538 e1 = neg_4 (Lit_4
42 `Add_4` Lit_4
38) `sub_4` Lit_4
0
539 \end{lstHaskellLhstex
}
541 When using classy deep embedding to the fullest, the ability of the compiler to infer very general types expires.
542 As a consequence, defining reuseable expressions that are overloaded in their semantics requires quite some type class constraints that cannot be inferred by the compiler (yet) if they use many extensions.
543 Solving this remains future work.
544 For example, the expression $
\sim(
42-
38)+
1$ has to be defined as:
546 \begin{lstHaskellLhstex
}
547 e3 :: (Typeable d, GDict (d (Neg_4 d)), GDict (d (Sub_4 d))) => Expr_4 d
548 e3 = neg_4 (Lit_4
42 `sub_4` Lit_4
38) `Add_4` Lit_4
1
549 \end{lstHaskellLhstex
}
551 \section{Generalised algebraic data types
}%
552 \Glspl{GADT
} are enriched data types that allow the type instantiation of the constructor to be explicitly defined
\citep{cheney_first-class_2003,hinze_fun_2003
}.
553 Leveraging
\glspl{GADT
}, deeply embedded
\glspl{DSL
} can be made statically type safe even when different value types are supported.
554 Even when
\glspl{GADT
} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types
\citep[\citesection{2.2}]{cheney_lightweight_2002
}.
555 Where some solutions to the expression problem do not easily generalise to
\glspl{GADT
} (see
\cref{sec:cde:related
}), classy deep embedding does.
556 Generalising the data structure of our
\gls{DSL
} is fairly straightforward and to spice things up a bit, we add an equality and boolean negation language construct.
557 To make the existing
\gls{DSL
} constructs more general, we relax the types of those constructors.
558 For example, operations on integers now work on all numerals instead.
559 Moreover, the
\haskelllhstexinline{Lit_g
} constructor can be used to lift values of any type to the
\gls{DSL
} domain as long as they have a
\haskelllhstexinline{Show
} instance, required for the printer.
560 Since some optimisations on
\haskelllhstexinline{Not_g
} remove constructors and therefore use cross-extensional pattern matches,
\haskelllhstexinline{Typeable
} constraints are added to
\haskelllhstexinline{a
}.
561 Furthermore, because the optimisations for
\haskelllhstexinline{Add_g
} and
\haskelllhstexinline{Sub_g
} are now more general, they do not only work for
\haskelllhstexinline{Int
}s but for any type with a
\haskelllhstexinline{Num
} instance, the
\haskelllhstexinline{Eq
} constraint is added to these constructors as well.
562 Finally, not to repeat ourselves too much, we only show the parts that substantially changed.
563 The omitted definitions and implementation can be found in
\cref{sec:cde:appendix
}.
565 \begin{lstHaskellLhstex
}
566 data Expr_g d a where
567 Lit_g :: Show a => a -> Expr_g d a
568 Add_g :: (Eq a, Num a) => Expr_g d a -> Expr_g d a -> Expr_g d a
569 Ext_g :: Typeable x => d x -> x a -> Expr_g d a
571 Neg_g :: (Typeable a, Num a) => Expr_g d a -> Neg_g d a
572 NegLoop_g :: Expr_g d a -> Neg_g d a
574 Not_g :: Expr_g d Bool -> Not_g d Bool
575 NotLoop_g :: Expr_g d a -> Not_g d a
576 \end{lstHaskellLhstex
}
578 The smart constructors for the language extensions inherit the class constraints of their data types and include a
\haskelllhstexinline{Typeable
} constraint on the
\haskelllhstexinline{d
} type variable for it to be useable in the
\haskelllhstexinline{Ext_g
} constructor as can be seen in the smart constructor for
\haskelllhstexinline{Neg_g
}:
580 \begin{lstHaskellLhstex
}
581 neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) =>
582 Expr_g d a -> Expr_g d a
583 neg_g e = Ext_g gdict (Neg_g e)
585 not_g :: (Typeable d, GDict (d (Not_g d))) =>
586 Expr_g d Bool -> Expr_g d Bool
587 not_g e = Ext_g gdict (Not_g e)
588 \end{lstHaskellLhstex
}
590 Upgrading the semantics type classes to support
\glspl{GADT
} is done by an easy textual search and replace.
591 All occurrences of
\haskelllhstexinline{v
} are now parametrised by type variable
\haskelllhstexinline{a
}:
593 \begin{lstHaskellLhstex
}
596 class Print_g v where
597 print_g :: v a -> String
600 \end{lstHaskellLhstex
}
602 Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
603 The introduced type variable
\haskelllhstexinline{a
} is not an argument to the type class, so it should not be an argument to the dictionary data type.
604 To represent this type class function, a rank-
2 polymorphic function is needed
\citep[\citesection{6.4.15}]{ghc_team_ghc_2021
}\citep{odersky_putting_1996
}.
605 Concretely, for the evaluator this results in the following definitions:
607 \begin{lstHaskellLhstex
}
608 newtype EvalDict_g v = EvalDict_g (forall a. v a -> a)
609 class HasEval_g d where
610 getEval_g :: d v -> v a -> a
611 instance HasEval_g EvalDict_g where
612 getEval_g (EvalDict_g e) = e
613 \end{lstHaskellLhstex
}
615 The
\haskelllhstexinline{GDict
} type class is general enough, so the instances can remain the same.
616 The
\haskelllhstexinline{Eval_g
} instance of
\haskelllhstexinline{GDict
} looks as follows:
618 \begin{lstHaskellLhstex
}
619 instance Eval_g v => GDict (EvalDict_g v) where
620 gdict = EvalDict_g eval_g
621 \end{lstHaskellLhstex
}
623 Finally, the implementations for the instances can be ported without complication show using the optimisation instance of
\haskelllhstexinline{Not_g
}:
625 \begin{lstHaskellLhstex
}
626 instance (Typeable d, GDict (d (Not_g d)), HasOpt_g d) => Opt_g (Not_g d) where
627 opt_g (Not_g (Ext_g d x))
628 = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of
629 Just (Not_g e) -> NotLoop_g e
630 _ -> Not_g (Ext_g d (getOpt_g d x))
631 opt_g (Not_g e) = Not_g (opt_g e)
632 opt_g (NotLoop_g e) = NotLoop_g (opt_g e)
633 \end{lstHaskellLhstex
}
635 \section{Related work
}%
636 \label{sec:cde:related
}
638 Embedded
\gls{DSL
} techniques in functional languages have been a topic of research for many years, thus we do not claim a complete overview of related work.
640 Clearly, classy deep embedding bears most similarity to the
\emph{Datatypes \`a la Carte
} \citep{swierstra_data_2008
}.
641 In
\citeauthor{swierstra_data_2008
}'s approach, semantics are lifted to type classes similarly to classy deep embedding.
642 Each language construct is their own datatype parametrised by a type parameter.
643 This parameter contains some type level representation of language constructs that are in use.
644 In classy deep embedding, extensions only have to be enumerated at the type level when the term is required to be overloaded, in all other cases they are captured in the extension case.
645 Because all the constructs are expressed in the type system, nifty type system tricks need to be employed to convince the compiler that everything is type safe and the class constraints can be solved.
646 Furthermore, it requires some boilerplate code such as functor instances for the data types.
647 In return, pattern matching is easier and does not require dynamic typing.
648 Classy deep embedding only strains the programmer with writing the extension case for the main data type and the occasional loopback constructor.
650 \Citet{loh_open_2006
} proposed a language extension that allows open data types and open functions, i.e.\ functions and data types that can be extended with more cases later on.
651 They hinted at the possibility of using type classes for open functions but had serious concerns that pattern matching would be crippled because constructors are becoming types, thus ultimately becoming impossible to type.
652 In contrast, this chapter shows that pattern matching is easily attainable---albeit using dynamic types---and that the terms can be typed without complicated type system extensions.
654 A technique similar to classy deep embedding was proposed by
\citet{najd_trees_2017
} to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form.
655 For example to decorate the abstract syntax tree of a compiler differently for each phase of the compiler.
656 They propose to add an extension descriptor as a type variable to a data type and a type family that can be used to decorate constructors with extra information and add additional constructors to the data type using an extension constructor.
657 Classy deep embedding works similarly but uses existentially quantified type variables to describe possible extensions instead of type variables and type families.
658 In classy deep embedding, the extensions do not need to be encoded in the type system and less boilerplate is required.
659 Furthermore, pattern matching on extensions becomes a bit more complicated but in return it allows for multiple extensions to be added orthogonally and avoids the necessity for type system extensions.
661 Tagless-final embedding is the shallowly embedded counterpart of classy deep embedding and was invented for the same purpose; overcoming the issues with standard shallow embedding
\citep{carette_finally_2009
}.
662 Classy deep embedding was organically grown from observing the evolution of tagless-final embedding.
663 The main difference between tagless-final embedding and classy deep embedding---and in general between shallow and deep embedding---is that intensional analyses of the abstract syntax tree is more difficult because there is no tangible abstract syntax tree data structure.
664 In classy deep embedding, it is possible to define transformations even across extensions.
665 Furthermore, in classy deep embedding, defining (mutual) dependent interpretations is automatically supported whereas in tagless-final embedding this requires some amount of code duplication
\citep{sun_compositional_2022
}.
667 Hybrid approaches between deep and shallow embedding exist as well.
668 For example,
\citet{svenningsson_combining_2013
} show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well.
669 Classy deep embedding differs from the hybrid approaches in the sense that it does not require the language extensions to be expressible in the core language.
671 \subsection{Comparison
}
672 No
\gls{DSL
} embedding technique is the silver bullet, there is no way of perfectly satisfying all requirements programmers have.
673 \Citet{sun_compositional_2022
} provided a thorough comparison of embedding techniques including more axes than just the two stated in the expression problem.
675 \Cref{tbl:dsl_comparison_brief
} shows a variant of their comparison table.
676 The first two rows describe the two axes of the original expression problem and the third row describes the added axis of modular dependency handling as stated by
\citeauthor{sun_compositional_2022
}.
677 The
\emph{poly.
} style of embedding---including tagless-final---falls short of this requirement.
679 Intensional analysis is an umbrella term for pattern matching and transformations.
680 In shallow embedding, intensional analysis is more complex and requires stateful views describing context, but it is possible to implement though.
682 Simple type system describes the whether it is possible to encode this embedding technique without many type system extensions.
683 In classy deep embedding, there is either a bit more scaffolding and boilerplate required or advanced type system extensions need to be used.
685 Little boilerplate denotes the amount of scaffolding and boilerplate required.
686 For example, hybrid embedding requires a transcoding step between the deep syntax and the shallow core language.
689 \begin{threeparttable
}[b
]
691 \caption{Comparison of embedding techniques, extended from
\citet[\citesection{3.6}]{sun_compositional_2022
}.
}%
692 \label{tbl:dsl_comparison_brief
}
693 \begin{tabular
}{llllllll
}
695 & Shallow & Deep & Hybrid
696 & Poly. & Comp. & \`a la
699 Extend constructs &
\CIRCLE{} &
\Circle{} &
\LEFTcircle{}\tnote{1}
700 &
\CIRCLE{} &
\CIRCLE{} &
\CIRCLE{}
702 Extend views &
\Circle{} &
\CIRCLE{} &
\CIRCLE{}
703 &
\CIRCLE{} &
\CIRCLE{} &
\CIRCLE{}
705 Modular dependencies &
\Circle{} &
\CIRCLE{} &
\CIRCLE{}
706 &
\Circle{} &
\CIRCLE{} &
\CIRCLE{}
708 Intensional analysis &
\LEFTcircle{}\tnote{2} &
\CIRCLE{} &
\CIRCLE{}
709 &
\LEFTcircle{}\tnote{2} &
\LEFTcircle{}\tnote{2} &
\CIRCLE{}
710 &
\CIRCLE{}\tnote{3}\\
711 Simple type system &
\CIRCLE{} &
\CIRCLE{} &
\Circle{}
712 &
\CIRCLE{} &
\CIRCLE{} &
\Circle{}
713 &
\textcolor{gray
}{\CIRCLE{}}\tnote{4}\\
714 Little boilerplate &
\CIRCLE{} &
\CIRCLE{} &
\Circle{}
715 &
\CIRCLE{} &
\CIRCLE{} &
\Circle{}
716 &
\textcolor{gray
}{\CIRCLE{}}\tnote{4}\\
720 \item [1] Only if the extension is expressible in the core language.
721 \item [2] Requires ingenuity and are sometimes awkward to write.
722 \item [3] Cross-extensional pattern matching requires
\emph{safe
} dynamic typing.
723 \item [4] Either a simple type system or little boilerplate.
728 \section{Conclusion
}%
729 Classy deep embedding is a novel organically grown embedding technique that alleviates deep embedding from the extensibility problem in most cases.
731 By abstracting the semantics functions to type classes they become overloaded in the language constructs.
732 Thus, making it possible to add new language constructs in a separate type.
733 These extensions are brought together in a special extension constructor residing in the main data type.
734 This extension case is overloaded by the language construct using a data type containing the class dictionary.
735 As a result, orthogonal extension is possible for language constructs and semantics using only little syntactic overhead or type annotations.
736 The basic technique only requires---well established through history and relatively standard---existential data types.
737 However, if needed, the technique generalises to
\glspl{GADT
} as well, adding rank-
2 types to the list of type system requirements as well.
738 Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
740 Defining reuseable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around these issues remains future work.
741 \Cref{sec:classy_reprise
} shows how the boilerplate can be minimised using advanced type system extensions.
743 \section*
{Acknowledgements
}
744 This research is partly funded by the Royal Netherlands Navy.
745 Furthermore, I would like to thank Pieter and Rinus for the fruitful discussions, Ralf for inspiring me to write a functional pearl, and the anonymous reviewers for their valuable and honest comments.
747 \begin{subappendices
}
748 \section{Reprise: reducing boilerplate
}%
749 \label{sec:classy_reprise
}
750 One of the unique selling points of this novel
\gls{DSL
} embedding technique is that it, in its basic form, does not require advanced type system extensions nor a lot of boilerplate.
751 However, generalising the technique to
\glspl{GADT
} arguably unleashes a cesspool of
\emph{unsafe
} compiler extensions.
752 If we are willing to work with extensions, almost all the boilerplate can be inferred or generated.
754 In classy deep embedding, the
\gls{DSL
} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
755 When using multiple interpretations, these need to be bundled in a data type.
756 Using the
\gls{GHC
}'s
\GHCmod{ConstraintKind
} extension, we can make these witnesses explicit, tying into
\gls{HASKELL
}'s type system immediately.
757 Furthermore, this constraint does not necessarily have to be a single constraint, after enabling
\GHCmod{DataKinds
} and
\GHCmod{TypeOperators
}, we can encode lists of witnesses instead
\citep{yorgey_giving_2012
}.
758 The data type for this list of witnesses is
\haskelllhstexinline{Record
} as shown in
\cref{lst_cbde:record_type
}.
759 This
\gls{GADT
} is parametrised by two type variables.
760 The first type variable (
\haskelllhstexinline{dt
}) is the type or type constructor on which the constraints can be applied and the second type variable (
\haskelllhstexinline{clist
}) is the list of constraints constructors itself.
761 This means that when
\haskelllhstexinline{Cons
} is pattern matched, the overloading of the type class constraint for
\haskelllhstexinline{c dt
} can be solved by the compiler.
762 \GHCmod{KindSignatures
} is used to force the kinds of the type parameters and the kind of
\haskelllhstexinline{dt
} is polymorphic (
\GHCmod{PolyKinds
}) so that the
\haskelllhstexinline{Record
} data type can be used for
\glspl{DSL
} using type classes but also type constructor classes (e.g.\ when using
\glspl{GADT
}).
764 \begin{lstHaskellLhstex
}[label=
{lst_cbde:record_type
},caption=
{Data type for a list of constraints.
}]
765 data Record (dt :: k) (clist ::
[k -> Constraint
]) where
767 Cons :: c dt => Record dt cs -> Record dt (c ': cs)
768 \end{lstHaskellLhstex
}
770 To incorporate this type in the
\haskelllhstexinline{Expr
} type, the
\haskelllhstexinline{Ext
} constructor changes from containing a single witness dictionary to a
\haskelllhstexinline{Record
} type containing all the required dictionaries.
772 \begin{lstHaskellLhstex
}[caption=
{Main data type with extension constructor.
}]
775 | Add (Expr c) (Expr c)
777 \end{lstHaskellLhstex
}
779 Furthermore, we define a type class (
\haskelllhstexinline{In
}) that allows us to extract explicit dictionaries
\haskelllhstexinline{Dict
} from these records if the constraint can is present in the list.
780 Since the constraints become available as soon as the
\haskelllhstexinline{Cons
} constructor is matched, the implementation is a type-level list traversal.
782 \begin{lstHaskellLhstex
}[caption=
{Membership functions for constraints.
}]
783 class c `In` cs where
784 project :: Record dt cs -> Dict (c dt)
785 instance
{-# OVERLAPPING #-
} c `In` (c ': cs) where
786 project (Cons _) = Dict
787 instance
{-# OVERLAPPING #-
} c `In` cs => c `In` (b ': cs) where
788 project (Cons xs) = project xs
789 \end{lstHaskellLhstex
}
791 The final scaffolding is a multi-parameter type class
\haskelllhstexinline{CreateRecord
} (requiring the
\GHCmod{MultiParamTypeclasses
} and
\GHCmod{FlexibleInstances
} extension) to create these
\haskelllhstexinline{Record
} witnesses automatically.
792 This type class creates a record structure cons by cons if and only if all type class constraints are available in the list of constraints.
793 It is not required to provide instances for this for specific records or type classes, the two instances describe all the required constraints.
795 \begin{lstHaskellLhstex
}[caption=
{Functions for creating the witness records.
}]
796 class CreateRecord dt c where
797 createRecord :: Record dt c
798 instance CreateRecord d '
[] where
800 instance (c (d c0), CreateRecord (d c0) cs) =>
801 CreateRecord (d c0) (c ': cs) where
802 createRecord = Cons createRecord
803 \end{lstHaskellLhstex
}
805 The class constraints for the interpretation instances can now be greatly simplified, as shown in the evaluation instance for
\haskelllhstexinline{Expr
}.
806 The implementation remains the same, only that for the extension case, a trick needs to be applied to convince the compiler of the correct instances.
807 Using
\haskelllhstexinline{`In`
}'s
\haskelllhstexinline{project
} function, a dictionary can be brought into scope.
808 This dictionary can then subsequently be used to apply the type class function on the extension using the
\haskelllhstexinline{withDict
} function from the
\haskelllhstexinline{Data.Constraint
} library.
\footnote{\haskelllhstexinline{withDict :: Dict c -> (c => r) -> r
}}
809 The
\GHCmod{ScopedTypeVariables
} extension is used to make sure the existentially quantified type variable for the extension is matched to the type of the dictionary.
810 Furthermore, because the class constraint is not smaller than the instance head,
\GHCmod{UndecidableInstances
} should be enabled.
812 \begin{lstHaskellLhstex
}
816 instance Eval `In` s => Eval (Expr s) where
818 eval (Add l r) = eval l + eval r
819 eval (Ext r (e :: x)) = withDict (project r :: Dict (Eval x)) eval e
820 \end{lstHaskellLhstex
}
822 Smart constructors need to be adapted as well, as can be seen from the smart constructor
\haskelllhstexinline{subst
}.
823 Instead of a
\haskelllhstexinline{GDict
} class constraint, a
\haskelllhstexinline{CreateRecord
} class constraint needs to be added.
825 \begin{lstHaskellLhstex
}
826 subst :: (Typeable c, CreateRecord (Subt c) c)
827 => Expr c -> Expr c -> Expr c
828 subst l r = Ext createRecord (l `Subt` r)
829 \end{lstHaskellLhstex
}
831 Finally, defining terms in the language can be done immediately if the interpretations are known.
832 For example, if we want to print and/or optimise the term $
\displaystyle ~(~(
42+(
38-
4)))$, we can define it as follows:
834 \begin{lstHaskellLhstex
}
835 e0 :: Expr '
[Print,Opt
]
836 e0 = neg (neg (Lit
42 `Add` (Lit
38 `subt` Lit
4)))
837 \end{lstHaskellLhstex
}
839 It is also possible to define terms in the
\gls{DSL
} as being overloaded in the interpretation.
840 This does require enumerating all the
\haskelllhstexinline{CreateRecord
} type classes for every extension similarly as was required for
\haskelllhstexinline{GDict
}.
841 At the call site, the concrete list of constraints must be known.
843 \begin{lstHaskellLhstex
}
844 e1 :: (Typeable c, CreateRecord (Neg c) c, CreateRecord (Subst c) c)
846 e1 = neg (neg (Lit
42 `Add` (Lit
38 `subt` Lit
4)))
847 \end{lstHaskellLhstex
}
849 Finally, using the
\GHCmod{TypeFamilies
} extension, type families can be created for bundling
\haskelllhstexinline{`In`
} constraints (
\haskelllhstexinline{UsingExt
}) and
\haskelllhstexinline{CreateRecord
} constraints
\mbox{(
\haskelllhstexinline{DependsOn
})
}, making the syntax even more descriptive.
850 E.g.\
\mbox{\haskelllhstexinline{UsingExt '
[A, B, C
] c
}} expands to
\newline\haskelllhstexinline{(CreateRecord (A c) c, CreateRecord (B c) c, CreateRecord (C c) c)
}.
851 \hspace{-
1.42284pt
} Similarly,
\haskelllhstexinline{DependsOn '
[A, B, C
] s
} expands to
\haskelllhstexinline{(A `In` s, B `In` s, C `In` s)
}.
853 \begin{lstHaskellLhstex
}
854 type family UsingExt cs c :: Constraint where
856 UsingExt (d ': cs) c = (CreateRecord (d c) c, UsingExt cs c)
858 type family DependsOn cs c :: Constraint where
860 DependsOn (d ': cs) c = (d `In` c, DependsOn cs c)
861 \end{lstHaskellLhstex
}
863 Defining the previous expression can now be done with the following shortened type that describes the semantics better:
865 \begin{lstHaskellLhstex
}
866 e1 :: (Typeable c, UsingExt '
[Neg, Subst
]) => Expr c
867 \end{lstHaskellLhstex
}
869 Giving an instance for
\haskelllhstexinline{Interp
} for
\haskelllhstexinline{DataType
} that uses the extensions
\haskelllhstexinline{e_1, e2, ...
} and depends on interpretations
\haskelllhstexinline{i_1,i_2, ...
} is done as follows:
871 \begin{lstHaskellLhstex
}
872 instance ( UsingExt '
[e_1, e_2, ...
] s, DependsOn '
[i_1, i_2, ...
] s)
873 => Interp (DataType s) where
875 \end{lstHaskellLhstex
}
877 With these enhancements, there is hardly any boilerplate required to use classy deep embedding.
878 The
\haskelllhstexinline{Record
} data type; the
\haskelllhstexinline{CreateRecord
} type class; and the
\haskelllhstexinline{UsingExt
} and
\haskelllhstexinline{DependsOn
} type families can be provided as a library only requiring the programmer to create the extension constructors with their respective implementations and smart constructors for language construct extensions.
879 The source code for this extension can be found here:
\url{https://gitlab.com/mlubbers/classydeepembedding
}.
\footnote{Lubbers, M. (
2022): Library and examples for enhanced classy deep embedding.\ Zenodo.\
\href{https://doi.org/
10.5281/zenodo
.7277498}{10.5281/zenodo
.7277498}.
}
880 It contains examples for expressions, expressions using
\glspl{GADT
}, detection of sharing in expressions (modelled after
\citet{kiselyov_implementing_2011
}), a
\gls{GADT
} version of sharing detection, and a region
\gls{DSL
} (modelled after
\citet{sun_compositional_2022
}).
882 \section{Data types and definitions
}%
883 \label{sec:cde:appendix
}
884 This appendix collects all definitions omitted for brevity.
886 \lstset{basicstyle=
\tt\footnotesize}
887 \begin{lstHaskellLhstex
}[caption=
{Data type definitions.
}]
889 Sub_g :: (Eq a, Num a) => Expr_g d a -> Expr_g d a -> Sub_g d a
890 SubLoop_g :: Expr_g d a -> Sub_g d a
893 Eq_g :: (Typeable a, Eq a) => Expr_g d a -> Expr_g d a -> Eq_g d Bool
894 EqLoop_g :: Expr_g d a -> Eq_g d a
895 \end{lstHaskellLhstex
}
897 \begin{lstHaskellLhstex
}[caption=
{Smart constructors.
}]
898 sub_g :: (Typeable d, GDict (d (Sub_g d)), Eq a, Num a) =>
899 Expr_g d a -> Expr_g d a -> Expr_g d a
900 sub_g e1 e2 = Ext_g gdict (Sub_g e1 e2)
902 eq_g :: (Typeable d, GDict (d (Eq_g d)), Eq a, Typeable a) =>
903 Expr_g d a -> Expr_g d a -> Expr_g d Bool
904 eq_g e1 e2 = Ext_g gdict (Eq_g e1 e2)
905 \end{lstHaskellLhstex
}
907 \begin{lstHaskellLhstex
}[caption=
{Semantics classes and data types.
}]
908 newtype PrintDict_g v = PrintDict_g (forall a.v a -> String)
910 class HasPrint_g d where
911 getPrint_g :: d v -> v a -> String
913 instance HasPrint_g PrintDict_g where
914 getPrint_g (PrintDict_g e) = e
916 newtype OptDict_g v = OptDict_g (forall a.v a -> v a)
918 class HasOpt_g d where
919 getOpt_g :: d v -> v a -> v a
921 instance HasOpt_g OptDict_g where
922 getOpt_g (OptDict_g e) = e
923 \end{lstHaskellLhstex
}
925 \begin{lstHaskellLhstex
}[caption=
{{\tt GDict
} instances.
}]
926 instance Print_g v => GDict (PrintDict_g v) where
927 gdict = PrintDict_g print_g
928 instance Opt_g v => GDict (OptDict_g v) where
929 gdict = OptDict_g opt_g
930 \end{lstHaskellLhstex
}
932 \begin{lstHaskellLhstex
}[caption=
{Evaluator instances.
}]
933 instance HasEval_g d => Eval_g (Expr_g d) where
935 eval_g (Add_g e1 e2) = eval_g e1 + eval_g e2
936 eval_g (Ext_g d x) = getEval_g d x
938 instance HasEval_g d => Eval_g (Sub_g d) where
939 eval_g (Sub_g e1 e2) = eval_g e1 - eval_g e2
940 eval_g (SubLoop_g e) = eval_g e
942 instance HasEval_g d => Eval_g (Neg_g d) where
943 eval_g (Neg_g e) = negate (eval_g e)
944 eval_g (NegLoop_g e) = eval_g e
946 instance HasEval_g d => Eval_g (Eq_g d) where
947 eval_g (Eq_g e1 e2) = eval_g e1 == eval_g e2
948 eval_g (EqLoop_g e) = eval_g e
950 instance HasEval_g d => Eval_g (Not_g d) where
951 eval_g (Not_g e) = not (eval_g e)
952 eval_g (NotLoop_g e) = eval_g e
953 \end{lstHaskellLhstex
}
955 \begin{lstHaskellLhstex
}[caption=
{Printer instances.
}]
956 instance HasPrint_g d => Print_g (Expr_g d) where
957 print_g (Lit_g v) = show v
958 print_g (Add_g e1 e2) = "(" ++ print_g e1 ++ "+" ++ print_g e2 ++ ")"
959 print_g (Ext_g d x) = getPrint_g d x
961 instance HasPrint_g d => Print_g (Sub_g d) where
962 print_g (Sub_g e1 e2) = "(" ++ print_g e1 ++ "-" ++ print_g e2 ++ ")"
963 print_g (SubLoop_g e) = print_g e
965 instance HasPrint_g d => Print_g (Neg_g d) where
966 print_g (Neg_g e) = "(negate " ++ print_g e ++ ")"
967 print_g (NegLoop_g e) = print_g e
969 instance HasPrint_g d => Print_g (Eq_g d) where
970 print_g (Eq_g e1 e2) = "(" ++ print_g e1 ++ "==" ++ print_g e2 ++ ")"
971 print_g (EqLoop_g e) = print_g e
973 instance HasPrint_g d => Print_g (Not_g d) where
974 print_g (Not_g e) = "(not " ++ print_g e ++ ")"
975 print_g (NotLoop_g e) = print_g e
976 \end{lstHaskellLhstex
}
978 \begin{lstHaskellLhstex
}[caption=
{Optimisation instances.
}]
979 instance HasOpt_g d => Opt_g (Expr_g d) where
980 opt_g (Lit_g v) = Lit_g v
981 opt_g (Add_g e1 e2) = case (opt_g e1, opt_g e2) of
982 (Lit_g
0, e2p ) -> e2p
983 (e1p, Lit_g
0) -> e1p
984 (e1p, e2p ) -> Add_g e1p e2p
985 opt_g (Ext_g d x) = Ext_g d (getOpt_g d x)
987 instance HasOpt_g d => Opt_g (Sub_g d) where
988 opt_g (Sub_g e1 e2) = case (opt_g e1, opt_g e2) of
989 (e1p, Lit_g
0) -> SubLoop_g e1p
990 (e1p, e2p ) -> Sub_g e1p e2p
991 opt_g (SubLoop_g e) = SubLoop_g (opt_g e)
993 instance (Typeable d, GDict (d (Neg_g d)), HasOpt_g d) => Opt_g (Neg_g d) where
994 opt_g (Neg_g (Add_g e1 e2))
995 = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2)))
996 opt_g (Neg_g (Ext_g d x))
997 = case fromDynamic (toDyn (getOpt_g d x)) of
998 Just (Neg_g e) -> NegLoop_g e
999 _ -> Neg_g (Ext_g d (getOpt_g d x))
1000 opt_g (Neg_g e) = Neg_g (opt_g e)
1001 opt_g (NegLoop_g e) = NegLoop_g (opt_g e)
1003 instance HasOpt_g d => Opt_g (Eq_g d) where
1004 opt_g (Eq_g e1 e2) = Eq_g (opt_g e1) (opt_g e2)
1005 opt_g (EqLoop_g e) = EqLoop_g (opt_g e)
1006 \end{lstHaskellLhstex
}
1007 \lstset{basicstyle=
\tt\small}
1011 \input{subfilepostamble
}