domain-specific_languages/class_deep_embedding.tex

   1 \documentclass[../thesis.tex]{subfiles}
   2
   3 \begin{document}
   4 \ifSubfilesClassLoaded{
   5         \pagenumbering{arabic}
   6 }{}
   7
   8 \mychapter{chp:classy_deep_embedding}{Deep embedding with class}%
   9
  10 \begin{chapterabstract}
  11         The two flavours of DSL embedding are shallow and deep embedding.
  12         In functional languages, shallow embedding models the language constructs as functions in which the semantics are embedded.
  13         Adding semantics is therefore cumbersome while adding constructs is a breeze.
  14         Upgrading the functions to type classes lifts this limitation to a certain extent.
  15
  16         Deeply embedded languages represent their language constructs as data and the semantics are functions on it.
  17         As a result, the language constructs are embedded in the semantics, hence adding new language constructs is laborious where adding semantics is trouble free.
  18
  19         This paper shows that by abstracting the semantics functions in deep embedding to type classes, it is possible to easily add language constructs as well.
  20         So-called classy deep embedding results in DSLs that are extensible both in language constructs and in semantics while maintaining a concrete abstract syntax tree.
  21         Additionally, little type-level trickery or complicated boilerplate code is required to achieve this.
  22 \end{chapterabstract}
  23
  24 \section{Introduction}%
  25 The two flavours of DSL embedding are deep and shallow embedding~\citep{boulton_experience_1992}.
  26 In functional programming languages, shallow embedding models language constructs as functions in the host language.
  27 As a result, adding new language constructs---extra functions---is easy.
  28 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.
  29
  30 On the other hand, deep embedding models language constructs as data in the host language.
  31 The semantics of the language are represented by functions over the data.
  32 Consequently, adding new semantics, i.e.\ novel functions, is straightforward.
  33 It can be stated that the language constructs are embedded in the functions that form a semantics.
  34 If one wants to add a language construct, all semantics functions must be revisited and revised to avoid ending up with partial functions.
  35
  36 This juxtaposition has been known for many years~\citep{reynolds_user-defined_1978} and discussed by many others~\citep{krishnamurthi_synthesizing_1998} but most famously dubbed the \emph{expression problem} by Wadler~\citep{wadler_expression_1998}:
  37
  38 \begin{quote}
  39         The \emph{expression problem} is a new name for an old problem.
  40         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).
  41 \end{quote}
  42
  43 In shallow embedding, abstracting the functions to type classes disentangles the language constructs from the semantics, allowing extension both ways.
  44 This technique is dubbed tagless-final embedding~\citep{carette_finally_2009}, nonetheless it is no silver bullet.
  45 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.
  46 The semantics of the 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}.
  47
  48 \subsection{Research contribution}
  49 This paper shows how to apply the technique observed in tagless-final embedding to deep embedding.
  50 The presented basic technique, christened \emph{classy deep embedding}, does not require advanced type system extensions to be used.
  51 However, it is suitable for type system extensions such as generalised algebraic data types.
  52 While this paper is written as a literate
  53 Haskell~\citep{peyton_jones_haskell_2003} program using some minor extensions provided by GHC~\citep{ghc_team_ghc_2021}, the idea is applicable to other languages as well\footnotemark{}.
  54 \footnotetext{Lubbers, M. (2021): Literate Haskell/lhs2\TeX{} source code of the paper ``Deep Embedding
  55 with Class'': TFP 2022.\ DANS.\ \url{https://doi.org/10.5281/zenodo.5081386}.}
  56
  57 \section{Deep embedding}%
  58
  59 Pick a DSL, any 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.}.
  62
  63 \begin{lstHaskellLhstex}
  64 data Expr_0 = Lit_0 Int
  65            | Add_0 Expr_0 Expr_0
  66 \end{lstHaskellLhstex}
  67
  68 Semantics are defined as functions on the \haskelllhstexinline{Expr_0} data type.
  69 For example, a function transforming the term to an integer---an evaluator---is implemented as follows.
  70
  71 \begin{lstHaskellLhstex}
  72 eval_0 :: Expr_0 -> Int
  73 eval_0 (Lit_0 e)     = e
  74 eval_0 (Add_0 e1 e2) = eval_0 e1 + eval_0 e2
  75 \end{lstHaskellLhstex}
  76
  77 Adding semantics---e.g.\ a printer---just means adding another function while the existing functions remain untouched.
  78 I.e.\ the key property of deep embedding.
  79 The following function, transforming the \haskelllhstexinline{Expr_0} data type to a string, defines a simple printer for our language.
  80
  81 \begin{lstHaskellLhstex}
  82 print_0 :: Expr_0 -> String
  83 print_0 (Lit_0 v)     = show v
  84 print_0 (Add_0 e1 e2) = "(" ++ print_0 e1 ++ "-" ++ print_0 e2 ++ ")"
  85 \end{lstHaskellLhstex}
  86
  87 While the language is concise and elegant, it is not very expressive.
  88 Traditionally, extending the language is achieved by adding a case to the \haskelllhstexinline{Expr_0} data type.
  89 So, adding subtraction to the language results in the following revised data type.
  90
  91 \begin{lstHaskellLhstex}
  92 data Expr_0 = Lit_0 Int
  93            | Add_0 Expr_0 Expr_0
  94            | Sub_0 Expr_0 Expr_0
  95 \end{lstHaskellLhstex}
  96
  97 Extending the DSL with language constructs exposes the Achilles' heel of deep embedding.
  98 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.
  99 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.
 100
 101 \section{Shallow embedding}%
 102
 103 Conversely, let us see how this would be done in shallow embedding.
 104 First, the data type is represented by functions in the host language with embedded semantics.
 105 Therefore, the evaluators for literals and addition both become a function in the host language as follows.
 106
 107 \begin{lstHaskellLhstex}
 108 type Sem_s = Int
 109
 110 lit_s :: Int -> Sem_s
 111 lit_s i = i
 112
 113 add_s :: Sem_s -> Sem_s -> Sem_s
 114 add_s e1 e2 = e1 + e2
 115 \end{lstHaskellLhstex}
 116
 117 Adding constructions to the language is done by adding functions.
 118 Hence, the following function adds subtraction to our language.
 119
 120 \begin{lstHaskellLhstex}
 121 sub_s :: Sem_s -> Sem_s -> Sem_s
 122 sub_s e1 e2 = e1 - e2
 123 \end{lstHaskellLhstex}
 124
 125 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.
 126 One way to add semantics is to change all functions to execute both semantics at the same time.
 127 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
 128 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.
 129
 130 \subsection{Tagless-final embedding}
 131 Tagless-final embedding overcomes the limitations of standard shallow embedding.
 132 To upgrade to this embedding technique, the language constructs are changed from functions to type classes.
 133 For our language this results in the following type class definition.
 134
 135 \begin{lstHaskellLhstex}
 136 class Expr_t s where
 137     lit_t :: Int -> s
 138     add_t :: s -> s -> s
 139 \end{lstHaskellLhstex}
 140
 141 Semantics become data types\footnotemark{} implementing these type classes, resulting in the following instance for the evaluator.
 142 \footnotetext{%
 143         In this case \haskelllhstexinline{newtype}s are used instead of regular \haskelllhstexinline{data} declarations.
 144         A \haskelllhstexinline{newtype} is a special data type with a single constructor containing a single value only to which it is isomorphic.
 145         It allows the programmer to define separate class instances that the instances of the isomorphic type without any overhead.
 146         During compilation the constructor is completely removed~\cite[Sec.~4.2.3]{peyton_jones_haskell_2003}.
 147 }
 148
 149 \begin{lstHaskellLhstex}
 150 newtype Eval_t = E_t Int
 151
 152 instance Expr_t Eval_t where
 153     lit_t v               = E_t v
 154     add_t (E_t e1) (E_t e2) = E_t (e1 + e2)
 155 \end{lstHaskellLhstex}
 156
 157 Adding constructs---e.g.\ subtraction---just results in an extra type class and corresponding instances.
 158
 159 \begin{lstHaskellLhstex}
 160 class Sub_t s where
 161     sub_t :: s -> s -> s
 162
 163 instance Sub_t Eval_t where
 164     sub_t (E_t e1) (E_t e2) = E_t (e1 - e2)
 165 \end{lstHaskellLhstex}
 166
 167 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.
 168
 169 \begin{lstHaskellLhstex}
 170 newtype Printer_t = P_t String
 171
 172 instance Expr_t Printer_t where
 173     lit_t i               = P_t (show i)
 174     add_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "+" ++ e2 ++ ")")
 175
 176 instance Sub_t Printer_t where
 177     sub_t (P_t e1) (P_t e2) = P_t ("(" ++ e1 ++ "-" ++ e2 ++ ")")
 178 \end{lstHaskellLhstex}
 179
 180 \section{Lifting the backends}%
 181 Let us rethink the deeply embedded DSL design.
 182 Remember that in shallow embedding, the semantics are embedded in the language construct functions.
 183 Obtaining extensibility both in constructs and semantics was accomplished by abstracting the semantics functions to type classes, making the constructs overloaded in the semantics.
 184 In deep embedding, the constructs are embedded in the semantics functions instead.
 185 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.
 186 The same effect may be achieved when using similar techniques such as explicit dictionary passing or ML style modules.
 187 In our language this results in the following type class.
 188
 189 \begin{lstHaskellLhstex}
 190 class Eval_1 v where
 191     eval_1 :: v -> Int
 192
 193 data Expr_1 = Lit_1 Int
 194            | Add_1 Expr_1 Expr_1
 195 \end{lstHaskellLhstex}
 196
 197 Implementing the semantics type class instances for the \haskelllhstexinline{Expr_1} data type is an elementary exercise.
 198 By a copy-paste and some modifications, we come to the following implementation.
 199
 200 \begin{lstHaskellLhstex}
 201 instance Eval_1 Expr_1 where
 202     eval_1 (Lit_1 v)     = v
 203     eval_1 (Add_1 e1 e2) = eval_1 e1 + eval_1 e2
 204 \end{lstHaskellLhstex}
 205
 206 Subtraction can now be defined in a separate data type, leaving the original data type intact.
 207 Instances for the additional semantics can now be implemented separately as instances of the type classes.
 208
 209 \begin{lstHaskellLhstex}
 210 data Sub_1 = Sub_1 Expr_1 Expr_1
 211
 212 instance Eval_1 Sub_1 where
 213     eval_1 (Sub_1 e1 e2) = eval_1 e1 - eval_1 e2
 214 \end{lstHaskellLhstex}
 215
 216 \section{Existential data types}%
 217
 218 The astute reader might have noticed that we have dissociated ourselves from the original data type.
 219 It is only possible to create an expression with a subtraction on the top level.
 220 The recursive knot is left untied and as a result, \haskelllhstexinline{Sub_1} can never be reached from an \haskelllhstexinline{Expr_1}.
 221
 222 Luckily, we can reconnect them by adding a special constructor to the \haskelllhstexinline{Expr_1} data type for housing extensions.
 223 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~\cite[Chp.~6.4.6]{ghc_team_ghc_2021} to allow it to house not just subtraction but any future extension.
 224
 225 \begin{lstHaskellLhstex}
 226 data Expr_2 =                      Lit_2 Int
 227            |                      Add_2 Expr_2 Expr_2
 228            | forall x. Eval_2 x => Ext_2 x
 229 \end{lstHaskellLhstex}
 230
 231 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.
 232
 233 \begin{lstHaskellLhstex}
 234 instance Eval_2 Expr_2 where
 235     eval_2 (Lit_2  v)      = v
 236     eval_2 (Add_2  e1 e2)  = eval_2 e1 + eval_2 e2
 237     eval_2 (Ext_2  x)      = eval_2 x
 238 \end{lstHaskellLhstex}
 239
 240 Adding language construct extensions in different data types does mean that an extra \haskelllhstexinline{Ext_2} tag is introduced when using the extension.
 241 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.
 242
 243 \begin{lstHaskellLhstex}
 244 sub_2 :: Expr_2 -> Expr_2 -> Expr_2
 245 sub_2 e1 e2 = Ext_2 (Sub_2 e1 e2)
 246 \end{lstHaskellLhstex}
 247
 248 In our example this means that the programmer can write\footnotemark{}:
 249 \footnotetext{%
 250         Backticks are used to use functions or constructors in an infix fashion~\cite[Sec.~4.3.3]{peyton_jones_haskell_2003}.
 251 }
 252 \begin{lstHaskellLhstex}
 253 e2 :: Expr_2
 254 e2 = Lit_2 42 `sub_2` Lit_2 1
 255 \end{lstHaskellLhstex}
 256 instead of having to write
 257 \begin{lstHaskellLhstex}
 258 e2p :: Expr_2
 259 e2p = Ext_2 (Lit_2 42 `Sub_2` Lit_2 1)
 260 \end{lstHaskellLhstex}
 261
 262 \subsection{Unbraiding the semantics from the data}
 263 This approach does reveal a minor problem.
 264 Namely, that all semantics type classes are braided into our datatypes via the \haskelllhstexinline{Ext_2} constructor.
 265 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
 266 Thus, if we add semantics, the main data type's type class constraints in the \haskelllhstexinline{Ext_2} constructor need to be updated.
 267 To avoid this, the type classes can be bundled in a type class alias or type class collection as follows.
 268
 269 \begin{lstHaskellLhstex}
 270 class (Eval_2 x, Print_2 x) => Semantics_2 x
 271
 272 data Expr_2 =                           Lit_2 Int
 273            |                           Add_2 Expr_2 Expr_2
 274            | forall x. Semantics_2 x => Ext_2 x
 275 \end{lstHaskellLhstex}
 276
 277 The class alias removes the need for the programmer to visit the main data type when adding additional semantics.
 278 Unfortunately, the compiler does need to visit the main data type again.
 279 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.
 280 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.
 281 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.
 282 First the data types for the language constructs are parametrised by the type variable \haskelllhstexinline{d} as follows.
 283
 284 \begin{lstHaskellLhstex}
 285 data Expr_3 d =           Lit_3 Int
 286              |           Add_3 (Expr_3 d) (Expr_3 d)
 287              | forall x. Ext_3 (d x) x
 288
 289 data Sub_3 d =            Sub_3 (Expr_3 d) (Expr_3 d)
 290 \end{lstHaskellLhstex}
 291
 292 The \haskelllhstexinline{d} type variable is inhabited by an explicit dictionary for the semantics, i.e.\ a witness to the class instance.
 293 Therefore, for all semantics type classes, a data type is made that contains the semantics function for the given semantics.
 294 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}.
 295
 296 \begin{lstHaskellLhstex}
 297 newtype EvalDict_3 v = EvalDict_3 (v -> Int)
 298
 299 class HasEval_3 d where
 300     getEval_3 :: d v -> v -> Int
 301
 302 instance HasEval_3 EvalDict_3 where
 303     getEval_3 (EvalDict_3 e) = e
 304 \end{lstHaskellLhstex}
 305
 306 The instances for the type classes change as well according to the change in the datatype.
 307 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}.
 308
 309 \begin{lstHaskellLhstex}
 310 instance HasEval_3 d => Eval_3 (Expr_3 d) where
 311     eval_3 (Lit_3 v)     = v
 312     eval_3 (Add_3 e1 e2) = eval_3 e1 + eval_3 e2
 313     eval_3 (Ext_3 d x)   = getEval_3 d x
 314
 315 instance HasEval_3 d => Eval_3 (Sub_3 d) where
 316     eval_3 (Sub_3 e1 e2) = eval_3 e1 - eval_3 e2
 317 \end{lstHaskellLhstex}
 318
 319 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.
 320 To achieve this, a type class is introduced that allows the generation of such a dictionary.
 321
 322 \begin{lstHaskellLhstex}
 323 class GDict a where
 324     gdict :: a
 325 \end{lstHaskellLhstex}
 326
 327 This type class has individual instances for all semantics dictionaries, linking the class instance to the witness value.
 328 I.e.\ if there is a type class instance known, a witness value can be conjured using the \haskelllhstexinline{gdict} function.
 329
 330 \begin{lstHaskellLhstex}
 331 instance Eval_3 v => GDict (EvalDict_3 v) where
 332     gdict = EvalDict_3 eval_3
 333 \end{lstHaskellLhstex}
 334
 335 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:
 336
 337 \begin{lstHaskellLhstex}
 338 sub_3 :: GDict (d (Sub_3 d)) => Expr_3 d -> Expr_3 d -> Expr_3 d
 339 sub_3 e1 e2 = Ext_3 gdict (Sub_3 e1 e2)
 340 \end{lstHaskellLhstex}
 341
 342 Finally, we reached the end goal, orthogonal extension of both language constructs as shown by adding subtraction to the language and in language semantics.
 343 Adding the printer can now be done without touching the original code as follows.
 344 First the printer type class, dictionaries and instances for \haskelllhstexinline{GDict} are defined.
 345
 346 \begin{lstHaskellLhstex}
 347 class Print_3 v where
 348     print_3 :: v -> String
 349
 350 newtype PrintDict_3 v = PrintDict_3 (v -> String)
 351
 352 class HasPrint_3 d where
 353     getPrint_3 :: d v -> v -> String
 354
 355 instance HasPrint_3 PrintDict_3 where
 356     getPrint_3 (PrintDict_3 e) = e
 357
 358 instance Print_3 v => GDict (PrintDict_3 v) where
 359     gdict = PrintDict_3 print_3
 360 \end{lstHaskellLhstex}
 361
 362 Then the instances for \haskelllhstexinline{Print_3} of all the language constructs can be defined.
 363
 364 \begin{lstHaskellLhstex}
 365 instance HasPrint_3 d => Print_3 (Expr_3 d) where
 366     print_3 (Lit_3 v)     = show v
 367     print_3 (Add_3 e1 e2) = "(" ++ print_3 e1 ++ "+" ++ print_3 e2 ++ ")"
 368     print_3 (Ext_3 d x)   = getPrint_3 d x
 369 instance HasPrint_3 d => Print_3 (Sub_3 d) where
 370     print_3 (Sub_3 e1 e2) = "(" ++ print_3 e1 ++ "-" ++ print_3 e2 ++ ")"
 371 \end{lstHaskellLhstex}
 372
 373 \section{Transformation semantics}%
 374
 375 Most semantics convert a term to some final representation and can be expressed just by functions on the cases.
 376 However, the implementation of semantics such as transformation or optimisation may benefit from a so-called intentional analysis of the abstract syntax tree.
 377 In shallow embedding, the implementation for these types of semantics is difficult because there is no tangible abstract syntax tree.
 378 In off-the-shelf deep embedding this is effortless since the function can pattern match on the constructor or structures of constructors.
 379
 380 To demonstrate intensional analyses in classy deep embedding we write an optimizer that removes addition and subtraction by zero.
 381 In classy deep embedding, adding new semantics means first adding a new type class housing the function including the machinery for the extension constructor.
 382
 383 \begin{lstHaskellLhstex}
 384 class Opt_3 v where
 385     opt_3 :: v -> v
 386
 387 newtype OptDict_3 v = OptDict_3 (v -> v)
 388
 389 class HasOpt_3 d where
 390     getOpt_3 :: d v -> v -> v
 391
 392 instance HasOpt_3 OptDict_3 where
 393     getOpt_3 (OptDict_3 e) = e
 394
 395 instance Opt_3 v => GDict (OptDict_3 v) where
 396     gdict = OptDict_3 opt_3
 397 \end{lstHaskellLhstex}
 398
 399 The implementation of the optimizer for the \haskelllhstexinline{Expr_3} data type is no complicated task.
 400 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.
 401 If this is the case, the addition is removed.
 402
 403 \begin{lstHaskellLhstex}
 404 instance HasOpt_3 d => Opt_3 (Expr_3 d) where
 405     opt_3 (Lit_3 v)     = Lit_3 v
 406     opt_3 (Add_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
 407         (Lit_3 0, e2p    ) -> e2p
 408         (e1p,     Lit_3 0) -> e1p
 409         (e1p,     e2p    ) -> Add_3 e1p e2p
 410     opt_3 (Ext_3 d x)   = Ext_3 d (getOpt_3 d x)
 411 \end{lstHaskellLhstex}
 412
 413 Replicating this for the \haskelllhstexinline{Opt_3} instance of \haskelllhstexinline{Sub_3} seems a clear-cut task at first glance.
 414
 415 \begin{lstHaskellLhstex}
 416 instance HasOpt_3 d => Opt_3 (Sub_3 d) where
 417     opt_3 (Sub_3 e1 e2) = case (opt_3 e1, opt_3 e2) of
 418         (e1p, Lit_3 0) -> e1p
 419         (e1p, e2p    ) -> Sub_3 e1p e2p
 420 \end{lstHaskellLhstex}
 421
 422 Unsurprisingly, this code is rejected by the compiler.
 423 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.
 424 However, the type signature of the function dictates that it should be of type \haskelllhstexinline{Sub_3}.
 425 To overcome this problem we add a convolution constructor.
 426
 427 \subsection{Convolution}%
 428
 429 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.
 430 It should be noted that a loopback case is \emph{only} required if the transformation actually removes tags.
 431 This changes the \haskelllhstexinline{Sub_3} data type as follows.
 432
 433 \begin{lstHaskellLhstex}
 434 data Sub_4 d = Sub_4     (Expr_4 d) (Expr_4 d)
 435             | SubLoop_4 (Expr_4 d)
 436
 437 instance HasEval_4 d => Eval_4 (Sub_4 d) where
 438     eval_4 (Sub_4     e1 e2) = eval_4 e1 - eval_4 e2
 439     eval_4 (SubLoop_4 e1)    = eval_4 e1
 440 \end{lstHaskellLhstex}
 441
 442 With this loopback case in the toolbox, the following \haskelllhstexinline{Sub} instance optimises away subtraction with zero literals.
 443
 444 \begin{lstHaskellLhstex}
 445 instance HasOpt_4 d => Opt_4 (Sub_4 d) where
 446     opt_4 (Sub_4 e1 e2) = case (opt_4 e1, opt_4 e2) of
 447         (e1p, Lit_4 0) -> SubLoop_4 e1p
 448         (e1p, e2p    ) -> Sub_4 e1p e2p
 449     opt_4 (SubLoop_4 e) =  SubLoop_4 (opt_4 e)
 450 \end{lstHaskellLhstex}
 451
 452 \subsection{Pattern matching}%
 453
 454 Pattern matching within datatypes and from an extension to the main data type works out of the box.
 455 Cross-extensional pattern matching on the other hand---matching on a particular extension---is something that requires a bit of extra care.
 456 Take for example negation propagation and double negation elimination.
 457 Pattern matching on values with an existential type is not possible without leveraging dynamic typing~\citep{abadi_dynamic_1991,baars_typing_2002}.
 458 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.
 459 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.
 460
 461 \begin{lstHaskellLhstex}
 462 data Expr_4 d =                         Lit_4 Int
 463              |                         Add_4 (Expr_4 d) (Expr_4 d)
 464              | forall x. Typeable x => Ext_4 (d x) x
 465 \end{lstHaskellLhstex}
 466
 467 First let us add negation to the language by defining a datatype representing it.
 468 Negation elimination requires the removal of negation constructors, so a convolution constructor is defined as well.
 469
 470 \begin{lstHaskellLhstex}
 471 data Neg_4 d = Neg_4     (Expr_4 d)
 472             | NegLoop_4 (Expr_4 d)
 473
 474 neg_4 :: (Typeable d, GDict (d (Neg_4 d))) => Expr_4 d -> Expr_4 d
 475 neg_4 e = Ext_4 gdict (Neg_4 e)
 476 \end{lstHaskellLhstex}
 477
 478 The evaluation and printer instances for the \haskelllhstexinline{Neg_4} datatype are defined as follows.
 479
 480 \begin{lstHaskellLhstex}
 481 instance HasEval_4 d => Eval_4 (Neg_4 d) where
 482     eval_4 (Neg_4     e) = negate (eval_4 e)
 483     eval_4 (NegLoop_4 e) = eval_4 e
 484
 485 instance HasPrint_4 d => Print_4 (Neg_4 d) where
 486     print_4 (Neg_4     e) = "(~" ++ print_4 e ++ ")"
 487     print_4 (NegLoop_4 e) = print_4 e
 488 \end{lstHaskellLhstex}
 489
 490 The \haskelllhstexinline{Opt_4} instance contains the interesting bit.
 491 If the sub expression of a negation is an addition, negation is propagated downwards.
 492 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.
 493
 494 \begin{lstHaskellLhstex}
 495 instance (Typeable d, GDict (d (Neg_4 d)), HasOpt_4 d) => Opt_4 (Neg_4 d) where
 496     opt_4 (Neg_4 (Add_4 e1 e2))
 497         = NegLoop_4 (Add_4 (opt_4 (neg_4 e1)) (opt_4 (neg_4 e2)))
 498     opt_4 (Neg_4 (Ext_4 d x))
 499         = case fromDynamic (toDyn (getOpt_4 d x)) of
 500             Just (Neg_4 e) -> NegLoop_4 e
 501             _             -> Neg_4 (Ext_4 d (getOpt_4 d x))
 502     opt_4 (Neg_4     e) = Neg_4 (opt_4 e)
 503     opt_4 (NegLoop_4 e) = NegLoop_4 (opt_4 e)
 504 \end{lstHaskellLhstex}
 505
 506 Loopback cases do make cross-extensional pattern matching less modular in general.
 507 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.
 508 Fortunately, this problem can be mitigated---if required---by just introducing an additional optimisation semantics that removes loopback cases.
 509 Luckily, one does not need to resort to these arguably blunt matters often.
 510 Dependent language functionality often does not need to span extensions, i.e.\ it is possible to group them in the same data type.
 511
 512 \subsection{Chaining semantics}
 513 Now that the data types are parametrised by the semantics a final problem needs to be overcome.
 514 The data type is parametrised by the semantics, thus, using multiple semantics, such as evaluation after optimising is not straightforwardly possible.
 515 Luckily, a solution is readily at hand: introduce an ad-hoc combination semantics.
 516
 517 \begin{lstHaskellLhstex}
 518 data OptPrintDict_4 v = OPD_4 (OptDict_4 v) (PrintDict_4 v)
 519
 520 instance HasOpt_4   OptPrintDict_4 where
 521     getOpt_4   (OPD_4 v _) = getOpt_4 v
 522 instance HasPrint_4 OptPrintDict_4 where
 523     getPrint_4 (OPD_4 _ v) = getPrint_4 v
 524
 525 instance (Opt_4 v, Print_4 v) => GDict (OptPrintDict_4 v) where
 526     gdict = OPD_4 gdict gdict
 527 \end{lstHaskellLhstex}
 528
 529 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.
 530
 531 \begin{lstHaskellLhstex}
 532 e1 :: Expr_4  OptPrintDict_4
 533 e1 = neg_4 (Lit_4 42 `Add_4` Lit_4 38) `sub_4` Lit_4 0
 534 \end{lstHaskellLhstex}
 535
 536 When using classy deep embedding to the fullest, the ability of the compiler to infer very general types expires.
 537 As a consequence, defining reusable expressions that are overloaded in their semantics requires quite some type class constraints that cannot be inferred by the compiler (yet) if they use many extensions.
 538 Solving this remains future work.
 539 For example, the expression $\sim(42-38)+1$ has to be defined as:
 540
 541 \begin{lstHaskellLhstex}
 542 e3 :: (Typeable d, GDict (d (Neg_4 d)), GDict (d (Sub_4 d))) => Expr_4 d
 543 e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1
 544 \end{lstHaskellLhstex}
 545
 546 \section{Generalised algebraic data types}%
 547 Generalised algebraic data types (GADTs) are enriched data types that allow the type instantiation of the constructor to be explicitly defined~\citep{cheney_first-class_2003,hinze_fun_2003}.
 548 Leveraging GADTs, deeply embedded DSLs can be made statically type safe even when different value types are supported.
 549 Even when GADTs are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types~\cite[Sec.~2.2]{cheney_lightweight_2002}.
 550 Where some solutions to the expression problem do not easily generalise to GADTs (see \cref{sec:cde:related}), classy deep embedding does.
 551 Generalising the data structure of our DSL is fairly straightforward and to spice things up a bit, we add an equality and boolean not language construct.
 552 To make the existing DSL constructs more general, we relax the types of those constructors.
 553 For example, operations on integers now work on all numerals instead.
 554 Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the DSL domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer.
 555 Since some optimisations on \haskelllhstexinline{Not_g} remove constructors and therefore use cross-extensional pattern matches, \haskelllhstexinline{Typeable} constraints are added to \haskelllhstexinline{a}.
 556 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.
 557 Finally, not to repeat ourselves too much, we only show the parts that substantially changed.
 558 The omitted definitions and implementation can be found in \cref{sec:cde:appendix}.
 559
 560 \begin{lstHaskellLhstex}
 561 data Expr_g d a where
 562     Lit_g     :: Show a        => a -> Expr_g d a
 563     Add_g     :: (Eq a, Num a) => Expr_g d a -> Expr_g d a -> Expr_g d a
 564     Ext_g     :: Typeable x    => d x -> x a -> Expr_g d a
 565 data Neg_g  d a where
 566     Neg_g     :: (Typeable a, Num a) => Expr_g d a -> Neg_g d a
 567     NegLoop_g ::                        Expr_g d a -> Neg_g d a
 568 data Not_g  d a where
 569     Not_g     :: Expr_g d Bool -> Not_g d Bool
 570     NotLoop_g :: Expr_g d a    -> Not_g d a
 571 \end{lstHaskellLhstex}
 572
 573 The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskelllhstexinline{d} type variable for it to be usable in the \haskelllhstexinline{Ext_g} constructor as can be seen in the smart constructor for \haskelllhstexinline{Neg_g}:
 574
 575 \begin{lstHaskellLhstex}
 576 neg_g  :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) =>
 577     Expr_g d a -> Expr_g d a
 578 neg_g e = Ext_g gdict (Neg_g e)
 579
 580 not_g  :: (Typeable d,  GDict (d (Not_g d))) =>
 581     Expr_g d Bool -> Expr_g d Bool
 582 not_g e = Ext_g gdict (Not_g e)
 583 \end{lstHaskellLhstex}
 584
 585 Upgrading the semantics type classes to support GADTs is done by an easy textual search and replace.
 586 All occurrences of \haskelllhstexinline{v} are now parametrised by type variable \haskelllhstexinline{a}:
 587
 588 \begin{lstHaskellLhstex}
 589 class Eval_g  v where
 590     eval_g  :: v a -> a
 591 class Print_g v where
 592     print_g :: v a -> String
 593 class Opt_g   v where
 594     opt_g   :: v a -> v a
 595 \end{lstHaskellLhstex}
 596
 597 Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
 598 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.
 599 To represent this type class function, a rank-2 polymorphic function is needed~\cite[Chp.~6.4.15]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
 600 Concretely, for the evaluatior this results in the following definitions:
 601
 602 \begin{lstHaskellLhstex}
 603 newtype EvalDict_g v = EvalDict_g (forall a. v a -> a)
 604 class HasEval_g d where
 605     getEval_g :: d v -> v a -> a
 606 instance HasEval_g EvalDict_g where
 607     getEval_g (EvalDict_g e) = e
 608 \end{lstHaskellLhstex}
 609
 610 The \haskelllhstexinline{GDict} type class is general enough, so the instances can remain the same.
 611 The \haskelllhstexinline{Eval_g} instance of \haskelllhstexinline{GDict} looks as follows:
 612
 613 \begin{lstHaskellLhstex}
 614 instance Eval_g v => GDict (EvalDict_g v) where
 615     gdict = EvalDict_g eval_g
 616 \end{lstHaskellLhstex}
 617
 618 Finally, the implementations for the instances can be ported without complication show using the optimisation instance of \haskelllhstexinline{Not_g}:
 619
 620 \begin{lstHaskellLhstex}
 621 instance (Typeable d, GDict (d (Not_g d)), HasOpt_g d) => Opt_g (Not_g d) where
 622     opt_g (Not_g (Ext_g d x))
 623         = case fromDynamic (toDyn (getOpt_g d x)) :: Maybe (Not_g d Bool) of
 624             Just (Not_g e) -> NotLoop_g e
 625             _             -> Not_g (Ext_g d (getOpt_g d x))
 626     opt_g (Not_g e)     = Not_g (opt_g e)
 627     opt_g (NotLoop_g e) = NotLoop_g (opt_g e)
 628 \end{lstHaskellLhstex}
 629
 630 \section{Conclusion}%
 631
 632 Classy deep embedding is a novel organically grown embedding technique that alleviates deep embedding from the extensibility problem in most cases.
 633
 634 By abstracting the semantics functions to type classes they become overloaded in the language constructs.
 635 Thus, making it possible to add new language constructs in a separate type.
 636 These extensions are brought together in a special extension constructor residing in the main data type.
 637 This extension case is overloaded by the language construct using a data type containing the class dictionary.
 638 As a result, orthogonal extension is possible for language constructs and semantics using only little syntactic overhead or type annotations.
 639 The basic technique only requires---well established through history and relatively standard---existential data types.
 640 However, if needed, the technique generalises to GADTs as well, adding rank-2 types to the list of type system requirements as well.
 641 Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
 642
 643 Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
 644
 645 \section{Related work}%
 646 \label{sec:cde:related}
 647
 648 Embedded 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.
 649
 650 Clearly, classy deep embedding bears most similarity to the \emph{Datatypes \`a la Carte}~\citep{swierstra_data_2008}.
 651 In Swierstra's approach, semantics are lifted to type classes similarly to classy deep embedding.
 652 Each language construct is their own datatype parametrised by a type parameter.
 653 This parameter contains some type level representation of language constructs that are in use.
 654 In classy deep embedding, extensions do not have to be enumerated at the type level but are captured in the extension case.
 655 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.
 656 Furthermore, it requires some boilerplate code such as functor instances for the data types.
 657 In return, pattern matching is easier and does not require dynamic typing.
 658 Classy deep embedding only strains the programmer with writing the extension case for the main data type and the occasional loopback constructor.
 659
 660 L\"oh and Hinze 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~\citep{loh_open_2006}.
 661 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.
 662 In contrast, this paper shows that pattern matching is easily attainable---albeit using dynamic types---and that the terms can be typed without complicated type system extensions.
 663
 664 A technique similar to classy deep embedding was proposed by Najd and Peyton~Jones to tackle a slightly different problem, namely that of reusing a data type for multiple purposes in a slightly different form~\citep{najd_trees_2017}.
 665 For example to decorate the abstract syntax tree of a compiler differently for each phase of the compiler.
 666 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.
 667 Classy deep embedding works similarly but uses existentially quantified type variables to describe possible extensions instead of type variables and type families.
 668 In classy deep embedding, the extensions do not need to be encoded in the type system and less boilerplate is required.
 669 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.
 670
 671 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}.
 672 Classy deep embedding was organically grown from observing the evolution of tagless-final embedding.
 673 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.
 674 In classy deep embedding, it is possible to define transformations even across extensions.
 675
 676 Hybrid approaches between deep and shallow embedding exist as well.
 677 For example, Svenningson et al.\ show that by expressing the deeply embedded language in a shallowly embedded core language, extensions can be made orthogonally as well~\citep{svenningsson_combining_2013}.
 678 This paper differs from those approaches in the sense that it does not require a core language in which all extensions need to be expressible.
 679
 680 \section*{Acknowledgements}
 681 This research is partly funded by the Royal Netherlands Navy.
 682 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.
 683
 684 %\appendix
 685 \begin{subappendices}
 686 \section{Data types and definitions}%
 687 \label{sec:cde:appendix}
 688 \begin{lstHaskellLhstex}[caption={Data type definitions.}]
 689 data Sub_g d a where
 690     Sub_g     :: (Eq a, Num a)      => Expr_g d a -> Expr_g d a -> Sub_g d a
 691     SubLoop_g ::                       Expr_g d a -> Sub_g d a
 692
 693 data Eq_g d a  where
 694     Eq_g      :: (Typeable a, Eq a) => Expr_g d a -> Expr_g d a -> Eq_g d Bool
 695     EqLoop_g  ::                       Expr_g d a -> Eq_g d a
 696 \end{lstHaskellLhstex}
 697
 698 \begin{lstHaskellLhstex}[caption={Smart constructions.}]
 699 sub_g :: (Typeable d, GDict (d (Sub_g d)), Eq a, Num a) =>
 700     Expr_g d a -> Expr_g d a -> Expr_g d a
 701 sub_g e1 e2 = Ext_g gdict (Sub_g e1 e2)
 702
 703 eq_g :: (Typeable d, GDict (d (Eq_g d)), Eq a, Typeable a) =>
 704     Expr_g d a -> Expr_g d a -> Expr_g d Bool
 705 eq_g e1 e2 = Ext_g gdict (Eq_g e1 e2)
 706 \end{lstHaskellLhstex}
 707
 708 \begin{lstHaskellLhstex}[caption={Semantics classes and data types.}]
 709 newtype PrintDict_g v = PrintDict_g (forall a.v a -> String)
 710
 711 class HasPrint_g d where
 712     getPrint_g :: d v -> v a -> String
 713
 714 instance HasPrint_g PrintDict_g where
 715     getPrint_g (PrintDict_g e) = e
 716
 717 newtype OptDict_g v = OptDict_g (forall a.v a -> v a)
 718
 719 class HasOpt_g d where
 720     getOpt_g :: d v -> v a -> v a
 721
 722 instance HasOpt_g OptDict_g where
 723     getOpt_g (OptDict_g e) = e
 724 \end{lstHaskellLhstex}
 725
 726 \begin{lstHaskellLhstex}[caption={\texorpdfstring{\haskelllhstexinline{GDict}}{GDict} instances}]
 727 instance Print_g v => GDict (PrintDict_g v) where
 728     gdict = PrintDict_g print_g
 729 instance Opt_g v   => GDict (OptDict_g v)   where
 730     gdict = OptDict_g opt_g
 731 \end{lstHaskellLhstex}
 732
 733 \begin{lstHaskellLhstex}[caption={Evaluator instances}]
 734 instance HasEval_g d => Eval_g (Expr_g d) where
 735     eval_g (Lit_g v)     = v
 736     eval_g (Add_g e1 e2) = eval_g e1 + eval_g e2
 737     eval_g (Ext_g d x)   = getEval_g d x
 738
 739 instance HasEval_g d => Eval_g (Sub_g d) where
 740     eval_g (Sub_g     e1 e2) = eval_g e1 - eval_g e2
 741     eval_g (SubLoop_g e)     = eval_g e
 742
 743 instance HasEval_g d => Eval_g (Neg_g d) where
 744     eval_g (Neg_g     e) = negate (eval_g e)
 745     eval_g (NegLoop_g e) = eval_g e
 746
 747 instance HasEval_g d => Eval_g (Eq_g d) where
 748     eval_g (Eq_g     e1 e2) = eval_g e1 == eval_g e2
 749     eval_g (EqLoop_g e)     = eval_g e
 750
 751 instance HasEval_g d => Eval_g (Not_g d) where
 752     eval_g (Not_g     e) = not (eval_g e)
 753     eval_g (NotLoop_g e) = eval_g e
 754 \end{lstHaskellLhstex}
 755
 756 \begin{lstHaskellLhstex}[caption={Printer instances}]
 757 instance HasPrint_g d => Print_g (Expr_g d) where
 758     print_g (Lit_g v)     = show v
 759     print_g (Add_g e1 e2) = "(" ++ print_g e1 ++ "+" ++ print_g e2 ++ ")"
 760     print_g (Ext_g d x)   = getPrint_g d x
 761
 762 instance HasPrint_g d => Print_g (Sub_g d) where
 763     print_g (Sub_g     e1 e2) = "(" ++ print_g e1 ++ "-" ++ print_g e2 ++ ")"
 764     print_g (SubLoop_g e)     = print_g e
 765
 766 instance HasPrint_g d => Print_g (Neg_g d) where
 767     print_g (Neg_g     e) = "(negate " ++ print_g e ++ ")"
 768     print_g (NegLoop_g e) = print_g e
 769
 770 instance HasPrint_g d => Print_g (Eq_g d) where
 771     print_g (Eq_g     e1 e2) = "(" ++ print_g e1 ++ "==" ++ print_g e2 ++ ")"
 772     print_g (EqLoop_g e)     = print_g e
 773
 774 instance HasPrint_g d => Print_g (Not_g d) where
 775     print_g (Not_g     e) = "(not " ++ print_g e ++ ")"
 776     print_g (NotLoop_g e) = print_g e
 777 \end{lstHaskellLhstex}
 778
 779 \begin{lstHaskellLhstex}[caption={Optimisation instances}]
 780 instance HasOpt_g d => Opt_g (Expr_g d) where
 781     opt_g (Lit_g v)     = Lit_g v
 782     opt_g (Add_g e1 e2) = case (opt_g e1, opt_g e2) of
 783         (Lit_g 0, e2p    ) -> e2p
 784         (e1p,     Lit_g 0) -> e1p
 785         (e1p,     e2p    ) -> Add_g e1p e2p
 786     opt_g (Ext_g d x)   = Ext_g d (getOpt_g d x)
 787
 788 instance HasOpt_g d => Opt_g (Sub_g d) where
 789     opt_g (Sub_g     e1 e2) = case (opt_g e1, opt_g e2) of
 790         (e1p, Lit_g 0) -> SubLoop_g e1p
 791         (e1p, e2p    ) -> Sub_g e1p e2p
 792     opt_g (SubLoop_g e)     = SubLoop_g (opt_g e)
 793
 794 instance (Typeable d, GDict (d (Neg_g d)), HasOpt_g d) => Opt_g (Neg_g d) where
 795     opt_g (Neg_g (Add_g e1 e2))
 796         = NegLoop_g (Add_g (opt_g (neg_g e1)) (opt_g (neg_g e2)))
 797     opt_g (Neg_g (Ext_g d x))
 798         = case fromDynamic (toDyn (getOpt_g d x)) of
 799             Just (Neg_g e) -> NegLoop_g e
 800             _             -> Neg_g (Ext_g d (getOpt_g d x))
 801     opt_g (Neg_g     e)        = Neg_g (opt_g e)
 802     opt_g (NegLoop_g e)        = NegLoop_g (opt_g e)
 803
 804 instance HasOpt_g d => Opt_g (Eq_g d) where
 805     opt_g (Eq_g     e1 e2) = Eq_g (opt_g e1) (opt_g e2)
 806     opt_g (EqLoop_g e)     = EqLoop_g (opt_g e)
 807 \end{lstHaskellLhstex}
 808
 809 \end{subappendices}
 810
 811 \input{subfilepostamble}
 812 \end{document}