arbitrary monads, not just lists. Guards are desugared to sequential
compositions $(>>)$ and a guard operation for the monad. We omitted these
constructs since for lists they are directly definable.

The following table lists the intended desugaring rules, where $\%u$ is a
freshly chosen name that is guaranteed to be unique and not used elsewhere in
the term,.

$\small\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SListComp}(t,q)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MApp}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QEmpty}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}}(\%u,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Return}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MVar}}(\%u)))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QBind}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x}},t,q)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}}(\%u,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Bind}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLam}}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x}}],{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MApp}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MVar}}(\%u)))))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QGuard}(t,q)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}}(\%u,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CIf}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MApp}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MVar}}(\%u)),{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CList}}([])))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x}},t,q)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}}(\%u,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Let}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MApp}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MVar}}(\%u))))\end{array}$

As we extended the sequential learning process of the previous case study, we
assumed that the translation rules of the whole Pidgin language are fixed in
advance.

Hypothesis space. Our hypothesis space $\mathcal{H}^{lc}$ is mostly identical
with $\mathcal{H}^{1}$, but it does not contain any of the meta-rules Case,
Throw, Unzip or Fresh. Instead, to express the desugaring rules in this table,
a macro version of the fresh rule was necessary:

$\displaystyle{\Gamma;i:\texttt{Id}\vdash
M:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$
Meta-lambda
$\displaystyle\Gamma\vdash\mathbf{let}\,i=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}M}})}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\mathstrut$

Decomposition. This case study demonstrates that sometimes ”large” (¿2)
constructor groups are necessary, and our enumerative method does not scale up
to large groups.

The smallest constructor group required for any example is SListComp and
QEmpty, so they need to be included in the first step. But any list
comprehension example that does not use the other qualifiers simply reduces to
Return, therefore we can not learn the intended semantics of this group
without the others. Adding the simplest qualifier, QGuard, is still not
enough: without any bound variable we can not write examples that exclude
similarly erroneous desugarings. Setting up the first step of the sequential
learning task with just SListComp and QEmpty or perhaps adding QGuard
demonstrates a case where we would commit to a wrong translation rule early,
and can not continue the learning process.

The first step needs to contain at least three source constructors, one of
them should be QBind or QLet. But this group is too large, with combined AST
size of 14 our search runs to a timeout.

As a second test, we used a hint from the user: we provided the semantics
(desugaring rule) of SListComp. This allowed us to learn the semantics of each
qualifier one-by-one.

Results. The results we obtained after the user hint are presented in Table 2.

Constructor group | AST size | Index | #tests | time
---|---|---|---|---
QEmpty | 3 | 6 | 1 | 0.0s
QBind | 10 | 97632734 | 1 | 25min27s
QLet | 7 | 116747 | 1 | 2s
QGuard | 6 | 31307 | 1 | 1s
total |  |  | 4 | 25min30s
Table 2. Case study – List comprehensions

In one case, QGuard, the found semantics is equivalent with the intended one
but shorter:

$\small\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QGuard}(t,q)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CIf}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}}(\%\\_,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CList}}([])))\\\
\end{array}$

Test cases. We only needed one test case for every individual learning task:
one test case suffices per source constructor. These test cases are not
trivial: to demonstrate the non-trivial scoping behaviour of qualifiers we
needed to embed them. To hypothetically auto-generate such test cases the
binding and scoping rules of the source language must be taken into account.

###  6.4. Try/Catch/Finally

Setup. Finally we extended the Pidgin languages with exceptions. The source
Pidgin is extended with try/catch/finally, which desugars to the core language
extended with just try/catch.

$\small\begin{array}[]{rcl}t,t_{1},t_{2},t_{3}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{STerm}}&::=&\dots\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{STryCatchFinally}(t_{1},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{2},t_{3})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SThrow}(t)}\\\
e,e_{1},e_{2},e_{3}\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}&::=&\dots\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CTryCatch}(e_{1},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},e_{2})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CThrow}(e)}\end{array}$

In a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{CTryCatchFinally}(t_{1},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{2},t_{3})}$
expression, first is $t_{1}$ is executed. If it terminates normally with value
$v$ then $t_{3}$ is executed with default outcome $v$. If it raises an
exception $ex$, then $t_{2}$ is executed with
$\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}}$
bound to $ex$. If executing $t_{2}$ terminates normally with value $v$ then
$t_{3}$ is executed with default outcome $v$. Otherwise if $t_{2}$ also raises
an exception $ex^{\prime}$ then $t_{3}$ is executed with default outcome
$ex^{\prime}$. (In particular, the absence of an exception handler can be
emulated by having the handler be
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{Throw}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}$.)
When the `finally` expression $t_{3}$ is executed, if it terminates normally
with some result value, that value is ignored and the default outcome is
performed instead. If $t_{3}$ also raises an exception then this exception is
the result and the default outcome is ignored.

Our intended desugaring is the following:

$\small\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{STryCatchFinally}(t_{1},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\%v}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CTryCatch}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CTryCatch}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})),\\\
&&\qquad\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\%j}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}}(\%\\_,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CThrow}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\%j}})))),\\\
&&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}}(\%\\_,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\%v}})))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{CThrow}(t)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CThrow}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\end{array}$

Note that this desugaring rule duplicates the translated finally block
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$.
To avoid code bloat, one would normally create a thunk for the finally block.
But our method can not distinguish the thunked version from inserting the
finally block twice, and the latter is smaller. We use CLet with an unused
variable for sequencing operations.

Hypothesis space. To express the intended desugaring, we need a version of the
Fresh rule for the new try-catch construct:

$\displaystyle{\Gamma\vdash
M:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$$\displaystyle\hskip
8.00003pt{\Gamma;x:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\vdash
N:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$
Fresh-trycatch
$\displaystyle\Gamma\vdash\mathbf{let}\,i=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CTryCatch}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}M}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}N}}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Var}}(i)/x]):{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\mathstrut$

Our first hypothesis space was based on $\mathcal{H}^{1}$, but we removed
Case, Throw, and Unzip, and added Fresh-trycatch. But we found that the size
of the intended desugaring is too large for such a general hypothesis space.

We created a second, severely restricted hypothesis space $\mathcal{H}^{tcf}$.
It only contained Fresh, Fresh-trycatch, and the core term constructors CThrow
and CTryCatch. We also used an additional user layer: Fresh and Fresh-trycatch
was in the first layer, so they were not allowed inside the core term
constructors.

Decomposition. The relabelling of SThrow can easily be learned on its own,
because throw has a unique behaviour. This allows us to learn in two steps.

Results. The desugaring rule for STryCatchFinally (even without thunking) is
very large, and we reached the timeout even with the very restricted
hypothesis space $\mathcal{H}^{tcf}$. To see how much we missed the mark we
ran the search to completion. The results are shown in Table 3.

Constructor group | AST size | Index | #tests | time
---|---|---|---|---
SThrow | 2 | 18 | 1 | 0.0s
STryCatchFinally | 13 | 396643849 | 7 | 1hours 16min 54s
total |  |  | 8 | 1hours 16min 54s
Table 3. Case study – Try-catch-finally

Test cases. Learning the desugaring rule of STryCatchFinally needs many
complex examples. First, try-catch-finally can branch: the main block may or
may not throw and the catch block also may or may not throw. Covering all
cases already needs 3 examples. We also need to ensure the evaluation order.
In general, branching constructs needs at least as many examples as potential
paths of execution. Also, to fix evaluation order we need examples that
exclude any other permutation, and with constructs with many parameters
(STryCatchFinally has the most parameters amongst our constructs: 4) the
number of potential permutations are higher.

###  6.5. Threats to validity

Perhaps the most important, but at the same time the hardest thing to evaluate
is how well our approach generalises. We can not yet evaluate our methods on
real life programming languages, because real desugarings are too large. Pre-
defined examples always carry the danger of inadvertent cherry-picking of the
results. A further danger is that since we know the intended desugarings in
advance, we do not need to experiment with user guidance such as restrictions
on the hypothesis space, and we risk inadvertently underestimating the amount
of user guidance needed.

We try to highlight each form of user guidance that we used in our case
studies: each shows a limitation of our approach. We do not include writing
the correct test cases or decomposing the language, since they were assumed to
be the user’s task from the beginning.

  1. (1)

Our selection of meta-rules was somewhat tailored to the requirements. For
example, we did not include a Fresh-like rule for CLam because we did not need
it.

  2. (2)

We needed a hand-written meta-rule Unzip to express the desugaring rule of
SFor. Other meta-rules used can be imagined to be auto-generated, but the
Unzip rule is hand-crafted.

  3. (3)

In two cases, SBetween and STryCatchFinally, we used a severely restricted
hypothesis space, and in the second case we even used a user-defined layer.
This shows the scalability problem: the desugaring rules have AST size 14 and
13 respectively, which is too large for our method to find with an
unrestricted hypothesis space.

  4. (4)

Similarly, we needed user guidance to provide the rule of SListComp. This was
again a scalability problem, although a different one: we would have to learn
the rules for too many term constructors at once.

We do not regard these limitations as fatal flaws. Instead, they may
illustrate that our approach should be thought of as a “desugaring synthesis
assistant”, rather than a fully automatic synthesis tool. Knowledgeable
semantics engineers may be able to make use of our approach’s brute-force
search even if detailed guidance is sometimes needed, analogously to
interactive proof assistants in theorem proving. In this light our work may be
regarded as identifying an approach that may work, but further research (e.g.
usability studies) would need to be done to determine whether our approach
offers significant benefits in real semantics engineering efforts.

##  7\. Related work

Program synthesis is a vast research field, for a review see Gulwani et al.
(2017). To solve the desugaring extension problem, we experimented with
enumerative program synthesis, which may serve as a baseline algorithm, but we
did not use extensive pruning or heuristics which may allow us to scale up
learning to larger examples. In general, it is not clear how more
sophisticated program synthesis methods could be applied to the desugaring
extension problem. For example, in the desugaring extension problem there can
be multiple unknown language constructs and they may appear in argument
position in the examples. The implications of these differences need to be
investigated. Most algorithms in program synthesis are specialised to a fixed
language — it is an open question how to abstract away the target language and
what additional information on the target language is needed. Many algorithms
are not specialised to inductive synthesis, and thus it is an open question
whether any such method leads to a significant speed-up in our use-case.

The most closely related work, by Krishnamurthi et al. (2019), has been
discussed and compared with our approach throughout the paper. There is
existing work to automatically synthesise translations between languages, such
as _verified lifting_ (Kamil et al., 2016; Ahmad et al., 2019), but they
search for translations of source _programs_ (of a fixed source language) to a
fixed target language, as opposed to searching for translation rules for the
source _language_ , which is a rather different problem. Nevertheless there
may be interesting connections between verified lifting and desugaring
synthesis, which should be explored.

We are aware of a number of works that could serve as the basis of further
investigation. FlashMeta (Polozov and Gulwani, 2015) is an industrial
framework by Microsoft to build synthesis algorithms for user-defined target
languages. The framework is based on inductive enumerative synthesis, thus it
is possible that it could be used for our problem. The framework allows the
user to define witness functions for the target language, that capture part of
the inverse behaviour of the functions in the language and can speed up the
search. A possible future direction is investigating whether providing
suitable witness functions for a given core language is feasible, and whether
it speeds up the search in our examples.

Bartha and Cheney (2020) used _meta-interpretive learning_ (Muggleton et al.,
2014), a framework for inductive logic programming, to learn the small-step
semantic rules of a very simple programming language. The task they solved is
close to ours; they attempted to learn inductively the structural operational
semantics rules of a language rather than desugaring. However, their approach
relied on identifying problem-specific _meta-rules_ (needed by meta-
interpretive learning), so it is hard to see how their method can be
generalised to various language features or larger languages.

In our code we represented the search space by sorted terms, a.k.a. algebraic
data types (ADTs) in typed functional languages such as ML or Haskell. We are
aware of two bodies of work that consider synthesising functions on ADTs:
_type-directed synthesis_ as in Myth (Osera and Zdancewic, 2015) and Myth2
(Frankle et al., 2016), and an extension of the Sketch framework (Solar-
Lezama, 2013) called _SyntRec_ (Inala et al., 2017). Type-directed synthesis
as implemented in Myth and Myth2 is not easy to apply to our problem because
it requires the example set to be closed under recursive calls (for example,
to learn a recursive function on a list we need examples showing the results
of that function on all sub-lists). On the other hand, SyntRec is more
directly applicable to our problem, indeed it was the system used in the
fourth attempt analysed by kle, but SyntRec was only successfully applied to
languages without state. SyntRec, when applied to desugaring synthesis
problems, also requires the core language interpreter to be implemented in the
synthesis language, whereas our approach assumes only an opaque implementation
of the core language is available. Nevertheless, further evaluation is needed
to see whether these systems can be modified to provide full solutions to the
Pidgin challenge problem, or whether insights from their approaches can be
incorporated into our approach.

Tested semantics such as $\lambda_{JS}$ for JavaScript (Guha et al., 2010), S5
(Li et al., 2015), and $\lambda_{Py}$ (Politz et al., 2013) provide case
studies showing how to handle large, real languages by desugaring to a core
language. Compared to Pidgin, these desugarings are considerably larger, and
from inspecting their code or formalization artifacts, it is clear that some
of the desugaring rules are much too large for our enumerative approach to
handle (e.g. desugaring JavaScript function declarations to $\lambda_{JS}$
requires around 50 lines of Haskell code). The Scheme report (Sperber et al.,
2010) also specifies certain constructs by desugaring to a core, and may be a
more plausible intermediate goal. Interestingly, Li et al. (2015) identify the
issue of _semantic bloat_ , resulting from desugarings that defensively cover
all cases, but yield large amounts of boilerplate that is not needed in common
cases. This suggests an alternative strategy for learning complex desugarings,
mirroring the gradual inductive approach apparently followed in practice, in
which we might first seek simple explanations for common constructs in common
cases (e.g. a “Newtonian model”), and then look for counterexamples to the
simple model and try to repair it to accommodate them (e.g. a “relativistic
model”). Another interesting possibility is to analyze (non)interdefinability
of core language features (see e.g. (Pierce et al., 2010)) to guide the design
of the core language or structure the decomposition into incremental learning
problems. We leave these intriguing possibilities for future work.

##  8\. Conclusion and future work

Developing correct semantics rules for real-world languages is a necessary,
but arduous, prerequisite to formal analysis. The problem of learning
desugarings from examples has been introduced by Krishnamurthi et al. (2019),
but the four approaches they tried each had inherent limitations. In this
paper we have carefully analysed the problem and highlighted two key aspects:
decomposability of language feature learning into a sequence of easier
_desugaring extension problems_ , and careful attention to the hypothesis
space and meta-language in which the desugaring rules are expressed. Moreover,
we show that, with some additional guidance, a simple enumerative search
technique can successfully solve the desugaring synthesis challenge problem
introduced by Krishnamurthi et al. (2019), and we evaluated our approach on
additional extensions such as simple list comprehensions and exception
handling with ‘finally’. While this is just one step toward the vision of
learning the next 700 language semantics, our experimental results provide
grounds for optimism. We plan to explore whether our approach can be
incorporated into a CEGIS loop to automatically learn both semantics rules and
suitable examples; whether the choice of suitable hypothesis spaces or meta-
template rules can be automated; and whether our approach can be scaled up to
synthesise desugarings for larger, more realistic languages that have been
developed by hand, such as JavaScript (Guha et al., 2010) and Python (Politz
et al., 2013).

## Acknowledgements

We would like to thank the anonymous reviewers and our shepherd Shriram
Krishnamurthi for helpful feedback and suggestions for improvement. We also
thank the artifact evaluators and AEC chairs for allowing us to update our
artifact submission to reflect the final version of the paper. This work was
supported by ERC Consolidator Grant Skye (grant number 682315) and by an ISCF
Metrology Fellowship grant provided by the UK government’s Department for
Business, Energy and Industrial Strategy (BEIS). Vaishak Belle was supported
by a Royal Society University Research Fellowship.

## References

  * Ahmad et al. (2019) Maaz Bin Safeer Ahmad, Jonathan Ragan-Kelley, Alvin Cheung, and Shoaib Kamil.  Automatically translating image processing libraries to Halide.  _ACM Trans. Graph._ , 38(6), November 2019.  ISSN 0730-0301.  doi: 10.1145/3355089.3356549.  URL https://doi.org/10.1145/3355089.3356549.
  * Alur et al. (2013) R. Alur, R. Bodik, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa.  Syntax-guided synthesis.  In _2013 Formal Methods in Computer-Aided Design_ , pages 1–8, 2013\.  doi: 10.1109/FMCAD.2013.6679385.
  * Alur et al. (2017) Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa.  Scaling enumerative program synthesis via divide and conquer.  In Axel Legay and Tiziana Margaria, editors, _Tools and Algorithms for the Construction and Analysis of Systems_ , pages 319–336, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg.  ISBN 978-3-662-54577-5.
  * Amin and Tate (2016) Nada Amin and Ross Tate.  Java and scala’s type systems are unsound: The existential crisis of null pointers.  In _Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications_ , OOPSLA 2016, page 838–848, New York, NY, USA, 2016. Association for Computing Machinery.  ISBN 9781450344449.  doi: 10.1145/2983990.2984004.  URL https://doi.org/10.1145/2983990.2984004.
  * Bartha and Cheney (2020) Sándor Bartha and James Cheney.  Towards meta-interpretive learning of programming language semantics.  In _Proceedings of the 29th International Conference on Inductive Logic Programming (ILP 2019)_ , number 11770 in LNCS, pages 16–25, 06 2020.  ISBN 978-3-030-49209-0.  doi: 10.1007/978-3-030-49210-6˙2.
  * Comon et al. (2007) H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi.  Tree automata techniques and applications.  Available on: http://www.grappa.univ-lille3.fr/tata, 2007.  release October, 12th 2007.
  * Duregård et al. (2012) Jonas Duregård, Patrik Jansson, and Meng Wang.  Feat: Functional enumeration of algebraic types.  _SIGPLAN Not._ , 47(12):61–72, September 2012\.  ISSN 0362-1340.  doi: 10.1145/2430532.2364515.  URL https://doi.org/10.1145/2430532.2364515.
  * Felleisen et al. (2001) Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi.  _How to Design Programs_.  MIT Press, 2001.
  * Filaretti and Maffeis (2014) Daniele Filaretti and Sergio Maffeis.  An Executable Formal Semantics of PHP.  In Richard Jones, editor, _ECOOP_ , pages 567–592, Berlin, Heidelberg, 2014. Springer.  ISBN 978-3-662-44202-9.
  * Frankle et al. (2016) Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic.  Example-directed synthesis: A type-theoretic interpretation.  _SIGPLAN Not._ , 51(1):802–815, January 2016\.  ISSN 0362-1340.  doi: 10.1145/2914770.2837629.  URL http://doi.acm.org/10.1145/2914770.2837629.
  * Guha et al. (2010) Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi.  The essence of JavaScript.  In _Proceedings of the 24th European Conference on Object Oriented Programming (ECOOP 2010)_ , pages 126–150, 2010.  doi: 10.1007/978-3-642-14107-2“˙7.  URL https://doi.org/10.1007/978-3-642-14107-2_7.
  * Gulwani et al. (2017) Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh.  Program synthesis.  _Foundations and Trends® in Programming Languages_ , 4(1-2):1–119, 2017.  ISSN 2325-1107.  doi: 10.1561/2500000010.  URL http://dx.doi.org/10.1561/2500000010.
  * Inala et al. (2017) Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, and Armando Solar-Lezama.  Synthesis of recursive ADT transformations from reusable templates.  In Axel Legay and Tiziana Margaria, editors, _Tools and Algorithms for the Construction and Analysis of Systems_ , pages 247–263, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg.  ISBN 978-3-662-54577-5.
  * Jha et al. (2010) Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari.  Oracle-guided component-based program synthesis.  In _Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South Africa, 1-8 May 2010_ , pages 215–224, 2010.  doi: 10.1145/1806799.1806833.  URL https://doi.org/10.1145/1806799.1806833.
  * Jung et al. (2017) Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer.  Rustbelt: Securing the foundations of the rust programming language.  _Proc. ACM Program. Lang._ , 2(POPL), December 2017.  doi: 10.1145/3158154.  URL https://doi.org/10.1145/3158154.
  * Kamil et al. (2016) Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama.  Verified lifting of stencil computations.  In _Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation_ , PLDI ’16, page 711–726, New York, NY, USA, 2016. Association for Computing Machinery.  ISBN 9781450342612.  doi: 10.1145/2908080.2908117.  URL https://doi.org/10.1145/2908080.2908117.
  * Kern and Greenstreet (1999) Christoph Kern and Mark R. Greenstreet.  Formal verification in hardware design: A survey.  _ACM Trans. Des. Autom. Electron. Syst._ , 4(2):123–193, April 1999.  ISSN 1084-4309.  doi: 10.1145/307988.307989.  URL https://doi.org/10.1145/307988.307989.
  * Krishnamurthi et al. (2019) Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty.  The Next 700 Semantics: A Research Challenge.  In _SNAPL_ , 2019.
  * Landin (1966) P. J. Landin.  The next 700 programming languages.  _Commun. ACM_ , 9(3):157–166, March 1966.  ISSN 0001-0782.  doi: 10.1145/365230.365257.  URL https://doi.org/10.1145/365230.365257.
  * Li et al. (2015) Junsong Li, Justin Pombrio, Joe Gibbs Politz, and Shriram Krishnamurthi.  Slimming languages by reducing sugar: A case for semantics-altering transformations.  In _2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)_ , Onward! 2015, page 90–106, New York, NY, USA, 2015. Association for Computing Machinery.  ISBN 9781450336888.  doi: 10.1145/2814228.2814240.  URL https://doi.org/10.1145/2814228.2814240.
  * Maffeis et al. (2008) Sergio Maffeis, John C. Mitchell, and Ankur Taly.  An Operational Semantics for JavaScript.  In G. Ramalingam, editor, _ESOP_ , pages 307–325, Berlin, Heidelberg, 2008. Springer.  ISBN 978-3-540-89330-1.
  * Marlow et al. (2009) Simon Marlow, Simon Peyton Jones, and Satnam Singh.  Runtime support for multicore haskell.  In _Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming_ , ICFP ’09, page 65–78, New York, NY, USA, 2009. Association for Computing Machinery.  ISBN 9781605583327.  doi: 10.1145/1596550.1596563.  URL https://doi.org/10.1145/1596550.1596563.
  * Meinke and Tucker (1993) K. Meinke and J. V. Tucker.  Universal algebra.  In _Handbook of Logic in Computer Science (Vol. 1): Background: Mathematical Structures_ , page 189–368. Oxford University Press, Inc., USA, 1993\.  ISBN 0198537352.
  * Moggi (1991) Eugenio Moggi.  Notions of computation and monads.  _Inf. Comput._ , 93(1):55–92, 1991.  doi: 10.1016/0890-5401(91)90052-4.  URL https://doi.org/10.1016/0890-5401(91)90052-4.
  * Morandat et al. (2012) Floréal Morandat, Brandon Hill, Leo Osvald, and Jan Vitek.  Evaluating the Design of the R Language: Objects and Functions for Data Analysis.  In _ECOOP_ , pages 104–131, Berlin, Heidelberg, 2012. Springer-Verlag.  ISBN 978-3-642-31056-0.
  * Muggleton et al. (2014) Stephen H. Muggleton, Dianhuan Lin, Niels Pahlavi, and Alireza Tamaddoni-Nezhad.  Meta-interpretive Learning: Application to Grammatical Inference.  _Mach. Learn._ , 94(1):25–49, January 2014.  ISSN 0885-6125.
  * Nienhuis et al. (2016) Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell.  An operational semantics for c/c++11 concurrency.  In _Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications_ , OOPSLA 2016, page 111–128, New York, NY, USA, 2016. Association for Computing Machinery.  ISBN 9781450344449.  doi: 10.1145/2983990.2983997.  URL https://doi.org/10.1145/2983990.2983997.
  * Osera and Zdancewic (2015) Peter-Michael Osera and Steve Zdancewic.  Type-and-example-directed program synthesis.  In _Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015_ , pages 619–630, 2015.  doi: 10.1145/2737924.2738007.  URL https://doi.org/10.1145/2737924.2738007.
  * Pierce et al. (2010) Benjamin C. Pierce, Alessandro Romanel, and Daniel Wagner.  The Spider Calculus: Computing in active graphs, 2010.  Manuscript, available from http://www.cis.upenn.edu/~bcpierce/papers/spider_calculus.pdf.
  * Politz et al. (2013) Joe Gibbs Politz, Alejandro Martinez, Matthew Milano, Sumner Warren, Daniel Patterson, Junsong Li, Anand Chitipothu, and Shriram Krishnamurthi.  Python: The Full Monty.  In _OOPSLA_ , pages 217–232, New York, NY, USA, 2013. ACM.  ISBN 978-1-4503-2374-1.
  * Polozov and Gulwani (2015) Oleksandr Polozov and Sumit Gulwani.  FlashMeta: A framework for inductive program synthesis.  In _OOPSLA_ , volume 50, 10 2015.  doi: 10.1145/2858965.2814310.
  * Reynolds et al. (2019) Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli.  cvc4sy: Smart and fast term enumeration for syntax-guided synthesis.  In Isil Dillig and Serdar Tasiran, editors, _Computer Aided Verification_ , pages 74–83, Cham, 2019. Springer International Publishing.  ISBN 978-3-030-25543-5.
  * Solar-Lezama (2013) Armando Solar-Lezama.  Program sketching.  _Int. J. Softw. Tools Technol. Transf._ , 15(5-6):475–495, 2013.  doi: 10.1007/s10009-012-0249-7.  URL https://doi.org/10.1007/s10009-012-0249-7.
  * Solar-Lezama et al. (2005) Armando Solar-Lezama, Rodric M. Rabbah, Rastislav Bodík, and Kemal Ebcioglu.  Programming by sketching for bit-streaming programs.  In _Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005_ , pages 281–294, 2005.  doi: 10.1145/1065010.1065045.  URL https://doi.org/10.1145/1065010.1065045.
  * Sperber et al. (2010) Michael Sperber, R. Kent Dybvig, Matthew Flatt, Anton van Straaten, Robby Findler, and Jacob Matthews.  _Revised [6] Report on the Algorithmic Language Scheme_.  Cambridge University Press, USA, 1st edition, 2010.  ISBN 0521193990.
  * Wadler (1992a) Philip Wadler.  The essence of functional programming.  In _Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992_ , pages 1–14, 1992a.  doi: 10.1145/143165.143169.  URL https://doi.org/10.1145/143165.143169.
  * Wadler (1992b) Philip Wadler.  Comprehending monads.  _Mathematical Structures in Computer Science_ , 2(4):461–493, 1992b.  doi: 10.1017/S0960129500001560.

##  Appendix A Reference implementation of Pidgin

For concreteness, we describe our reference implementation of the Pidgin
source language, core language, the core language interpreter, and the
intended desugaring translation in a Haskell-like pseudocode. The source
language behavior is defined as the composition of the desugaring and core
language interpreter (though in our implementation we give a direct
definition). Our implementation (submitted as part of the supplementary
material) shows the full details as runnable (but considerably more complex
and less readable) Haskell code. The differences are largely due to the
requirements of using FEAT for enumerating terms.

    newtype Id = Id String

    data Op = UMin | Not | Plus | Minus | And | Or | LT | GT

    data STerm = SVar String
               | SPrim Op [STerm]
               | SBetween STerm STerm STerm
               | SNum Int
               | SStr String
               | STrue
               | SFalse
               | SIf STerm STerm STerm
               | SLet Id STerm STerm
               | SLetRec Id STerm STerm
               | SLam [Id] STerm
               | SApp STerm [STerm]
               | SAssign [Id] STerm
               | SList [STerm]
               | SListCase STerm STerm STerm
               | SFor STerm [(Id,STerm)] STerm

    data CTerm = CVar Id
               | CPrim1 Op CExp
               | CPrim2 Op CExp
               | CNum Int
               | CStr String
               | CBool Bool
               | CIf CTerm CTerm CTerm
               | CLet Id CTerm CTerm
               | CLetRec Id CTerm CTerm
               | CLam [Id] CTerm
               | CApp CTerm [CTerm]
               | CAssign Id CTerm
               | CList [CTerm]
               | CListCase CTerm CTerm CTerm

    rename :: Id -> Id -> CTerm -> CTerm

Figure 6. Source and target term languages

    type Env = Map Id CTerm
    type Result a = ... -- error and state monad
    raise :: Error -> Result a
    fresh :: Result Id
    read :: Id -> Result CTerm
    write :: Id -> CTerm -> Result ()
    doUnop :: Op -> CTerm -> Result CTerm
    doBinop :: Op -> CTerm -> CTerm -> Result CTerm
    run : Result a -> Env -> Either a Error

Figure 7. Helper functions for evaluation and desugaring

    eval :: CTerm -> Either CTerm Error
    eval t = run (eval’ t) emptyEnv

    eval’ :: Map Id CTerm -> CTerm -> Result CTerm
    eval’ (CVar x)   = do
      e <- read x  -- might be an expression bound by letrec
      eval’ e
    eval’ (CPrim1 op e) = do
      v <- eval’ e
      case op of
        UMin -> doUnOp (negate @Int) v
        Not  -> doUnOp not v
        _    -> raise TypeError
    eval’ (CPrim2 op e1 e2) = do
      v1 <- eval’ e1
      v2 <- eval’ e2
      case op of
        Plus  ->
          case v1 of
            (CNum _) -> doBinOp ((+) @Int) v1 v2
            (CList l1) -> case v2 of
                            CList l2 -> return (CList (l1 ++ l2))
                            _ -> raise TypeError
            _ -> raise TypeError
        Minus -> doBinOp ((-) @Int) v1 v2
        And   -> doBinOp (&&) v1 v2
        Or    -> doBinOp (||) v1 v2
        LT    -> doBinOp ((<) @Int) v1 v2
        GT    -> doBinOp ((>) @Int) v1 v2
        _ -> raise TypeError
    eval’ ex@(CNum _) = return ex
    eval’ ex@(CStr _) = return ex
    eval’ ex@(CBool _) = return ex

Figure 8. Reference interpreter for Core Pidgin, part 1

    eval’ (CIf ex1 ex2 ex3) = do
      c <- eval’ ex1
      case c of
        CBool b  -> if b then eval’ ex2 else eval’ ex3
        _ -> raise TypeError
    eval’ (CLet i ex1 ex2) = do
      v <- eval’ ex1  -- let is eager
      i2 <- fresh
      write i2 v
      eval’ (rename i id ex2)
    eval’ (CLetRec i ex1 ex2) = do
      i2 <- fresh
      write i2 (rename i id ex1)  -- any recursive references will be expanded later
      eval’ (rename i id ex2)
    eval’ ex@(CLam _ _) = return ex
    eval’ (CApp ex es) = do
      f <- eval’ ex
      case f of
        CLam is body -> do
            vs <- mapM eval’ es
            case length is == length vs of
              True -> do iterM write (zip is vs)
                         eval’ body
              False -> case vs of
                         [ CLang’ (CList vs’)] ->
                            case length is == length vs’ of
                              True -> do iterM write (zip is vs’)
                                         eval’ body
                              False -> raise ArgumentNumberMismatchError
                         _ -> raise ArgumentNumberMismatchError
        _ -> raise TypeError
    eval’ (CAssign x ex) = do
      v <- eval’ ex
      write x v
      return v
    eval’ (CList es) = do
      vs <- mapM eval’ es
      return (CList vs)
    eval’ (CListCase e1 e2 e3) = do
      l <- eval’ e1
      case l of
        CList []     -> eval’ e2
        CList (e:es) -> do
              f <- eval’ e3
              eval’ (CApp f [e,(CList es)])
        _ -> raise TypeError

Figure 9. Reference interpreter for Core Pidgin, part 2

    ds :: STerm -> Either CTerm Error
    ds t = run (ds’ t) emptyEnv

    ds’ :: STerm -> Result STerm
    ds’ (SVar i) = return (CVar i)
    ds’ (SNum n) = return (CNum n)
    ds’ (SStr s) = return (CStr s)
    ds’ (SIf x y z) = do
         x’ <- ds’ x
         y’ <- ds’ y
         z’ <- ds’ z
         return (CIf x’ y’ z’)
    ds’ (SLet i x y ) = do
         x’ <- ds’ x
         y’ <- ds’ y
         return (CLet i x’ y’)
    ds’ (SLetRec i x y ) = do
         x’ <- ds’ x
         y’ <- ds’ y
         return (CLetRec i x’ y’)
    ds’ (SLam ids x) = do
         x’ <- ds’ x
         return (CLam ids x’)
    ds’ (SApp x xs)) = do
         x’  <- ds’ x
         xs’ <- mapM ds’ xs
         return (CApp x’ xs’)
    ds’ (SAssign i x)) = do
         x’ <- ds’ x
         return (CAssign i x’)
    ds’ (SList xs) = do
         xs’ <- mapM ds’ xs
         return (CList xs’)
    ds’ (SListCase x y z) = do
         x’ <- ds’ x
         y’ <- ds’ y
         z’ <- ds’ z
         return (CListCase x’ y’ z’)

Figure 10. Desugaring reference implementation, part 1: straightforward cases.

    ds’ STrue = return (CBool True)
    ds’ SFalse = return (CBool False)
    ds’ (SPrim o [s]) = do
         s’  <- ds’ s
         CPrim1(o,s’)
    ds’ (SPrim o [s1,s2]) = do
         s1’  <- ds’ s1
         s2’ <- ds’ s2
         CPrim2(o,s1’,s2’)
    ds’ (SPrim (_,_)) = errorResult (syntaxError)
    ds’ (SBetween x y z) = do
         x’ <- ds’ x
         y’ <- ds’ y
         z’ <- ds’ z
         v1 <- freshVar
         v2 <- freshVar
         v2 <- freshVar
         return (CLet(v1,x’,CLet(v2,y’,CLet(v3,z’,
                          CAnd (CPrim2(LT, CVar v1, CVar v2),
                                       CPrim2(LT, CVar v2, CVar v3))))))
    ds’ (SFor x bs y) = do
         x’  <- ds’ x
         bs’ <- mapM dsBind bs
         y’  <- ds’ y
         (ids, zs) <- unzip bs’
         return (CApp (x’, [CLam(ids, y’), CList(zs)]))

    dsBind :: (Id,STerm) -> Result (Id,CTerm)
    dsBind (i,x) = do
            x’ <- ds’ x
            return (i,x’)

Figure 11. Desugaring reference implementation, part 2: nontrivial cases.