+ opt_g (Eq_g e1 e2) = Eq_g (opt_g e1) (opt_g e2)
+ opt_g (EqLoop_g e) = EqLoop_g (opt_g e)
+\end{lstHaskellLhstex}
+
+\section{Chaining semantics (reprise)}\label{sec:classy_reprise}
+\todo{Verbeteren}
+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.
+However, while generalising the technique to \glspl{GADT} arguably unleashes a cesspool of \emph{unsafe} compiler extensions.
+If we are willing to work with extensions, much of the boilerplate can be either generated or omitted entirely.
+
+The \gls{DSL} datatype is parametrised by a type variable providing a witness to the view on the language.
+Using constraint kinds, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
+Furthermore, when resorting to the \GHCmod{DataKinds} and \GHCmod{PolyKinds} extensions, this constraint does not necessarily has to be a single constraint, using a \haskelllhstexinline{Record} auxiliary type, we can encode list of witnesses.
+The data type for this list of witnesses is \haskelllhstexinline{Record}.
+Record is parametrised by two type variables, the first type variable (\haskelllhstexinline{dt}) is the data type on which the constraints can be applied.
+The second type variable (\haskelllhstexinline{clist}) is the list of constraints itself.
+It is not just a list of \haskelllhstexinline{Constraint} but it is a list containing constraint constructors that will, when given a type of kind \haskelllhstexinline{k}, produce a constraint.
+This means that when \haskelllhstexinline{Cons} is pattern matched, the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
+
+\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+data Record (dt :: k) (clist :: [k -> Constraint]) where
+ Nil :: Record dt '[]
+ Cons :: c dt => Record dt cs -> Record dt (c ': cs)
+\end{lstHaskellLhstex}
+
+To incorporate this type in the \haskelllhstexinline{Expr} type, the \haskelllhstexinline{Ext} constructor changes as follows:
+
+\begin{lstHaskellLhstex}[caption={Data type for a list of constraints}]
+data Expr c
+ = Lit Int
+ | Add (Expr c) (Expr c)
+ | Ext (Record x c) x
+\end{lstHaskellLhstex}
+
+Furthermore, we define a type class that allows us to extract explicit dictionaries \haskelllhstexinline{Dict} from these records if the constraint can is present in the list.
+
+\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+class c `In` cs where
+ project :: Record dt cs -> Dict (c dt)
+instance {-# OVERLAPPING #-} c `In` (c ': cs) where
+ project (Cons _) = Dict
+instance {-# OVERLAPPING #-} c `In` cs => c `In` (b ': cs) where
+ project (Cons xs) = project xs
+\end{lstHaskellLhstex}
+
+Finally, creating these \haskelllhstexinline{Record} witnesses is a chore so this can be automated as well using a \haskelllhstexinline{CreateRecord} type class that will create a record structure cell by cell if and only if all type class constraints are available.
+
+\begin{lstHaskellLhstex}[caption={Membership functions for constraints}]
+class CreateRecord dt c where
+ createRecord :: Record dt c
+instance CreateRecord d '[] where
+ createRecord = Nil
+instance (c (d c0), CreateRecord (d c0) cs) =>
+ CreateRecord (d c0) (c ': cs) where
+ createRecord = Cons createRecord
+\end{lstHaskellLhstex}
+
+The class constraints for the interpretation instances can now be greatly simplified, as shown in the evaluation instance for \haskelllhstexinline{Expr}.
+The implementation remains the same, only that for the extension case, a trick needs to be applied to convince the compiler of the correct instances.
+Using \haskelllhstexinline{`In`}'s \haskelllhstexinline{project} function, a dictionary can be brought into scope.
+This dictionary can then subsequently be used to apply the type class function on the extension using the \haskelllhstexinline{withDict} function from the \haskelllhstexinline{Data.Constraint} library\footnote{\haskelllhstexinline{withDict :: Dict c -> (c => r) -> r}}.
+The \GHCmod{ScopedTypeVariables} extension is used to make sure the existentially quantified type variable for the extension is matched to the type of the dictionary.
+
+\begin{lstHaskellLhstex}[caption={Evaluation instance for the main data type}]
+class Eval v where eval :: v -> Int
+
+instance Eval `In` s => Eval (Expr s) where
+ eval (Lit i) = i
+ eval (Add l r) = eval l + eval r
+ eval (Ext r (e :: x)) = withDict (project r :: Dict (Eval x)) eval e
+\end{lstHaskellLhstex}
+
+Smart constructors need to be adapted as well, as can be seen from the smart constructor \haskelllhstexinline{subst}.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+subst :: (Typeable c, CreateRecord (Subt c) c) => Expr c -> Expr c -> Expr c
+subst l r = Ext createRecord (l `Subt` r)
+\end{lstHaskellLhstex}
+
+Finally, defining terms in the language is can be done immediately if the interpretations are known.
+For example, if we want to print the term $~(~(42+(38-4)))$, we can define it as follows.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+e0 :: Expr '[Print,Opt]
+e0 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))
+\end{lstHaskellLhstex}
+
+It is also possible to define terms in the \gls{DSL} as being overloaded in the interpretation.
+This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension.
+At the call site, the concrete list of constraints must be known.
+
+\begin{lstHaskellLhstex}[caption={Substitution smart constructor}]
+e1 :: (Typeable c
+ , CreateRecord (Neg c) c
+ , CreateRecord (Subst c) c)
+ => Expr c
+e1 = neg (neg (Lit 42 `Add` (Lit 38 `subt` Lit 4)))