In shallow embedding, the implementation for these types of semantics is difficult because there is no tangible abstract syntax tree.
In off-the-shelf deep embedding this is effortless since the function can pattern match on the constructor or structures of constructors.
-To demonstrate intensional analyses in classy deep embedding we write an optimizer that removes addition and subtraction by zero.
+To demonstrate intensional analyses in classy deep embedding we write an optimiser that removes addition and subtraction by zero.
In classy deep embedding, adding new semantics means first adding a new type class housing the function including the machinery for the extension constructor.
\begin{lstHaskellLhstex}
gdict = OptDict_3 opt_3
\end{lstHaskellLhstex}
-The implementation of the optimizer for the \haskelllhstexinline{Expr_3} data type is no complicated task.
+The implementation of the optimiser for the \haskelllhstexinline{Expr_3} data type is no complicated task.
The only interesting bit occurs in the \haskelllhstexinline{Add_3} constructor, where we pattern match on the optimised children to determine whether an addition with zero is performed.
If this is the case, the addition is removed.
\end{lstHaskellLhstex}
When using classy deep embedding to the fullest, the ability of the compiler to infer very general types expires.
-As a consequence, defining reusable expressions that are overloaded in their semantics requires quite some type class constraints that cannot be inferred by the compiler (yet) if they use many extensions.
+As a consequence, defining reuseable expressions that are overloaded in their semantics requires quite some type class constraints that cannot be inferred by the compiler (yet) if they use many extensions.
Solving this remains future work.
For example, the expression $\sim(42-38)+1$ has to be defined as:
NotLoop_g :: Expr_g d a -> Not_g d a
\end{lstHaskellLhstex}
-The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskelllhstexinline{d} type variable for it to be usable in the \haskelllhstexinline{Ext_g} constructor as can be seen in the smart constructor for \haskelllhstexinline{Neg_g}:
+The smart constructors for the language extensions inherit the class constraints of their data types and include a \haskelllhstexinline{Typeable} constraint on the \haskelllhstexinline{d} type variable for it to be useable in the \haskelllhstexinline{Ext_g} constructor as can be seen in the smart constructor for \haskelllhstexinline{Neg_g}:
\begin{lstHaskellLhstex}
neg_g :: (Typeable d, GDict (d (Neg_g d)), Typeable a, Num a) =>
Now that the shape of the type classes has changed, the dictionary data types and the type classes need to be adapted as well.
The introduced type variable \haskelllhstexinline{a} is not an argument to the type class, so it should not be an argument to the dictionary data type.
To represent this type class function, a rank-2 polymorphic function is needed \citep[\citesection{6.4.15}]{ghc_team_ghc_2021}\citep{odersky_putting_1996}.
-Concretely, for the evaluatior this results in the following definitions:
+Concretely, for the evaluator this results in the following definitions:
\begin{lstHaskellLhstex}
newtype EvalDict_g v = EvalDict_g (forall a. v a -> a)
Classy deep embedding differs from the hybrid approaches in the sense that it does not require the language extensions to be expressible in the core language.
\subsection{Comparison}
-No \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requiremens programmers have.
+No \gls{DSL} embedding technique is the silver bullet, there is no way of perfectly satisfying all requirements programmers have.
\Citet{sun_compositional_2022} provided a thorough comparison of embedding techniques including more axes than just the two stated in the expression problem.
\Cref{tbl:dsl_comparison_brief} shows a variant of their comparison table.
The \emph{poly.} style of embedding---including tagless-final---falls short of this requirement.
Intensional analysis is an umbrella term for pattern matching and transformations.
-In shallow embedding, intensional analysis is more complex and requires stateful views describing context but it is possible to implement though.
+In shallow embedding, intensional analysis is more complex and requires stateful views describing context, but it is possible to implement though.
Simple type system describes the whether it is possible to encode this embedding technique without many type system extensions.
In classy deep embedding, there is either a bit more scaffolding and boilerplate required or advanced type system extensions need to be used.
However, if needed, the technique generalises to \glspl{GADT} as well, adding rank-2 types to the list of type system requirements as well.
Finally, the abstract syntax tree remains observable which makes it suitable for intensional analyses, albeit using occasional dynamic typing for truly cross-extensional transformations.
-Defining reusable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around this remains future work.
+Defining reuseable expressions overloaded in semantics or using multiple semantics on a single expression requires some boilerplate still, getting around these issues remains future work.
\Cref{sec:classy_reprise} shows how the boilerplate can be minimised using advanced type system extensions.
\section*{Acknowledgements}
\label{sec:classy_reprise}
One of the unique selling points of this novel \gls{DSL} embedding technique is that it, in its basic form, does not require advanced type system extensions nor a lot of boilerplate.
However, generalising the technique to \glspl{GADT} arguably unleashes a cesspool of \emph{unsafe} compiler extensions.
-If we are willing to work with extensions, almost all of the boilerplate can be inferred or generated.
+If we are willing to work with extensions, almost all the boilerplate can be inferred or generated.
In classy deep embedding, the \gls{DSL} datatype is parametrised by a type variable providing a witness to the interpretation on the language.
When using multiple interpretations, these need to be bundled in a data type.
Using the \gls{GHC}'s \GHCmod{ConstraintKind} extension, we can make these witnesses explicit, tying into \gls{HASKELL}'s type system immediately.
-Furthermore, this constraint does not necessarily has to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead \citep{yorgey_giving_2012}.
+Furthermore, this constraint does not necessarily have to be a single constraint, after enabling \GHCmod{DataKinds} and \GHCmod{TypeOperators}, we can encode lists of witnesses instead \citep{yorgey_giving_2012}.
The data type for this list of witnesses is \haskelllhstexinline{Record} as shown in \cref{lst_cbde:record_type}.
This \gls{GADT} is parametrised by two type variables.
The first type variable (\haskelllhstexinline{dt}) is the type or type constructor on which the constraints can be applied and the second type variable (\haskelllhstexinline{clist}) is the list of constraints constructors itself.
\end{lstHaskellLhstex}
It is also possible to define terms in the \gls{DSL} as being overloaded in the interpretation.
-This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension in a similar fashion as was required for \haskelllhstexinline{GDict}.
+This does require enumerating all the \haskelllhstexinline{CreateRecord} type classes for every extension similarly as was required for \haskelllhstexinline{GDict}.
At the call site, the concrete list of constraints must be known.
\begin{lstHaskellLhstex}
repositories / phd-thesis.git / blobdiff